[STATEMENT]
lemma (in Corps) ring_n_distinct_prime_divisors:"distinct_pds K n P \<Longrightarrow>
       Ring (Sr K {x. x\<in>carrier K \<and> (\<forall>j\<le> n. 0 \<le> ((\<nu>\<^bsub> K (P j)\<^esub>) x))})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. P j \<in> Pds) \<and> (\<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m) \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m\<rbrakk> \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> Ring (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule Ring.Sr_ring, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (subst sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<subseteq> carrier K \<and> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<subseteq> carrier K
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rbrakk> \<Longrightarrow> x \<in> carrier K
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> (\<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (simp add:Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) 1\<^sub>r
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) 1\<^sub>r
 2. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp,
        simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. \<forall>y\<in>{x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}. x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; x \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}; y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x} \<and> x \<cdot>\<^sub>r y \<in> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; 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)\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; 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); aGroup K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = y in aGroup.ag_mOp_closed[of "K"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = x and y = "-\<^sub>a y" in aGroup.ag_pOp_closed[of "K"], 
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)) \<and> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rotate_tac -4, frule_tac a = j in forall_spec, assumption,
        rotate_tac -3,
        drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (cut_tac P = "P j" in representative_of_pd_valuation, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac v = "\<nu>\<^bsub>K (P j)\<^esub>" and x = x and y = "-\<^sub>a y" in amin_le_plus, 
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) (-\<^sub>a y)) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (simp add:val_minus_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac x = "(\<nu>\<^bsub>K (P j)\<^esub>) x" and y = "(\<nu>\<^bsub>K (P j)\<^esub>) y" in amin_ge1[of "0"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y
 2. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y); 0 \<le> amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 3. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y j. \<lbrakk>y \<in> carrier K; \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) y; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K; j \<le> n; \<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; x \<in> carrier K; 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x; valuation K (\<nu>\<^bsub>K P j\<^esub>); amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y) \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y); 0 \<le> amin ((\<nu>\<^bsub>K P j\<^esub>) x) ((\<nu>\<^bsub>K P j\<^esub>) y)\<rbrakk> \<Longrightarrow> 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<plusminus> -\<^sub>a y)
 2. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule_tac j = "amin ((\<nu>\<^bsub>K (P j)\<^esub>) x) ((\<nu>\<^bsub>K (P j)\<^esub>) y)" and k = "(\<nu>\<^bsub>K (P j)\<^esub>) (x \<plusminus> -\<^sub>a y)" in ale_trans[of "0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y))
[PROOF STEP]
apply (simp add:Ring.ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>j\<le>n. P j \<in> Pds; \<forall>l\<le>n. \<forall>m\<le>n. l \<noteq> m \<longrightarrow> P l \<noteq> P m; Ring K; aGroup K; 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; -\<^sub>a y \<in> carrier K; x \<plusminus> -\<^sub>a y \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply (rule allI, rule impI,
       cut_tac P = "P j" in representative_of_pd_valuation, simp,
       subst val_t2p [where v="\<nu>\<^bsub>K P j\<^esub>"], assumption+,
       rule aadd_two_pos, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done