[STATEMENT]
lemma (in Corps) prime_n_pd_prime:"\<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow>
              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\<rbrakk> \<Longrightarrow> prime_ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)
[PROOF STEP]
apply (subst prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> ideal (O\<^bsub>K P n\<^esub>) (P\<^bsub>K P n\<^esub> j)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:ideal_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> O\<^bsub>K P n\<^esub> +> P\<^bsub>K P n\<^esub> j \<and> (\<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> O\<^bsub>K P n\<^esub> +> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule aGroup.asubg_test)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> aGroup (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<subseteq> carrier (O\<^bsub>K P n\<^esub>)
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<noteq> {}
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 6. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"], simp add:Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<subseteq> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<noteq> {}
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule subsetI, simp add:prime_n_pd_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<noteq> {}
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (subgoal_tac "\<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> \<in> P\<^bsub>K P n\<^esub> j")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> P\<^bsub>K P n\<^esub> j \<noteq> {}
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<zero> \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:prime_n_pd_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add: ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) \<zero>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac field_is_ring, simp add:Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) \<zero>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ja. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K; ja \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac P = "P ja" in representative_of_pd_valuation,
        simp add:distinct_pds_def, simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) \<zero>
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation,
        simp add:distinct_pds_def, simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n; Ring K; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 < \<infinity>
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>a\<in>P\<^bsub>K P n\<^esub> j. \<forall>b\<in>P\<^bsub>K P n\<^esub> j. a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> P\<^bsub>K P n\<^esub> j; b \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:prime_n_pd_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) b\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule ring_n_pd [of "n" "P"], frule Ring.ring_is_ag[of "O\<^bsub>K P n\<^esub>"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; Ring (O\<^bsub>K P n\<^esub>); aGroup (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule_tac x = b in aGroup.ag_mOp_closed[of "O\<^bsub>K P n\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; Ring (O\<^bsub>K P n\<^esub>); aGroup (O\<^bsub>K P n\<^esub>); -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>) \<and> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; Ring (O\<^bsub>K P n\<^esub>); aGroup (O\<^bsub>K P n\<^esub>); -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; aGroup (O\<^bsub>K P n\<^esub>); -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (thin_tac "aGroup (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier (O\<^bsub>K P n\<^esub>); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> -\<^sub>a\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; a \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a); 0 < (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b); 0 < (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b))\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac v = "\<nu>\<^bsub>K (P j)\<^esub>" and x = a and y = "-\<^sub>a b" in
        amin_le_plus)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
 2. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> a \<in> carrier K
 3. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a b \<in> carrier K
 4. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 6. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule_tac P = "P j" in representative_of_pd_valuation,
        simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> a \<in> carrier K
 2. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a b \<in> carrier K
 3. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 5. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> P j \<in> Pds
 2. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b); valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b); valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) a" and y = "(\<nu>\<^bsub>K (P j)\<^esub>) (-\<^sub>a b)" in
         amin_gt[of "0"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b); valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)
 2. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b); valuation K (\<nu>\<^bsub>K P j\<^esub>); 0 < amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b))\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 4. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:val_minus_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>distinct_pds K n P; j \<le> n; 0 < (\<nu>\<^bsub>K P j\<^esub>) a; 0 < (\<nu>\<^bsub>K P j\<^esub>) b; a \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) a; b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) b; -\<^sub>a b \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b); amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b); valuation K (\<nu>\<^bsub>K P j\<^esub>); 0 < amin ((\<nu>\<^bsub>K P j\<^esub>) a) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a b))\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) (a \<plusminus> -\<^sub>a b)
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule_tac y = "amin ((\<nu>\<^bsub>K (P j)\<^esub>) a) ((\<nu>\<^bsub>K (P j)\<^esub>) (-\<^sub>a b))" and
 z = "(\<nu>\<^bsub>K (P j)\<^esub>) ( a \<plusminus> -\<^sub>a b)" in aless_le_trans[of "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (O\<^bsub>K P n\<^esub>). \<forall>x\<in>P\<^bsub>K P n\<^esub> j. r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule ring_n_pd [of "n" "P"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (frule_tac x = r and y = x in Ring.ring_tOp_closed[of "O\<^bsub>K P n\<^esub>"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; Ring (O\<^bsub>K P n\<^esub>); r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:prime_n_pd_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; Ring (O\<^bsub>K P n\<^esub>); r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation,
        simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; Ring (O\<^bsub>K P n\<^esub>); r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> carrier (O\<^bsub>K P n\<^esub>); valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (thin_tac "Ring (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; r \<in> carrier (O\<^bsub>K P n\<^esub>); x \<in> P\<^bsub>K P n\<^esub> j; r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> carrier (O\<^bsub>K P n\<^esub>); valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x \<in> P\<^bsub>K P n\<^esub> j
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:prime_n_pd_def ring_n_pd_def Sr_def, (erule conjE)+,
        simp add:val_t2p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; valuation K (\<nu>\<^bsub>K P j\<^esub>); r \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) r; x \<in> carrier K; r \<cdot>\<^sub>r x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (r \<cdot>\<^sub>r x); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; 0 < (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) r + (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (subgoal_tac "0 \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) r)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; valuation K (\<nu>\<^bsub>K P j\<^esub>); r \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) r; x \<in> carrier K; r \<cdot>\<^sub>r x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (r \<cdot>\<^sub>r x); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; 0 < (\<nu>\<^bsub>K P j\<^esub>) x; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) r\<rbrakk> \<Longrightarrow> 0 < (\<nu>\<^bsub>K P j\<^esub>) r + (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>r x. \<lbrakk>distinct_pds K n P; j \<le> n; valuation K (\<nu>\<^bsub>K P j\<^esub>); r \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) r; x \<in> carrier K; r \<cdot>\<^sub>r x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (r \<cdot>\<^sub>r x); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; 0 < (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) r
 3. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (simp add:aadd_pos_poss, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> 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)
[PROOF STEP]
apply (rule conjI,
        rule contrapos_pp, simp+,
        simp add:prime_n_pd_def,
        (erule conjE)+, simp add: one_in_ring_n_pd_one_K,
        simp add:distinct_pds_def, (erule conjE)+,
        cut_tac representative_of_pd_valuation[of "P j"],
        simp add:value_of_one, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; j \<le> n\<rbrakk> \<Longrightarrow> \<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
[PROOF STEP]
apply ((rule ballI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct_pds K n P; j \<le> n; x \<in> carrier (O\<^bsub>K P n\<^esub>); 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\<rbrakk> \<Longrightarrow> x \<in> P\<^bsub>K P n\<^esub> j \<or> y \<in> P\<^bsub>K P n\<^esub> j
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule conjE,
        simp add:prime_n_pd_def, (erule conjE)+,
        simp add:ring_n_pd_def Sr_def, (erule conjE)+,
        simp add:aneg_less,
        frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) x" in ale_antisym[of _ "0"], simp,
        frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) y" in ale_antisym[of _ "0"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct_pds K n P; j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> 0; (\<nu>\<^bsub>K P j\<^esub>) y \<le> 0; 0 < (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y); x \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; x \<cdot>\<^sub>r y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y); (\<nu>\<^bsub>K P j\<^esub>) x = 0; (\<nu>\<^bsub>K P j\<^esub>) y = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:distinct_pds_def, (erule conjE)+,
        cut_tac representative_of_pd_valuation[of "P j"],
        simp add:val_t2p aadd_0_l,
        simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) n_eq_val_eq_idealTr:
"\<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>);
\<forall>j \<le> n. ((\<nu>\<^bsub>K (P j)\<^esub>) x) \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) y)\<rbrakk> \<Longrightarrow> Rxa (O\<^bsub>K P n\<^esub>) y \<subseteq> Rxa (O\<^bsub>K P n\<^esub>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
[PROOF STEP]
apply (subgoal_tac "\<forall>j \<le> n. valuation K (\<nu>\<^bsub>K (P j)\<^esub>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (case_tac "x = \<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub>",
        simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) \<zero> \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x = \<zero>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p \<zero>
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. \<infinity> \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x = \<zero>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p \<zero>
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "y = \<zero>", simp,
        drule_tac a = n in forall_spec, simp,
        drule_tac a=n in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); x = \<zero>; \<infinity> \<le> (\<nu>\<^bsub>K P n\<^esub>) y; valuation K (\<nu>\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> y = \<zero>
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (cut_tac inf_ge_any[of "(\<nu>\<^bsub>K (P n)\<^esub>) y"],
        frule ale_antisym[of "(\<nu>\<^bsub>K (P n)\<^esub>) y" "\<infinity>"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); x = \<zero>; \<infinity> \<le> (\<nu>\<^bsub>K P n\<^esub>) y; valuation K (\<nu>\<^bsub>K P n\<^esub>); (\<nu>\<^bsub>K P n\<^esub>) y \<le> \<infinity>; (\<nu>\<^bsub>K P n\<^esub>) y = \<infinity>\<rbrakk> \<Longrightarrow> y = \<zero>
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (rule value_inf_zero, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); x = \<zero>; \<infinity> \<le> (\<nu>\<^bsub>K P n\<^esub>) y; valuation K (\<nu>\<^bsub>K P n\<^esub>); (\<nu>\<^bsub>K P n\<^esub>) y \<le> \<infinity>; (\<nu>\<^bsub>K P n\<^esub>) y = \<infinity>\<rbrakk> \<Longrightarrow> y \<in> carrier K
 2. \<lbrakk>distinct_pds K n P; \<zero> \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); x = \<zero>; \<infinity> \<le> (\<nu>\<^bsub>K P n\<^esub>) y; valuation K (\<nu>\<^bsub>K P n\<^esub>); (\<nu>\<^bsub>K P n\<^esub>) y \<le> \<infinity>; (\<nu>\<^bsub>K P n\<^esub>) y = \<infinity>\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P n\<^esub>) y = \<infinity>
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 4. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (simp add:mem_ring_n_pd_mem_K, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (frule ring_n_pd[of n P])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<le>n. 0 \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) (y \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "(y \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)) \<in> carrier (O\<^bsub>K P n\<^esub>)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 4. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (cut_tac field_frac_mul[of "y" "x"],
        frule Ring.rxa_in_Rxa[of "O\<^bsub>K P n\<^esub>" "x" "y \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)"], assumption+,
        simp add:ring_n_pd_tOp_K_tOp[THEN sym],
        frule Ring.principal_ideal[of "O\<^bsub>K P n\<^esub>" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>); y = y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x; y \<in> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x; ideal (O\<^bsub>K P n\<^esub>) ((O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> y \<in> carrier K
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> carrier K
 4. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<noteq> \<zero>
 5. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)
 6. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 7. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (cut_tac Ring.ideal_cont_Rxa[of "O\<^bsub>K P n\<^esub>" "(O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x" "y"],
        assumption+,
        simp add:mem_ring_n_pd_mem_K,
        simp add:mem_ring_n_pd_mem_K,
        simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (frule Ring.rxa_in_Rxa[of "O\<^bsub>K P n\<^esub>" "x" "y \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)"], assumption+,
        simp add:ring_n_pd_def Sr_def,
        (erule conjE)+,
        cut_tac field_is_ring, rule Ring.ring_tOp_closed, assumption+,
        cut_tac invf_closed1[of x], simp, simp,
        simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x); y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>; Ring (K\<lparr>carrier := {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, pop := \<lambda>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. restrict ((\<plusminus>) x) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, mop := restrict (mop K) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, tp := \<lambda>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. restrict ((\<cdot>\<^sub>r) x) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rparr>); \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>); (if y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K then restrict ((\<cdot>\<^sub>r) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} else undefined) x \<in> K\<lparr>carrier := {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, pop := \<lambda>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. restrict ((\<plusminus>) x) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, mop := restrict (mop K) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}, tp := \<lambda>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. restrict ((\<cdot>\<^sub>r) x) {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rparr> \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (cut_tac Ring.ring_tOp_closed, assumption+,
        cut_tac field_is_ring, assumption+, simp+,
        cut_tac invf_closed1[of x], simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI, drule_tac a = j in forall_spec, assumption+,
        cut_tac invf_closed1[of x], simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (y \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (subst val_t2p [where v="\<nu>\<^bsub>K P j\<^esub>"], simp,
        rule mem_ring_n_pd_mem_K[of "n" "P" "y"], assumption+,
        frule_tac x = j in spec, simp,
        simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y + (\<nu>\<^bsub>K P j\<^esub>) (x\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (subst value_of_inv [where v="\<nu>\<^bsub>K P j\<^esub>"], simp,
        simp add:ring_n_pd_def Sr_def, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y + - (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>); x \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>; Ring (O\<^bsub>K P n\<^esub>); j \<le> n; (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) x" and y = "(\<nu>\<^bsub>K (P j)\<^esub>) y" in ale_diff_pos,
        simp add:diff_ant_def,
        simp add:mem_ring_n_pd_mem_K[of "n" "P" "x"] zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI,
       simp add:distinct_pds_def, (erule conjE)+,
       rule_tac P = "P j" in representative_of_pd_valuation, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) n_eq_val_eq_ideal:"\<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>);
      y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j \<le> n.((\<nu>\<^bsub>K (P j)\<^esub>) x) = ((\<nu>\<^bsub>K (P j)\<^esub>) y)\<rbrakk> \<Longrightarrow>
                 Rxa (O\<^bsub>K P n\<^esub>) x = Rxa (O\<^bsub>K P n\<^esub>) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<le> n. (\<nu>\<^bsub>K (P j)\<^esub>) y \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) x)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) y \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) y \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 3. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
[PROOF STEP]
apply (rule n_eq_val_eq_idealTr, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) y \<le> (\<nu>\<^bsub>K P j\<^esub>) x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<le> n. (\<nu>\<^bsub>K (P j)\<^esub>) x \<le> ((\<nu>\<^bsub>K (P j)\<^esub>) y)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p y \<subseteq> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p x
 2. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y
[PROOF STEP]
apply (rule n_eq_val_eq_idealTr, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) x = (\<nu>\<^bsub>K P j\<^esub>) y; j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) x \<le> (\<nu>\<^bsub>K P j\<^esub>) y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mI_vals_nonempty:"\<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 \<noteq> {}"
[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 \<noteq> {}
[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; j \<le> n; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}
[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; j \<le> n; Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I\<rbrakk> \<Longrightarrow> \<nu>\<^bsub>K P j\<^esub> ` I \<noteq> {}
[PROOF STEP]
apply (simp add:image_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; Ring (O\<^bsub>K P n\<^esub>); \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> \<in> I\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>xa\<in>I. x = (\<nu>\<^bsub>K P j\<^esub>) xa
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done