[STATEMENT]
lemma (in Corps) mI_gen_in_I:"\<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>
  (nsum K (\<lambda>k. ((Zl_mI K P I k) \<cdot>\<^sub>r
  ((mprod_exp K (\<lambda>l. (\<gamma>\<^bsub>k l\<^esub>)) (Kb\<^bsub>K n P\<^esub>) n)\<^bsub>K\<^esub>\<^bsup>(m_zmax_pdsI K n P I)\<^esup>))) n) \<in> I"
[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> \<Sigma>\<^sub>e K (\<lambda>k. Zl_mI K P I k \<cdot>\<^sub>r mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup>) n \<in> I
[PROOF STEP]
apply (cut_tac field_is_ring, 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>); Ring K; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>k. Zl_mI K P I k \<cdot>\<^sub>r mprod_exp K (K_gamma k) (Kb\<^bsub>K n P\<^esub>) n\<^bsub>K\<^esub>\<^bsup>m_zmax_pdsI K n P I\<^esup>) n \<in> I
[PROOF STEP]
apply (rule ideal_eSum_closed[of n P I n], 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>); Ring K; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 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> I
[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>); Ring K; Ring (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> I
[PROOF STEP]
apply (frule_tac j = j in value_Zl_mI[of  "n" "P" "I"], assumption+)
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<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> I
[PROOF STEP]
apply (erule conjE)
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> Zl_mI K P I j \<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> I
[PROOF STEP]
apply (thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K (P j)\<^esub>) I")
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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> I
[PROOF STEP]
apply (subgoal_tac "(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 (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; 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 (O\<^bsub>K P n\<^esub>)\<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> I
 2. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (frule_tac x = "Zl_mI K P I j" and
   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 Ring.ideal_ring_multiple1[of "(O\<^bsub>K P n\<^esub>)" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; 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 (O\<^bsub>K P n\<^esub>); Zl_mI K P I j \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> 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> I\<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> I
 2. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (frule_tac h = "Zl_mI K P I j" in
               Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; 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 (O\<^bsub>K P n\<^esub>); Zl_mI K P I j \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> 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> I; Zl_mI K P I j \<in> carrier (O\<^bsub>K P n\<^esub>)\<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> I
 2. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (simp add:ring_n_pd_tOp_K_tOp[of "n" "P"])
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (subst ring_n_pd_def)
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 (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. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<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 \<and> (\<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>))
[PROOF STEP]
apply (simp add:value_mI_genTr1)
[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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>)
[PROOF STEP]
apply (case_tac "j = ja")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j = ja\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>)
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>)
[PROOF STEP]
apply (simp add:mgenerator2Tr3_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) (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>)
[PROOF STEP]
apply (simp add:mgenerator2Tr3_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> ant (m_zmax_pdsI K n P I)
[PROOF STEP]
apply (simp add:m_zmax_pdsI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> ant (m_zmax n (m_zmax_pdsI_hom K P I) + 1)
[PROOF STEP]
apply (simp add:m_zmax_pdsI_hom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> ant (m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1)
[PROOF STEP]
apply (simp only:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> ant 0 \<le> ant (m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1)
[PROOF STEP]
apply (simp add:aless_zless)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
[PROOF STEP]
apply (subgoal_tac "\<forall>l \<le> n. (\<lambda>j. tna (AMin ((\<nu>\<^bsub>K (P j)\<^esub>) ` I))) l \<in> Zset")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (frule m_zmax_gt_each[of n "\<lambda>j. tna (AMin ((\<nu>\<^bsub>K (P j)\<^esub>) ` I))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; \<forall>j\<le>n. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I)))\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (rotate_tac -1, drule_tac a = ja in forall_spec, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I)))\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (frule_tac j = ja in val_LI_pos[of  "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> LI K (\<nu>\<^bsub>K P ja\<^esub>) I\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (cut_tac j = "tna (LI K (\<nu>\<^bsub>K (P ja)\<^esub>) I)" in ale_zle[of "0"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> LI K (\<nu>\<^bsub>K P ja\<^esub>) I; (ant 0 \<le> ant (tna (LI K (\<nu>\<^bsub>K P ja\<^esub>) I))) = (0 \<le> tna (LI K (\<nu>\<^bsub>K P ja\<^esub>) I))\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (frule_tac j = ja in val_LI_noninf[of "n" "P" "I"], assumption+,
       frule_tac j = ja in val_LI_pos[of "n" "P" "I"], assumption+,
       frule_tac a = "LI K (\<nu>\<^bsub>K (P ja)\<^esub>) I" in apos_neq_minf, simp add:ant_tna,
       simp add:ant_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> tna (LI K (\<nu>\<^bsub>K P ja\<^esub>) I); LI K (\<nu>\<^bsub>K P ja\<^esub>) I \<noteq> \<infinity>; 0 \<le> LI K (\<nu>\<^bsub>K P ja\<^esub>) I; LI K (\<nu>\<^bsub>K P ja\<^esub>) I \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (unfold LI_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> AMin (\<nu>\<^bsub>K P ja\<^esub> ` I); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (frule_tac y = "tna (AMin (\<nu>\<^bsub>K (P ja)\<^esub> ` I))" and z = "m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K (P j)\<^esub> ` I)))" in order_trans[of "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> AMin (\<nu>\<^bsub>K P ja\<^esub> ` I); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> - \<infinity>; 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I)))\<rbrakk> \<Longrightarrow> 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (rule_tac y = "m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K (P j)\<^esub> ` I)))" and
        z = "m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K (P j)\<^esub> ` I))) + 1" in order_trans[of "0"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset; tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))); 0 \<le> tna (AMin (\<nu>\<^bsub>K P ja\<^esub> ` I)); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> AMin (\<nu>\<^bsub>K P ja\<^esub> ` I); AMin (\<nu>\<^bsub>K P ja\<^esub> ` I) \<noteq> - \<infinity>; 0 \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I)))\<rbrakk> \<Longrightarrow> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) \<le> m_zmax n (\<lambda>j. tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) + 1
 2. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j ja l. \<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>); Ring K; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; Zl_mI K P I j \<in> I; ja \<le> n; j \<noteq> ja; l \<le> n\<rbrakk> \<Longrightarrow> tna (AMin (\<nu>\<^bsub>K P l\<^esub> ` I)) \<in> Zset
[PROOF STEP]
apply (simp add:Zset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) value_mI_gen1:"\<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>
                \<forall>j \<le> n.(\<nu>\<^bsub>K (P j)\<^esub>) (mIg\<^bsub>K n P I\<^esub>) = LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"
[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> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[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>); j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (simp add:mIg_def value_mI_gen)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mI_gen_in_I1:"\<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>  (mIg\<^bsub>K n P I\<^esub>) \<in> I"
[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> mIg\<^bsub> K n P I\<^esub> \<in> I
[PROOF STEP]
apply (simp add:mIg_def mI_gen_in_I)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mI_principalTr:"\<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>); x \<in> I\<rbrakk> \<Longrightarrow>
 \<forall>j \<le> n. ((\<nu>\<^bsub>K (P j)\<^esub>) (mIg\<^bsub>K n P I\<^esub>)) \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) x)"
[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>); x \<in> I\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:value_mI_gen1)
[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>); x \<in> I\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[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>); x \<in> I; j \<le> n\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (rule Zleast_LI, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mI_principal:"\<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>
                                        I = Rxa (O\<^bsub>K P n\<^esub>) (mIg\<^bsub>K n P I\<^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> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (rule equalityI)
[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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (frule_tac x = x in mI_principalTr[of "n" "P" "I"],
                 assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (frule_tac y = x in n_eq_val_eq_idealTr[of "n" "P" "mIg\<^bsub>K n P I\<^esub>"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 4. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (frule mI_gen_in_I1[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; mIg\<^bsub> K n P I\<^esub> \<in> I\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 4. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (simp add:Ring.ideal_subset)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (thin_tac "\<forall>j\<le>n. (\<nu>\<^bsub>K (P j)\<^esub>) (mIg\<^bsub> K n P I\<^esub>) \<le> (\<nu>\<^bsub>K (P j)\<^esub>) x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (frule_tac h = x in Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (frule_tac a = x in Ring.a_in_principal[of "O\<^bsub>K P n\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<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>); Ring (O\<^bsub>K P n\<^esub>); x \<in> I; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (simp add:subsetD)
[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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>) \<subseteq> I
[PROOF STEP]
apply (rule Ring.ideal_cont_Rxa[of "O\<^bsub>K P n\<^esub>" "I" "mIg\<^bsub> K n P I\<^esub>"], 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>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> I
[PROOF STEP]
apply (rule mI_gen_in_I1[of  "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) prime_n_pd_principal:"\<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow>
       (P\<^bsub>K P n\<^esub> j) = Rxa (O\<^bsub>K P n\<^esub>) (((Kb\<^bsub>K n P\<^esub>) j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (frule prime_n_pd_prime[of "n" "P" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); prime_ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (simp add:prime_ideal_def, frule conjunct1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j) \<and> 1\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<notin> P\<^bsub>K P n\<^esub> j \<and> (\<forall>x\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>y\<in>carrier (O\<^bsub>K P n\<^esub>). x \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> y \<in> P\<^bsub>K P n\<^esub> j \<longrightarrow> x \<in> P\<^bsub>K P n\<^esub> j \<or> y \<in> P\<^bsub>K P n\<^esub> j); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (fold prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); prime_ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (thin_tac "prime_ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule_tac y = x in n_eq_val_eq_idealTr[of n P "(Kb\<^bsub>K n P\<^esub>) j"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)", thin_tac "ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (\<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j))
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule Kbase_hom[of  "n" "P"], simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; ja \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule Kbase_Kronecker[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; ja \<le> n; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:Kronecker_delta_def, rule impI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; ja \<le> n; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then 1 else 0); ja = j\<rbrakk> \<Longrightarrow> 0 \<le> 1
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp only:ant_0[THEN sym], simp only:ant_1[THEN sym])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> P\<^bsub>K P n\<^esub> j; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; True; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); ja = j\<rbrakk> \<Longrightarrow> ant 0 \<le> ant 1
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp del:ant_1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 4. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:prime_n_pd_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule Kbase_Kronecker[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (thin_tac "\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K (P j)\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (case_tac "ja = j", simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; j \<le> n; ja = j\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 4. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (thin_tac "ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; j \<le> n; ja = j\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 4. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:prime_n_pd_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 4. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule_tac x = x in  mem_ring_n_pd_mem_K[of "n" "P"],
                                         assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x; x \<in> carrier K\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 4. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (case_tac "x = \<zero>\<^bsub>K\<^esub>")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x; x \<in> carrier K; x = \<zero>\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x; x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 3. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule distinct_pds_valuation2[of "j" "n" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x; x \<in> carrier K; x = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>x ja. \<lbrakk>distinct_pds K n P; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; ja = j; x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x; x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 1 \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 3. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule gt_a0_ge_1, assumption)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> \<delta>\<^bsub>ja j\<^esub> \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule_tac j = ja in distinct_pds_valuation2[of  _ "n" "P"],
         assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; ja \<le> n; ja \<noteq> j; valuation K (\<nu>\<^bsub>K P ja\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:prime_n_pd_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) {x \<in> carrier (O\<^bsub>K P n\<^esub>). 0 < (\<nu>\<^bsub>K P j\<^esub>) x}; ja \<le> n; ja \<noteq> j; valuation K (\<nu>\<^bsub>K P ja\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (thin_tac "ideal (O\<^bsub>K P n\<^esub>) {x. x \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K (P j)\<^esub>) x}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ja \<le> n; ja \<noteq> j; valuation K (\<nu>\<^bsub>K P ja\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) x
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 3. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (cut_tac h = x in Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "P\<^bsub>K P n\<^esub> j"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> Ring (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 5. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (frule_tac a = x in Ring.a_in_principal[of "O\<^bsub>K P n\<^esub>"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j; x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> Ring (O\<^bsub>K P n\<^esub>)
 3. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)
 4. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j\<rbrakk> \<Longrightarrow> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 6. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:Ring.ideal_subset, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule_tac c = x and A = "(O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x" and B = "(O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j"
       in subsetD, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); x \<in> P\<^bsub>K P n\<^esub> j; (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (simp add:Ring.a_in_principal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) j \<subseteq> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule Ring.ideal_cont_Rxa[of "O\<^bsub>K P n\<^esub>" "P\<^bsub>K P n\<^esub> j" "(Kb\<^bsub>K n P\<^esub>) j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (subst prime_n_pd_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
[PROOF STEP]
apply (frule Kbase_Kronecker[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then 1 else 0)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < 1
[PROOF STEP]
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> ant 0 < ant 1
[PROOF STEP]
apply (simp del:ant_1 add:aless_zless)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (subst ring_n_pd_def, simp add:Sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0)\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (\<forall>ja. (ja = j \<longrightarrow> 0 \<le> 1) \<and> (ja \<noteq> j \<longrightarrow> ja \<le> n \<longrightarrow> 0 \<le> ant 0))
[PROOF STEP]
apply (frule Kbase_hom[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (\<forall>ja. (ja = j \<longrightarrow> 0 \<le> 1) \<and> (ja \<noteq> j \<longrightarrow> ja \<le> n \<longrightarrow> 0 \<le> ant 0))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>ja. (ja = j \<longrightarrow> 0 \<le> 1) \<and> (ja \<noteq> j \<longrightarrow> ja \<le> n \<longrightarrow> 0 \<le> ant 0)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> (ja = j \<longrightarrow> 0 \<le> 1) \<and> (ja \<noteq> j \<longrightarrow> ja \<le> n \<longrightarrow> 0 \<le> ant 0)
[PROOF STEP]
apply (simp add:ant_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> ja = j \<longrightarrow> 0 \<le> 1
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; ja = j\<rbrakk> \<Longrightarrow> 0 \<le> 1
[PROOF STEP]
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j); \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K; ja = j\<rbrakk> \<Longrightarrow> ant 0 \<le> ant 1
[PROOF STEP]
apply (simp del:ant_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done