[STATEMENT]
lemma (in Corps) mI_vals_LB:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow>
       ((\<nu>\<^bsub>K (P j)\<^esub>) `I) \<subseteq> LBset (ant 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; x \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (simp add:image_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (frule_tac h = xa in Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; Ring (O\<^bsub>K P n\<^esub>); xa \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (thin_tac "ideal (O\<^bsub>K P n\<^esub>) I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; Ring (O\<^bsub>K P n\<^esub>); xa \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; xa \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> LBset (ant 0)
[PROOF STEP]
apply (simp add: ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; xa \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) xa)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) xa \<in> LBset (ant 0)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; xa \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) xa\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) xa \<in> LBset (ant 0)
[PROOF STEP]
apply (drule_tac a = j in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>distinct_pds K n P; j \<le> n; xa \<in> I; x = (\<nu>\<^bsub>K P j\<^esub>) xa; xa \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) xa\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) xa \<in> LBset (ant 0)
[PROOF STEP]
apply (simp add:LBset_def ant_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mL_hom:"\<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>)\<rbrakk> \<Longrightarrow>
      \<forall>j \<le> n. mL K P I j \<in> Zset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. mL K P I j \<in> Zset
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> mL K P I j \<in> Zset
[PROOF STEP]
apply (simp add:mL_def LI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> tna (AMin (\<nu>\<^bsub>K P j\<^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) ex_Zleast_in_mI:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk>
      \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K (P j)\<^esub>) x = LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac j = j in mI_vals_nonempty[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac j = j in mI_vals_LB[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac A = "(\<nu>\<^bsub>K (P j)\<^esub>) ` I" and z = 0 in AMin_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (simp add:LI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = AMin (\<nu>\<^bsub>K P j\<^esub> ` I)
[PROOF STEP]
apply (thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) ` I \<subseteq> LBset (ant 0)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {}; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = AMin (\<nu>\<^bsub>K P j\<^esub> ` I)
[PROOF STEP]
apply (simp add:image_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {}; x \<in> I; AMin {y. \<exists>x\<in>I. y = (\<nu>\<^bsub>K P j\<^esub>) x} = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = AMin {y. \<exists>x\<in>I. y = (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {}; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x = AMin {y. \<exists>x\<in>I. y = (\<nu>\<^bsub>K P j\<^esub>) x}\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = AMin {y. \<exists>x\<in>I. y = (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) val_LI_pos:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
       I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac j = j in mI_vals_nonempty[of n P I], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac j = j in mI_vals_LB[of n P I], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule_tac A = "(\<nu>\<^bsub>K (P j)\<^esub>) ` I" and z = 0 in AMin_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (simp add:LI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I\<rbrakk> \<Longrightarrow> 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I)
[PROOF STEP]
apply (frule subsetD[of "(\<nu>\<^bsub>K (P j)\<^esub>) ` I" "LBset (ant 0)" "AMin ((\<nu>\<^bsub>K (P j)\<^esub>) ` I)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> LBset (ant 0)\<rbrakk> \<Longrightarrow> 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I)
[PROOF STEP]
apply (simp add:LBset_def ant_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) val_LI_noninf:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
       I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K (P j)\<^esub>) I \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule_tac j = j in mI_vals_nonempty[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule_tac j = j in mI_vals_LB[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule_tac A = "(\<nu>\<^bsub>K (P j)\<^esub>) ` I" and z = 0 in AMin, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) ` I \<subseteq> LBset (ant 0)",
        thin_tac "(\<nu>\<^bsub>K (P j)\<^esub> ) ` I \<noteq> {}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule Ring.ideal_zero[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x); Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (erule conjE, simp add:LI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>
[PROOF STEP]
apply (frule singleton_sub[of "\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>" "I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>} \<subseteq> I\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>
[PROOF STEP]
apply (frule sets_not_eq[of "I" "{\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}"],
        assumption+, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>} \<subseteq> I; a \<in> I; a \<notin> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>
[PROOF STEP]
apply (subgoal_tac "\<exists>x\<in>I. AMin ((\<nu>\<^bsub>K (P j)\<^esub>) ` I) = (\<nu>\<^bsub>K (P j)\<^esub>) x",
        erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>; x \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; \<forall>xa\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) xa; a \<in> I; a \<noteq> \<zero>; x \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (drule_tac x = a in bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (thin_tac "AMin ((\<nu>\<^bsub>K (P j)\<^esub>) ` I) = (\<nu>\<^bsub>K (P j)\<^esub>) x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule_tac h = a in Ring.ideal_subset[of "O\<^bsub>K P n\<^esub>" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule_tac x = a in mem_ring_n_pd_mem_K[of n P], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:distinct_pds_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (cut_tac representative_of_pd_valuation[of "P j"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
 2. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> P j \<in> Pds
 3. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> P j \<in> Pds
 2. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
 3. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x; a \<in> I; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) = (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) a; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
[PROOF STEP]
apply (frule_tac x = a in val_nonzero_z[of "\<nu>\<^bsub>K (P j)\<^esub>"], assumption+,
        erule exE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x z. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> ant z; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; valuation K (\<nu>\<^bsub>K P j\<^esub>); (\<nu>\<^bsub>K P j\<^esub>) a = ant z\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
[PROOF STEP]
apply (thin_tac "\<forall>l \<le> n. \<forall>m \<le> n. l \<noteq> m \<longrightarrow> P l \<noteq> P m",
        thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) a = ant z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x z. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<le> ant z; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x z. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; \<infinity> \<le> ant z; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; valuation K (\<nu>\<^bsub>K P j\<^esub>); (\<nu>\<^bsub>K P j\<^esub>) x = \<infinity>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac x = "ant z" in inf_ge_any)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x z. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; \<infinity> \<le> ant z; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; valuation K (\<nu>\<^bsub>K P j\<^esub>); (\<nu>\<^bsub>K P j\<^esub>) x = \<infinity>; ant z \<le> \<infinity>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = "ant z" in ale_antisym[of _ "\<infinity>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x z. \<lbrakk>ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero> \<in> I; a \<in> I; a \<noteq> \<zero>; x \<in> I; \<infinity> \<le> ant z; a \<in> carrier (O\<^bsub>K P n\<^esub>); a \<in> carrier K; \<forall>j\<le>n. P j \<in> Pds; valuation K (\<nu>\<^bsub>K P j\<^esub>); (\<nu>\<^bsub>K P j\<^esub>) x = \<infinity>; ant z \<le> \<infinity>; ant z = \<infinity>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Zleast_in_mI_pos:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
       I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> mL K P I j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> mL K P I j
[PROOF STEP]
apply (simp add:mL_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)
[PROOF STEP]
apply (frule ex_Zleast_in_mI[of "n" "P" "I" "j"], assumption+,
       erule bexE, frule sym, thin_tac "(\<nu>\<^bsub>K (P j)\<^esub>) x = LI K (\<nu>\<^bsub>K (P j)\<^esub>) I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> tna (LI K (\<nu>\<^bsub>K P j\<^esub>) I)
[PROOF STEP]
apply (subgoal_tac "LI K (\<nu>\<^bsub>K (P j)\<^esub>) I \<noteq> \<infinity>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (thin_tac "LI K (\<nu>\<^bsub>K (P j)\<^esub>) I = (\<nu>\<^bsub>K (P j)\<^esub>) x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[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>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; Ring (O\<^bsub>K P n\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (thin_tac "ideal (O\<^bsub>K P n\<^esub>) I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; Ring (O\<^bsub>K P n\<^esub>); x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[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; I \<noteq> {\<zero>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x)\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; I \<noteq> {\<zero>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct_pds K n P; I \<noteq> {\<zero>}; j \<le> n; x \<in> I; (\<nu>\<^bsub>K P j\<^esub>) x \<noteq> \<infinity>; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> tna ((\<nu>\<^bsub>K P j\<^esub>) x)
 2. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (simp add:apos_tna_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; j \<le> n; x \<in> I; LI K (\<nu>\<^bsub>K P j\<^esub>) I = (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>
[PROOF STEP]
apply (rule val_LI_noninf, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Zleast_mL_I:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n;
   I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; x \<in> I\<rbrakk> \<Longrightarrow> ant (mL K P I j) \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I\<rbrakk> \<Longrightarrow> ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule val_LI_pos[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule apos_neq_minf[of "LI K (\<nu>\<^bsub>K (P j)\<^esub>) I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> - \<infinity>\<rbrakk> \<Longrightarrow> ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule val_LI_noninf[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> LI K (\<nu>\<^bsub>K P j\<^esub>) I; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> - \<infinity>; LI K (\<nu>\<^bsub>K P j\<^esub>) I \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> ant (mL K P I j) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:mL_def LI_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> ant (tna (AMin (\<nu>\<^bsub>K P j\<^esub> ` I))) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:ant_tna)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule Zleast_in_mI_pos[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule mI_vals_nonempty[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule mI_vals_LB[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule AMin[of "(\<nu>\<^bsub>K (P j)\<^esub>) `I" "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x)\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule Zleast_in_mI_pos[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; 0 \<le> AMin (\<nu>\<^bsub>K P j\<^esub> ` I); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> - \<infinity>; AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<noteq> \<infinity>; 0 \<le> mL K P I j; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x; 0 \<le> mL K P I j\<rbrakk> \<Longrightarrow> AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:mL_def LI_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Zleast_LI:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n;
   I \<noteq> {\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>}; x \<in> I\<rbrakk> \<Longrightarrow> (LI K (\<nu>\<^bsub>K (P j)\<^esub>) I) \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule mI_vals_nonempty[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule mI_vals_LB[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (frule AMin[of "(\<nu>\<^bsub>K (P j)\<^esub>) `I" "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I \<and> (\<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x)\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; x \<in> I; \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}; \<nu>\<^bsub>K P j\<^esub> ` I \<subseteq> LBset (ant 0); AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<in> \<nu>\<^bsub>K P j\<^esub> ` I; \<forall>x\<in>\<nu>\<^bsub>K P j\<^esub> ` I. AMin (\<nu>\<^bsub>K P j\<^esub> ` I) \<le> x\<rbrakk> \<Longrightarrow> LI K (\<nu>\<^bsub>K P j\<^esub>) I \<le> (\<nu>\<^bsub>K P j\<^esub>) x
[PROOF STEP]
apply (simp add:LI_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mpdiv_vals_nonequiv:"distinct_pds K n P \<Longrightarrow>
             vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K (P j)\<^esub>) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (simp add:vals_nonequiv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> valuations K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct_pds K n P \<Longrightarrow> valuations K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>)
 2. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. \<forall>l\<le>n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (simp add:valuations_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
 2. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. \<forall>l\<le>n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
 2. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. \<forall>l\<le>n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (rule representative_of_pd_valuation,
        simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. \<forall>l\<le>n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply  ((rule allI, rule impI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>distinct_pds K n P; j \<le> n; l \<le> n; j \<noteq> l\<rbrakk> \<Longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (simp add:distinct_pds_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>j \<le> n; l \<le> n; j \<noteq> l; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (rotate_tac 4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; j \<le> n; l \<le> n; j \<noteq> l; \<forall>j\<le>n. P j \<in> Pds\<rbrakk> \<Longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (
        drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>j \<le> n; l \<le> n; j \<noteq> l; \<forall>j\<le>n. P j \<in> Pds; \<forall>m\<le>n. j \<noteq> m \<longrightarrow> P j \<noteq> P m\<rbrakk> \<Longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (rotate_tac -1,
        drule_tac a = l in forall_spec, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>j \<le> n; l \<le> n; j \<noteq> l; \<forall>j\<le>n. P j \<in> Pds; P j \<noteq> P l\<rbrakk> \<Longrightarrow> \<not> v_equiv K (\<nu>\<^bsub>K P j\<^esub>) (\<nu>\<^bsub>K P l\<^esub>)
[PROOF STEP]
apply (simp add:distinct_p_divisors)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) KbaseTr:"distinct_pds K n P \<Longrightarrow>  \<exists>f. KbaseP K P n f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<exists>f. KbaseP K P n f
[PROOF STEP]
apply (simp add: KbaseP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (frule mpdiv_vals_nonequiv[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (case_tac "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n = 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (simp add:vals_nonequiv_def valuations_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K 0 P; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (frule n_val_n_val1[of "P 0"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (frule n_val_surj[of "\<nu>\<^bsub>K (P 0)\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; \<exists>x\<in>carrier K. n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (subgoal_tac " ((\<lambda>j\<in>{0::nat}. x) (0::nat)) \<in> carrier K \<and>
         (\<nu>\<^bsub>K (P 0)\<^esub>) ((\<lambda>j\<in>{0::nat}. x) (0::nat)) = (\<delta>\<^bsub>0 0\<^esub>)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1; (\<lambda>j\<in>{0}. x) 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) ((\<lambda>j\<in>{0}. x) 0) = \<delta>\<^bsub>0 0\<^esub>\<rbrakk> \<Longrightarrow> \<exists>f. f 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) (f 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{0}. x) 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) ((\<lambda>j\<in>{0}. x) 0) = \<delta>\<^bsub>0 0\<^esub>
 3. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{0}. x) 0 \<in> carrier K \<and> (\<nu>\<^bsub>K P 0\<^esub>) ((\<lambda>j\<in>{0}. x) 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{0}. x) 0 \<in> carrier K
 2. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P 0\<^esub>) ((\<lambda>j\<in>{0}. x) 0) = \<delta>\<^bsub>0 0\<^esub>
 3. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>P 0 \<in> Pds; valuation K (\<nu>\<^bsub>K P 0\<^esub>); n = 0; n_val K (\<nu>\<^bsub>K P 0\<^esub>) = \<nu>\<^bsub>K P 0\<^esub>; x \<in> carrier K; n_val K (\<nu>\<^bsub>K P 0\<^esub>) x = 1\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P 0\<^esub>) ((\<lambda>j\<in>{0}. x) 0) = \<delta>\<^bsub>0 0\<^esub>
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
[PROOF STEP]
apply (cut_tac Approximation1_5[of "n - Suc 0" "\<lambda>j. \<nu>\<^bsub>K (P j)\<^esub>"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0; \<exists>x. (\<forall>j\<le>Suc (n - Suc 0). x j \<in> carrier K) \<and> (\<forall>i\<le>Suc (n - Suc 0). \<forall>j\<le>Suc (n - Suc 0). (\<nu>\<^bsub>K P i\<^esub>) (x j) = \<delta>\<^bsub>i j\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>f. (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (f l) = \<delta>\<^bsub>j l\<^esub>)
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc (n - Suc 0)) (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>)
 3. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc (n - Suc 0). n_val K (\<nu>\<^bsub>K P j\<^esub>) = \<nu>\<^bsub>K P j\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc (n - Suc 0)) (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>)
 2. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); n \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc (n - Suc 0). n_val K (\<nu>\<^bsub>K P j\<^esub>) = \<nu>\<^bsub>K P j\<^esub>
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); 0 < n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. n_val K (\<nu>\<^bsub>K P j\<^esub>) = \<nu>\<^bsub>K P j\<^esub>
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); 0 < n; j \<le> n\<rbrakk> \<Longrightarrow> n_val K (\<nu>\<^bsub>K P j\<^esub>) = \<nu>\<^bsub>K P j\<^esub>
[PROOF STEP]
apply (rule n_val_n_val1 )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; vals_nonequiv K n (\<lambda>j. \<nu>\<^bsub>K P j\<^esub>); 0 < n; j \<le> n\<rbrakk> \<Longrightarrow> P j \<in> Pds
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Kbase_hom:"distinct_pds K n P \<Longrightarrow>
                       \<forall>j \<le> n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K
[PROOF STEP]
apply (frule KbaseTr1[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; KbaseP K P n (Kb\<^bsub>K n P\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K
[PROOF STEP]
apply (simp add:KbaseP_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Kbase_Kronecker:"distinct_pds K n P \<Longrightarrow>
      \<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 (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<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 STEP]
apply (frule KbaseTr1[of n P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; KbaseP K P n (Kb\<^bsub>K n P\<^esub>)\<rbrakk> \<Longrightarrow> \<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 STEP]
apply (simp add:KbaseP_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Kbase_nonzero:"distinct_pds K n P \<Longrightarrow>
                        \<forall>j \<le> n. (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
[PROOF STEP]
apply (frule Kbase_Kronecker[of n P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<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> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
[PROOF STEP]
apply (subgoal_tac "(\<nu>\<^bsub>K (P j)\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<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>; (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[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 (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = 1\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = 1; (Kb\<^bsub>K n P\<^esub>) j = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = 1; (Kb\<^bsub>K n P\<^esub>) j = \<zero>\<rbrakk> \<Longrightarrow> P j \<in> Pds
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = 1; (Kb\<^bsub>K n P\<^esub>) j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> False
 3. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) \<zero> = 1; (Kb\<^bsub>K n P\<^esub>) j = \<zero>; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> False
 2. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply (simp only:value_of_zero, simp only:ant_1[THEN sym],
        frule sym, thin_tac " \<infinity> = ant 1", simp del:ant_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; j \<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 j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j) = \<delta>\<^bsub>j j\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Kbase_hom1:"distinct_pds K n P \<Longrightarrow>
                    \<forall>j \<le> n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K - {\<zero>}
[PROOF STEP]
by(simp add:Kbase_nonzero Kbase_hom)


[STATEMENT]
lemma (in Corps) value_Zl_mI:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk>
 \<Longrightarrow>  (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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> 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
[PROOF STEP]
apply (subgoal_tac "\<exists>x. (x \<in> I \<and> ((\<nu>\<^bsub>K (P j)\<^esub>) x = LI K (\<nu>\<^bsub>K (P j)\<^esub>) I))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> 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
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (subst Zl_mI_def)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> (SOME x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I) \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) (SOME x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I) = LI K (\<nu>\<^bsub>K P j\<^esub>) I
 2. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (rule someI2_ex, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (frule ex_Zleast_in_mI[of "n" "P" "I" "j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; j \<le> n; \<exists>x\<in>I. (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> (\<nu>\<^bsub>K P j\<^esub>) x = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (erule bexE, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done