[STATEMENT]
lemma (in Corps) mgenerator1:"\<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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow>
((\<nu>\<^bsub>K (P j)\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n)) = ((\<nu>\<^bsub>K (P j)\<^esub>) (Zl_mI K P I j))"
[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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (case_tac "n = 0",
       frule value_Zl_mI[of "n" "P" "I" "j"], assumption+,
       frule val_LI_noninf[of "n" "P" "I" "j"], assumption+,
       frule val_LI_pos[of  "n" "P" "I" "j"], assumption+,
       frule apos_neq_minf[of "LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"],
       simp add:distinct_pds_def, erule conjE)
[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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P 0\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K 0 P\<^esub>) 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I
 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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (cut_tac representative_of_pd_valuation[of "P j"], simp+,
        simp add:mprod_exp_def,
        subst val_exp[THEN sym, of "\<nu>\<^bsub>K (P 0)\<^esub>" "(Kb\<^bsub>K 0 P\<^esub>) 0"], assumption+,
        cut_tac Kbase_hom[of "0" "P"], simp,
        simp add:distinct_pds_def,
        cut_tac Kbase_nonzero[of "0" "P"], simp+,
        simp add:distinct_pds_def)
[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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> mL K P I 0 *\<^sub>a (\<nu>\<^bsub>K P 0\<^esub>) ((Kb\<^bsub>K 0 P\<^esub>) 0) = LI 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> P j \<in> Pds
 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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (cut_tac Kbase_nonzero[of "0" "P"], simp add:distinct_pds_def)
[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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>); (Kb\<^bsub>K 0 P\<^esub>) 0 \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mL K P I 0 *\<^sub>a (\<nu>\<^bsub>K P 0\<^esub>) ((Kb\<^bsub>K 0 P\<^esub>) 0) = LI 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> distinct_pds K 0 P
 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> P j \<in> Pds
 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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (cut_tac Kbase_Kronecker[of "0" "P"], simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (5 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>); (Kb\<^bsub>K 0 P\<^esub>) 0 \<noteq> \<zero>; (\<nu>\<^bsub>K P 0\<^esub>) ((Kb\<^bsub>K 0 P\<^esub>) 0) = \<delta>\<^bsub>0 0\<^esub>\<rbrakk> \<Longrightarrow> mL K P I 0 *\<^sub>a (\<delta>\<^bsub>0 0\<^esub>) = LI 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>); (Kb\<^bsub>K 0 P\<^esub>) 0 \<noteq> \<zero>\<rbrakk> \<Longrightarrow> distinct_pds K 0 P
 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> distinct_pds K 0 P
 4. \<lbrakk>P 0 \<in> Pds; ideal (O\<^bsub>K P 0\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P 0\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> P j \<in> Pds
 5. \<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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (simp add:Kronecker_delta_def, simp add:mL_def, simp add:ant_tna)
[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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>); (Kb\<^bsub>K 0 P\<^esub>) 0 \<noteq> \<zero>\<rbrakk> \<Longrightarrow> distinct_pds K 0 P
 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I; valuation K (\<nu>\<^bsub>K P 0\<^esub>)\<rbrakk> \<Longrightarrow> distinct_pds K 0 P
 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>}; I \<noteq> carrier (O\<^bsub>K P 0\<^esub>); j = 0; n = 0; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P 0\<^esub>) I; LI K (\<nu>\<^bsub>K P 0\<^esub>) I \<noteq> - \<infinity>; Zl_mI K P I 0 \<in> I; (\<nu>\<^bsub>K P 0\<^esub>) (Zl_mI K P I 0) = LI K (\<nu>\<^bsub>K P 0\<^esub>) I\<rbrakk> \<Longrightarrow> P j \<in> Pds
 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>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (simp add:distinct_pds_def)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (cut_tac mgenerator0_2[of "n" "P" "I" "j"], simp+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> distinct_pds K n P
 2. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> ideal (O\<^bsub>K P n\<^esub>) I
 3. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 4. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> I \<noteq> carrier (O\<^bsub>K P n\<^esub>)
 5. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> j \<le> n
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> ideal (O\<^bsub>K P n\<^esub>) I
 2. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 3. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> I \<noteq> carrier (O\<^bsub>K P n\<^esub>)
 4. \<lbrakk>(\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m); ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 0 < n\<rbrakk> \<Longrightarrow> j \<le> n
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgenerator2Tr1:"\<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow>
      (\<nu>\<^bsub>K (P j)\<^esub>) (mprod_exp K (\<lambda>l. \<gamma>\<^bsub>k l\<^esub> ) (Kb\<^bsub>K n P\<^esub>) n) = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n) = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
[PROOF STEP]
apply (frule distinct_pds_valuation1[of "n" "j" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n) = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
[PROOF STEP]
apply (frule K_gamma_hom[of k n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n) = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "\<forall>j \<le> n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n) = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:value_mprod_exp[of "\<nu>\<^bsub>K (P j)\<^esub>" n "K_gamma k" "(Kb\<^bsub>K n P\<^esub>)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subgoal_tac "ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K (P j)\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n
       = ASum (\<lambda>ja. (((\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)))) n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subgoal_tac "\<forall>j \<le> n. (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) j \<in> Z\<^sub>\<infinity>")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n = (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac eSum_single[of n "\<lambda>ja. ((\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>))"  "j"], simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> n} - {j}. (\<gamma>\<^bsub>k l\<^esub>) *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>
 5. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 6. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule allI, rule impI, simp add:Kronecker_delta_def,
        rule impI, simp add:asprod_n_0 Zero_in_aug_inf, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> n} - {j}. (\<gamma>\<^bsub>k l\<^esub>) *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule ballI, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l. \<lbrakk>j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>; l \<le> n \<and> l \<noteq> j\<rbrakk> \<Longrightarrow> (\<gamma>\<^bsub>k l\<^esub>) *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:K_gamma_def, rule impI, simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n; ja \<le> n\<rbrakk> \<Longrightarrow> (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>ja ja\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:Kronecker_delta_def, simp add:K_gamma_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. (if k = j then 0 else 1) \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (if k = ja then 0 else 1) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (if k = ja then 0 else 1) *\<^sub>a (if j = ja then 1 else 0)) n; ja \<le> n\<rbrakk> \<Longrightarrow> (k = ja \<longrightarrow> ant 0 \<in> Z\<^sub>\<infinity>) \<and> (k \<noteq> ja \<longrightarrow> 1 \<in> Z\<^sub>\<infinity>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:ant_0 Zero_in_aug_inf)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. (if k = j then 0 else 1) \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. (if k = ja then 0 else 1) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (if k = ja then 0 else 1) *\<^sub>a (if j = ja then 1 else 0)) n; ja \<le> n\<rbrakk> \<Longrightarrow> k \<noteq> ja \<longrightarrow> 1 \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac z_in_aug_inf[of 1], simp add:ant_1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja)) n = ASum (\<lambda>ja. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule ASum_eq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ja \<le> n\<rbrakk> \<Longrightarrow> (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:K_gamma_def, simp add:Zero_in_aug_inf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. (if k = j then 0 else 1) \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ja \<le> n\<rbrakk> \<Longrightarrow> k \<noteq> ja \<longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 4. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule impI, rule value_in_aug_inf, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 3. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:K_gamma_def Zero_in_aug_inf Kdelta_in_Zinf1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; ja \<le> n\<rbrakk> \<Longrightarrow> (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) ja) = (\<gamma>\<^bsub>k ja\<^esub>) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
 2. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:Kbase_Kronecker[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule Kbase_hom1, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgenerator2Tr2:"\<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow>
     (\<nu>\<^bsub>K (P j)\<^esub>) ((mprod_exp K (\<lambda>l. \<gamma>\<^bsub>k l\<^esub> ) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>m\<^esup>)= ant (m * (\<gamma>\<^bsub>k j\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (frule K_gamma_hom[of k n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (frule Kbase_hom1[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (frule mprod_mem[of n "K_gamma k" "Kb\<^bsub>K n P\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (frule distinct_pds_valuation1[of "n" "j" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (simp add:val_exp[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> m *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (simp add:mgenerator2Tr1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> m *\<^sub>a ((\<gamma>\<^bsub>k j\<^esub>) *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)) = ant (m * (\<gamma>\<^bsub>k j\<^esub>))
[PROOF STEP]
apply (simp add:K_gamma_def Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. (if k = j then 0 else 1) \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> k = j \<longrightarrow> m *\<^sub>a ant 0 = ant 0
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; distinct_pds K n P; \<forall>j\<le>n. (if k = j then 0 else 1) \<in> Zset; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>); mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>; k = j\<rbrakk> \<Longrightarrow> m *\<^sub>a ant 0 = ant 0
[PROOF STEP]
apply (simp add:asprod_def a_z_z)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgenerator2Tr3_1:"\<lbrakk>0 < n; j \<le> n; k \<le> n; j = k;
      distinct_pds K n P\<rbrakk> \<Longrightarrow>
          (\<nu>\<^bsub>K (P j)\<^esub>) ((mprod_exp K (\<lambda>l. (\<gamma>\<^bsub>k l\<^esub>)) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; j = k; distinct_pds K n P\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = 0
[PROOF STEP]
apply (simp add:mgenerator2Tr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; k \<le> n; j = k; distinct_pds K n P\<rbrakk> \<Longrightarrow> m = 0 \<or> \<gamma>\<^bsub>k k\<^esub> = 0
[PROOF STEP]
apply (simp add:K_gamma_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgenerator2Tr3_2:"\<lbrakk>0 < n; j \<le> n; k \<le> n; j \<noteq> k;
      distinct_pds K n P\<rbrakk> \<Longrightarrow>
      (\<nu>\<^bsub>K (P j)\<^esub>) ((mprod_exp K (\<lambda>l. (\<gamma>\<^bsub>k l\<^esub>)) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; k \<le> n; j \<noteq> k; distinct_pds K n P\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m\<^esup>) = ant m
[PROOF STEP]
apply (simp add:mgenerator2Tr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> n; k \<le> n; j \<noteq> k; distinct_pds K n P\<rbrakk> \<Longrightarrow> m = 0 \<or> \<gamma>\<^bsub>k j\<^esub> = 1
[PROOF STEP]
apply (simp add:K_gamma_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgeneratorTr4:"\<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
      I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow>
       mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier (O\<^bsub>K P n\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (subst ring_n_pd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (simp add:Sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n))
[PROOF STEP]
apply (frule mL_hom[of  "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n))
[PROOF STEP]
apply (frule mprod_mem[of n "mL K P I" "Kb\<^bsub>K n P\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n))
[PROOF STEP]
apply (rule Kbase_hom1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n))
[PROOF STEP]
apply (simp add:mprod_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n)
[PROOF STEP]
apply (simp add:mgenerator1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (simp add:value_Zl_mI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. mL K P I j \<in> Zset; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (simp add:val_LI_pos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_Zl_mI_pos:"\<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
     I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; l \<le> n\<rbrakk> \<Longrightarrow>
     0 \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) (Zl_mI K P I l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; l \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (frule value_Zl_mI[of "n" "P" "I" "l"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[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>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (thin_tac "ideal (O\<^bsub>K P n\<^esub>) I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (thin_tac "I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (thin_tac "I \<noteq> carrier (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; j \<le> n; 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> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; j \<le> n; 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; Zl_mI K P I l \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I l)
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mI_genTr1:"\<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
 I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow>
 (mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>(m_zmax_pdsI K n P I)\<^esup> \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (frule K_gamma_hom[of "j" "n"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (frule mprod_mem[of n "K_gamma j" "Kb\<^bsub>K n P\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (rule Kbase_hom1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (rule npowf_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mI_genTr1_0:"\<lbrakk>0 < n; distinct_pds K n P;
 ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk>
 \<Longrightarrow> (mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n) \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K
[PROOF STEP]
apply (frule K_gamma_hom[of "j" "n"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K
[PROOF STEP]
apply (frule mprod_mem[of n "K_gamma j" "Kb\<^bsub>K n P\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K
[PROOF STEP]
apply (rule Kbase_hom1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mI_genTr2:"\<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
 I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow>
 (mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>(m_zmax_pdsI K n P I)\<^esup> \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (frule K_gamma_hom[of "j" "n"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (frule mprod_mem[of n "K_gamma j" "Kb\<^bsub>K n P\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule Kbase_hom1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K \<and> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; \<forall>ja\<le>n. \<gamma>\<^bsub>j ja\<^esub> \<in> Zset; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier K; mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n \<noteq> \<zero>\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (simp add: field_potent_nonzero1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mI_genTr3:"\<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
 I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow>
 (Zl_mI K P I j) \<cdot>\<^sub>r ((mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>(m_zmax_pdsI K n P I)\<^esup>)
  \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<cdot>\<^sub>r mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; Ring K\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<cdot>\<^sub>r mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (rule Ring.ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; Ring K\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<in> carrier K
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; Ring K\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (simp add:Zl_mI_mem_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n; Ring K\<rbrakk> \<Longrightarrow> mprod_exp K (K_gamma j) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup> \<in> carrier K
[PROOF STEP]
apply (simp add:value_mI_genTr1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done