[STATEMENT]
lemma (in Corps) mgenerator0_1:"\<lbrakk>distinct_pds K (Suc n) P;
 ideal (O\<^bsub>K P (Suc n)\<^esub>) I; I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P (Suc n)\<^esub>)\<^esub>};
 I \<noteq> carrier (O\<^bsub>K P (Suc n)\<^esub>); j \<le> (Suc n)\<rbrakk> \<Longrightarrow>
((\<nu>\<^bsub>K (P j)\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K (Suc n) P\<^esub>) (Suc 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 (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (frule distinct_pds_valuation[of j n P], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (frule mL_hom[of "Suc n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (frule Kbase_hom1[of "Suc n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (frule value_mprod_exp[of "\<nu>\<^bsub>K (P j)\<^esub>" "Suc n" "mL K P I"
           "Kb\<^bsub>K (Suc n) P\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K - {\<zero>}; (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (simp del:ASum_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n)\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K (Suc n) P\<^esub>) (Suc n)) =
     ASum (\<lambda>ja. (mL K P I ja) *\<^sub>a (\<nu>\<^bsub>K (P j)\<^esub>) ((Kb\<^bsub>K (Suc n) P\<^esub>) ja)) (Suc n)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
[PROOF STEP]
apply (subgoal_tac "ASum (\<lambda>ja. (mL K P I ja) *\<^sub>a
      ((\<nu>\<^bsub>K (P j)\<^esub>) ((Kb\<^bsub>K (Suc n) P\<^esub>) ja))) (Suc n) =
                ASum (\<lambda>ja. (mL K P I ja) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp del:ASum_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (subgoal_tac "\<forall>h \<le> (Suc n). (\<lambda>ja. (mL K P I ja) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) h \<in> Z\<^sub>\<infinity>")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (cut_tac eSum_single[of "Suc n" "\<lambda>ja. (mL K P I ja) *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)" "j"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n) = mL K P I j *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = mL K P I j *\<^sub>a (\<delta>\<^bsub>j j\<^esub>); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n + mL K P I (Suc n) *\<^sub>a (\<delta>\<^bsub>j Suc n\<^esub>) = mL K P I j *\<^sub>a (\<delta>\<^bsub>j j\<^esub>)\<rbrakk> \<Longrightarrow> mL K P I j *\<^sub>a (\<delta>\<^bsub>j j\<^esub>) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:Kronecker_delta_def asprod_n_0)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (mL K P I j); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (mL K P I j)\<rbrakk> \<Longrightarrow> ant (mL K P I j) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rotate_tac -1, drule not_sym)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (mL K P I j); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (mL K P I j); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I\<rbrakk> \<Longrightarrow> ant (mL K P I j) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:mL_def[of "K" "P" "I" "j"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I\<rbrakk> \<Longrightarrow> ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (frule val_LI_noninf[of "Suc n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I\<rbrakk> \<Longrightarrow> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}
 2. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I\<rbrakk> \<Longrightarrow> j \<le> Suc n
 3. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 7. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 8. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rule not_sym, simp, simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (frule val_LI_pos[of "Suc n" "P" "I" "j"], assumption+,
       rotate_tac -2, frule not_sym, simp, simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (frule apos_neq_minf[of "LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> ant (tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:ant_tna)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0) = LI K (\<nu>\<^bsub>K P j\<^esub>) I; distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = LI K (\<nu>\<^bsub>K P j\<^esub>) I; \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>} \<noteq> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 6. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:value_Zl_mI[of "Suc n" "P" "I" "j"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ja. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>; ja \<le> Suc n\<rbrakk> \<Longrightarrow> mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> j \<le> Suc n
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 4. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 5. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:Kdelta_in_Zinf, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> \<forall>l\<in>{h. h \<le> Suc n} - {j}. mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rule ballI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) n + mL K P I (Suc n) *\<^sub>a (\<delta>\<^bsub>j Suc n\<^esub>); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>; l \<le> Suc n \<and> l \<noteq> j\<rbrakk> \<Longrightarrow> mL K P I l *\<^sub>a (\<delta>\<^bsub>j l\<^esub>) = 0
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:Kronecker_delta_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) n + mL K P I (Suc n) *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) (Suc n)) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (if j = ja then 1 else 0)) n + mL K P I (Suc n) *\<^sub>a (if j = Suc n then 1 else 0); \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (if j = h then 1 else 0) \<in> Z\<^sub>\<infinity>; l \<le> Suc n; l \<noteq> j\<rbrakk> \<Longrightarrow> mL K P I l *\<^sub>a 0 = 0
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 3. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:asprod_n_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>h\<le>Suc n. mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n); h \<le> Suc n\<rbrakk> \<Longrightarrow> mL K P I h *\<^sub>a (\<delta>\<^bsub>j h\<^esub>) \<in> Z\<^sub>\<infinity>
 2. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (simp add:Kdelta_in_Zinf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (frule  Kbase_Kronecker[of "Suc n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>Suc n. \<forall>l\<le>Suc n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja)) (Suc n) = ASum (\<lambda>ja. mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)) (Suc n)
[PROOF STEP]
apply (rule ASum_eq,
        rule allI, rule impI,
        simp add:Kdelta_in_Zinf,
        rule allI, rule impI,
        simp add:Kdelta_in_Zinf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>Suc n. \<forall>l\<le>Suc n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja) = mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>distinct_pds K (Suc n) P; ideal (O\<^bsub>K P Suc n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P Suc n\<^esub>); j \<le> Suc n; valuation K (\<nu>\<^bsub>K P j\<^esub>); \<forall>j\<le>Suc n. mL K P I j \<in> Zset; \<forall>j\<le>Suc n. (Kb\<^bsub>K Suc n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K Suc n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>Suc n. \<forall>l\<le>Suc n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>; ja \<le> Suc n\<rbrakk> \<Longrightarrow> mL K P I ja *\<^sub>a (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K Suc n P\<^esub>) ja) = mL K P I ja *\<^sub>a (\<delta>\<^bsub>j ja\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mgenerator0_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\<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>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> (\<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_1[of  "n - Suc 0" "P" "I" "j"])
[PROOF STATE]
proof (prove)
goal (6 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; (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K Suc (n - Suc 0) P\<^esub>) (Suc (n - Suc 0))) = (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j)\<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)
 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\<rbrakk> \<Longrightarrow> distinct_pds K (Suc (n - Suc 0)) P
 3. \<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> ideal (O\<^bsub>K P Suc (n - Suc 0)\<^esub>) I
 4. \<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> I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P Suc (n - Suc 0)\<^esub>\<^esub>}
 5. \<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> I \<noteq> carrier (O\<^bsub>K P Suc (n - Suc 0)\<^esub>)
 6. \<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> j \<le> Suc (n - Suc 0)
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done