[STATEMENT]
lemma (in Corps) Zl_mI_nonzero:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
      I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow>  Zl_mI K P I j \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (case_tac "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n = 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 \<noteq> \<zero>
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (frule representative_of_pd_valuation[of "P 0"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 \<noteq> \<zero>
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (subgoal_tac "O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K (P 0)\<^esub>)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 \<noteq> \<zero>
 2. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)
 3. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (subgoal_tac "Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K (P 0)\<^esub>) I")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>); Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 \<noteq> \<zero>
 2. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K P 0\<^esub>) I
 3. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)
 4. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (Vr K (\<nu>\<^bsub>K P 0\<^esub>)) I; I \<noteq> {\<zero>\<^bsub>Vr K (\<nu>\<^bsub>K P 0\<^esub>)\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>); Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> Ig K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<zero>
 2. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K P 0\<^esub>) I
 3. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)
 4. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (simp add:Ig_nonzero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>); O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I 0 = Ig K (\<nu>\<^bsub>K P 0\<^esub>) I
 2. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)
 3. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (simp add:Ig_def Zl_mI_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; j = 0; n = 0; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> O\<^bsub>K P 0\<^esub> = Vr K (\<nu>\<^bsub>K P 0\<^esub>)
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (simp add:ring_n_pd_def Vr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (frule value_Zl_mI[of n P I j], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n; Zl_mI K P I j \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n; Zl_mI K P I j \<in> I; (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n; \<zero> \<in> I; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule distinct_pds_valuation1[of n j P], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n; \<zero> \<in> I; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule singleton_sub[of "\<zero>" "I"],
        frule sets_not_eq[of "I" "{\<zero>}"], assumption,
        erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = a in Zleast_mL_I[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = a in val_nonzero_z[of "\<nu>\<^bsub>K (P j)\<^esub>"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> carrier K
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> \<zero>
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; \<exists>z. (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 4. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 5. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> a \<in> carrier K
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> \<zero>
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; \<exists>z. (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 4. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 5. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac h = a in Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; Ring (O\<^bsub>K P n\<^esub>); a \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> a \<in> carrier K
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> \<zero>
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; \<exists>z. (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 4. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 5. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:mem_ring_n_pd_mem_K)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> \<zero>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; \<exists>z. (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 4. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; \<exists>z. (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<in> I
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule val_LI_noninf[THEN not_sym, of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> j \<le> n
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a; \<infinity> \<noteq> LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> j \<le> n
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a; \<infinity> \<noteq> LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; 0 < n; \<zero> \<in> I; \<infinity> = LI K (\<nu>\<^bsub>K P j\<^esub>) I; Zl_mI K P I j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); a \<in> I; a \<noteq> \<zero>; ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) a; \<infinity> \<noteq> LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Zl_mI_mem_K:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n\<rbrakk>
       \<Longrightarrow> (Zl_mI K P I l) \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n\<rbrakk> \<Longrightarrow> Zl_mI K P I l \<in> carrier K
[PROOF STEP]
apply (frule value_Zl_mI[of "n" "P" "I" "l"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n; Zl_mI K P I l \<in> I \<and> (\<nu>\<^bsub>K P l\<^esub>) (Zl_mI K P I l) = LI K (\<nu>\<^bsub>K P l\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I l \<in> carrier K
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n; Zl_mI K P I l \<in> I; (\<nu>\<^bsub>K P l\<^esub>) (Zl_mI K P I l) = LI K (\<nu>\<^bsub>K P l\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I l \<in> carrier K
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n; Zl_mI K P I l \<in> I; (\<nu>\<^bsub>K P l\<^esub>) (Zl_mI K P I l) = LI K (\<nu>\<^bsub>K P l\<^esub>) I; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I l \<in> carrier K
[PROOF STEP]
apply (frule Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I" "Zl_mI K P I l"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; l \<le> n; Zl_mI K P I l \<in> I; (\<nu>\<^bsub>K P l\<^esub>) (Zl_mI K P I l) = LI K (\<nu>\<^bsub>K P l\<^esub>) I; Ring (O\<^bsub>K P n\<^esub>); Zl_mI K P I l \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Zl_mI K P I l \<in> carrier K
[PROOF STEP]
apply (simp add:mem_ring_n_pd_mem_K[of "n" "P" "Zl_mI K P I l"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_expR_memTr:"(\<forall>j\<le>n. f j \<in> carrier K)  \<longrightarrow>
                      mprod_expR K e f n \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring K \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ring K \<Longrightarrow> (\<forall>j\<le>0. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f 0 \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring K; f 0 \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f 0 \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply (simp add:mprod_expR_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring K; f 0 \<in> carrier K\<rbrakk> \<Longrightarrow> f 0^\<^bsup>K e 0\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply (cut_tac Ring.npClose[of K "f 0" "e 0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; (\<forall>j\<le>n. f j \<in> carrier K) \<longrightarrow> mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f (Suc n) \<in> carrier K
[PROOF STEP]
apply (subst Ring.mprodR_Suc, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> e \<in> {j. j \<le> Suc n} \<rightarrow> Collect ((\<le>) 0)
 2. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> f \<in> {j. j \<le> Suc n} \<rightarrow> carrier K
 3. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f n \<cdot>\<^sub>r f (Suc n)^\<^bsup>K e (Suc n)\<^esup> \<in> carrier K
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> f \<in> {j. j \<le> Suc n} \<rightarrow> carrier K
 2. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f n \<cdot>\<^sub>r f (Suc n)^\<^bsup>K e (Suc n)\<^esup> \<in> carrier K
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f n \<cdot>\<^sub>r f (Suc n)^\<^bsup>K e (Suc n)\<^esup> \<in> carrier K
[PROOF STEP]
apply (rule Ring.ring_tOp_closed[of K], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> f (Suc n)^\<^bsup>K e (Suc n)\<^esup> \<in> carrier K
[PROOF STEP]
apply (rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; mprod_expR K e f n \<in> carrier K; \<forall>j\<le>Suc n. f j \<in> carrier K\<rbrakk> \<Longrightarrow> f (Suc n) \<in> carrier K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_expR_mem:"\<forall>j \<le> n. f j \<in> carrier K \<Longrightarrow>
           mprod_expR K e f n \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>n. f j \<in> carrier K \<Longrightarrow> mprod_expR K e f n \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier K; Ring K\<rbrakk> \<Longrightarrow> mprod_expR K e f n \<in> carrier K
[PROOF STEP]
apply (cut_tac Ring.mprod_expR_memTr[of K e n f])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier K; Ring K; e \<in> {j. j \<le> n} \<rightarrow> {j. 0 \<le> j} \<and> f \<in> {j. j \<le> n} \<rightarrow> carrier K \<longrightarrow> mprod_expR K e f n \<in> carrier K\<rbrakk> \<Longrightarrow> mprod_expR K e f n \<in> carrier K
 2. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier K; Ring K\<rbrakk> \<Longrightarrow> Ring K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier K; Ring K\<rbrakk> \<Longrightarrow> Ring K
[PROOF STEP]
apply (subgoal_tac "f \<in> {j. j \<le> n} \<rightarrow> carrier K", simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_Suc:"\<lbrakk> \<forall>j\<le>(Suc n). e j \<in> Zset;
                \<forall>j \<le> (Suc n). f j \<in> (carrier K - {\<zero>})\<rbrakk> \<Longrightarrow>
 mprod_exp K e f (Suc n) = (mprod_exp K e f n) \<cdot>\<^sub>r ((f (Suc n))\<^bsub>K\<^esub>\<^bsup>(e (Suc n))\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K e f (Suc n) = mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>
[PROOF STEP]
apply (simp add:mprod_exp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_memTr:"
 (\<forall>j \<le> n. e j \<in> Zset) \<and> (\<forall>j \<le> n. f j \<in> ((carrier K) - {\<zero>})) \<longrightarrow>
       (mprod_exp K e f n) \<in> ((carrier K) - {\<zero>})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>0. e j \<in> Zset) \<and> (\<forall>j\<le>0. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f 0 \<in> carrier K - {\<zero>}
 2. \<And>n. (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>} \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f (Suc n) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp, rule impI, (erule conjE)+,
        simp add:mprod_exp_def, simp add:npowf_mem,
        simp add:field_potent_nonzero1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>} \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f (Suc n) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule impI, simp, erule conjE,
       cut_tac field_is_ring, cut_tac field_is_idom,
       erule conjE, simp add:mprod_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>mprod_exp K e f n \<in> carrier K; mprod_exp K e f n \<noteq> \<zero>; Ring K; Idomain K; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<in> carrier K \<and> mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>mprod_exp K e f n \<in> carrier K; mprod_exp K e f n \<noteq> \<zero>; Ring K; Idomain K; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>mprod_exp K e f n \<in> carrier K; mprod_exp K e f n \<noteq> \<zero>; Ring K; Idomain K; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule Ring.ring_tOp_closed[of "K"], assumption+,
        simp add:npowf_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>mprod_exp K e f n \<in> carrier K; mprod_exp K e f n \<noteq> \<zero>; Ring K; Idomain K; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule Idomain.idom_tOp_nonzeros, assumption+,
        simp add:npowf_mem, assumption,
        simp add:field_potent_nonzero1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_mem:"\<lbrakk>\<forall>j \<le> n. e j \<in> Zset; \<forall>j \<le> n. f j \<in> ((carrier K) - {\<zero>})\<rbrakk> \<Longrightarrow>  (mprod_exp K e f n) \<in> ((carrier K) - {\<zero>})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. f j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac mprod_memTr[of n e f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. f j \<in> carrier K - {\<zero>}; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mprod_mprodR:"\<lbrakk>\<forall>j \<le> n. e j \<in> Zset; \<forall>j \<le> n. 0 \<le> (e j);
 \<forall>j \<le> n. f j \<in> ((carrier K) - {\<zero>})\<rbrakk> \<Longrightarrow>
              mprod_exp K e f n = mprod_expR K (nat o e) f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K e f n = mprod_expR K (nat \<circ> e) f n
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K - {\<zero>}; Ring K\<rbrakk> \<Longrightarrow> mprod_exp K e f n = mprod_expR K (nat \<circ> e) f n
[PROOF STEP]
apply (simp add:mprod_exp_def mprod_expR_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>K,n\<^esub> (\<lambda>j. f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup>) = e\<Pi>\<^bsub>K,n\<^esub> (\<lambda>j. f j^\<^bsup>K nat (e j)\<^esup>)
[PROOF STEP]
apply (rule Ring.nprod_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup> \<in> carrier K
 2. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j^\<^bsup>K nat (e j)\<^esup> \<in> carrier K
 3. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup> = f j^\<^bsup>K nat (e j)\<^esup>
[PROOF STEP]
apply (rule allI, rule impI, simp add:npowf_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j^\<^bsup>K nat (e j)\<^esup> \<in> carrier K
 2. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup> = f j^\<^bsup>K nat (e j)\<^esup>
[PROOF STEP]
apply (rule allI, rule impI, rule Ring.npClose, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup> = f j^\<^bsup>K nat (e j)\<^esup>
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. 0 \<le> e j; \<forall>j\<le>n. f j \<in> carrier K \<and> f j \<noteq> \<zero>; Ring K; j \<le> n\<rbrakk> \<Longrightarrow> f j\<^bsub>K\<^esub>\<^bsup>e j\<^esup> = f j^\<^bsup>K nat (e j)\<^esup>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_mprod_mprodRTr:"distinct_pds K n P \<Longrightarrow>
       (\<forall>j \<le> m. e j \<in> Zset) \<and> (\<forall>j \<le> m. 0 \<le> (e j)) \<and>
       (\<forall>j \<le> m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)-{\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}) \<longrightarrow>
        mprod_exp K e f m = mprod_expR (O\<^bsub>K P n\<^esub>) (nat o e) f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> (\<forall>j\<le>m. e j \<in> Zset) \<and> (\<forall>j\<le>m. 0 \<le> e j) \<and> (\<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f m = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f m
[PROOF STEP]
apply (frule ring_n_pd[of n P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>m. e j \<in> Zset) \<and> (\<forall>j\<le>m. 0 \<le> e j) \<and> (\<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f m = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f m
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>0. e j \<in> Zset) \<and> (\<forall>j\<le>0. 0 \<le> e j) \<and> (\<forall>j\<le>0. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f 0 = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f 0
 2. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); (\<forall>j\<le>na. e j \<in> Zset) \<and> (\<forall>j\<le>na. 0 \<le> e j) \<and> (\<forall>j\<le>na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f na\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc na. e j \<in> Zset) \<and> (\<forall>j\<le>Suc na. 0 \<le> e j) \<and> (\<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f (Suc na) = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f (Suc na)
[PROOF STEP]
apply (rule impI, (erule conjE)+,
        simp add:mprod_exp_def mprod_expR_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); e 0 \<in> Zset; 0 \<le> e 0; f 0 \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f 0 \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> f 0\<^bsub>K\<^esub>\<^bsup>e 0\<^esup> = f 0^\<^bsup>O\<^bsub>K P n\<^esub> nat (e 0)\<^esup>
 2. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); (\<forall>j\<le>na. e j \<in> Zset) \<and> (\<forall>j\<le>na. 0 \<le> e j) \<and> (\<forall>j\<le>na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f na\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc na. e j \<in> Zset) \<and> (\<forall>j\<le>Suc na. 0 \<le> e j) \<and> (\<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f (Suc na) = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f (Suc na)
[PROOF STEP]
apply (erule conjE, simp add:npowf_def, simp add:ring_n_exp_K_exp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); (\<forall>j\<le>na. e j \<in> Zset) \<and> (\<forall>j\<le>na. 0 \<le> e j) \<and> (\<forall>j\<le>na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f na\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc na. e j \<in> Zset) \<and> (\<forall>j\<le>Suc na. 0 \<le> e j) \<and> (\<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}) \<longrightarrow> mprod_exp K e f (Suc na) = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f (Suc na)
[PROOF STEP]
apply (rule impI, (erule conjE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> mprod_exp K e f (Suc na) = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f (Suc na)
[PROOF STEP]
apply (subst mprod_Suc, assumption+,
        rule allI, rule impI,
        simp add:mem_ring_n_pd_mem_K,
        simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> mprod_exp K e f na \<cdot>\<^sub>r f (Suc na)\<^bsub>K\<^esub>\<^bsup>e (Suc na)\<^esup> = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f (Suc na)
[PROOF STEP]
apply (subst Ring.mprodR_Suc, assumption+,
         simp add:cmp_def,
         simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> mprod_exp K e f na \<cdot>\<^sub>r f (Suc na)\<^bsub>K\<^esub>\<^bsup>e (Suc na)\<^esup> = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup>
[PROOF STEP]
apply (simp add:ring_n_pd, simp add:npowf_def,
         simp add:ring_n_exp_K_exp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na \<cdot>\<^sub>r f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup> = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup>
[PROOF STEP]
apply (subst ring_n_tOp_K_tOp, assumption+,
        rule Ring.mprod_expR_mem, simp add:ring_n_pd,
        simp,
        simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>distinct_pds K n P; mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>na. \<lbrakk>distinct_pds K n P; mprod_exp K e f na = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na; \<forall>j\<le>Suc na. e j \<in> Zset; \<forall>j\<le>Suc na. 0 \<le> e j; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> f j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na \<cdot>\<^sub>r f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup> = mprod_expR (O\<^bsub>K P n\<^esub>) (\<lambda>a. nat (e a)) f na \<cdot>\<^sub>r f (Suc na)^\<^bsup>O\<^bsub>K P n\<^esub> nat (e (Suc na))\<^esup>
[PROOF STEP]
apply (rule Ring.npClose, simp add:ring_n_pd, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_mprod_mprodR:"\<lbrakk>distinct_pds K n P; \<forall>j \<le> m. e j \<in> Zset;
 \<forall>j \<le> m. 0 \<le> (e j); \<forall>j \<le> m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)-{\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}\<rbrakk>
 \<Longrightarrow>  mprod_exp K e f m = mprod_expR (O\<^bsub>K P n\<^esub>) (nat o e) f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; \<forall>j\<le>m. e j \<in> Zset; \<forall>j\<le>m. 0 \<le> e j; \<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}\<rbrakk> \<Longrightarrow> mprod_exp K e f m = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> e) f m
[PROOF STEP]
apply (simp add:ring_n_mprod_mprodRTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mprod_expTr:"valuation K v  \<Longrightarrow>
 (\<forall>j \<le> n. e j \<in> Zset) \<and> (\<forall>j \<le> n. f j \<in> (carrier K - {\<zero>})) \<longrightarrow>
 v (mprod_exp K e f n) =  ASum  (\<lambda>j. (e j) *\<^sub>a (v (f j))) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation K v \<Longrightarrow> (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. valuation K v \<Longrightarrow> (\<forall>j\<le>0. e j \<in> Zset) \<and> (\<forall>j\<le>0. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f 0) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) 0
 2. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) (Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. valuation K v \<Longrightarrow> e 0 \<in> Zset \<and> f 0 \<in> carrier K \<and> f 0 \<noteq> \<zero> \<longrightarrow> v (mprod_exp K e f 0) = e 0 *\<^sub>a v (f 0)
 2. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) (Suc n)
[PROOF STEP]
apply (rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; e 0 \<in> Zset; f 0 \<in> carrier K \<and> f 0 \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f 0) = e 0 *\<^sub>a v (f 0)
 2. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) (Suc n)
[PROOF STEP]
apply(simp add:mprod_exp_def val_exp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. e j \<in> Zset) \<and> (\<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) (Suc n)
[PROOF STEP]
apply (rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. e j \<in> Zset) \<and> (\<forall>j\<le>n. f j \<in> carrier K - {\<zero>}) \<longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) (Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f (Suc n)) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (subst mprod_Suc, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. f j \<in> carrier K - {\<zero>}
 2. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f n \<cdot>\<^sub>r f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (subst val_t2p[of v], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K e f n \<in> carrier K
 2. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<in> carrier K
 3. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f n) + v (f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (cut_tac n = "n" in mprod_mem[of _ e f],
        (rule allI, rule impI, simp)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> v (mprod_exp K e f n) + v (f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (simp add:npowf_mem, simp add:field_potent_nonzero1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n; \<forall>j\<le>Suc n. e j \<in> Zset; \<forall>j\<le>Suc n. f j \<in> carrier K \<and> f j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + v (f (Suc n)\<^bsub>K\<^esub>\<^bsup>e (Suc n)\<^esup>) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n + e (Suc n) *\<^sub>a v (f (Suc n))
[PROOF STEP]
apply (simp add:val_exp[THEN sym, of "v"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mprod_exp:"\<lbrakk>valuation K v; \<forall>j \<le> n. e j \<in> Zset;
       \<forall>j \<le> n. f j \<in> (carrier K - {\<zero>})\<rbrakk> \<Longrightarrow>
     v (mprod_exp K e f n) = ASum (\<lambda>j. (e j) *\<^sub>a (v (f j))) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; \<forall>j\<le>n. e j \<in> Zset; \<forall>j\<le>n. f j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> v (mprod_exp K e f n) = ASum (\<lambda>j. e j *\<^sub>a v (f j)) n
[PROOF STEP]
apply (simp add:value_mprod_expTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done