[STATEMENT]
lemma (in PolynRg) P_mod_mult1:"\<lbrakk>ideal S I; ideal S J;
      p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q\<rbrakk>  \<Longrightarrow>
      P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p = \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
 2. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (simp add:ring_times_0_x, simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (case_tac "q = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q = \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
 2. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (simp add:ring_times_x_0, simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+,
       frule s_cf_expr[of q], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (cut_tac P_mod_mult[of I J "fst (s_cf R S X p)" "snd (s_cf R S X p)"
       "fst (s_cf R S X q)"  "snd (s_cf R S X q)"])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), snd (s_cf R S X p)) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X q)) (fst (s_cf R S X q), snd (s_cf R S X q)))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (p \<cdot>\<^sub>r q)
 2. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> ideal S I
 3. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> ideal S J
 4. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 5. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X q), snd (s_cf R S X q))
 6. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), snd (s_cf R S X p)))
 7. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X J (polyn_expr R X (fst (s_cf R S X q)) (fst (s_cf R S X q), snd (s_cf R S X q)))
[PROOF STEP]
apply (simp add:polyn_expr_split[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 2. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X q), snd (s_cf R S X q))
 3. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), snd (s_cf R S X p)))
 4. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X J (polyn_expr R X (fst (s_cf R S X q)) (fst (s_cf R S X q), snd (s_cf R S X q)))
[PROOF STEP]
apply (simp add:pol_coeff_split[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X q), snd (s_cf R S X q))
 2. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), snd (s_cf R S X p)))
 3. \<lbrakk>ideal S I; ideal S J; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X J q; p \<noteq> \<zero>; q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X J (polyn_expr R X (fst (s_cf R S X q)) (fst (s_cf R S X q), snd (s_cf R S X q)))
[PROOF STEP]
apply (simp add:polyn_expr_split[THEN sym])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult2l:"\<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R;
      P_mod R S X I p\<rbrakk>  \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring[of S],
       frule Ring.whole_ideal[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; Subring R S; Ring S; ideal S (carrier S)\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (frule P_mod_whole[of q])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; Subring R S; Ring S; ideal S (carrier S); P_mod R S X (carrier S) q\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (frule P_mod_mult1[of I "carrier S" p q], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; Subring R S; Ring S; ideal S (carrier S); P_mod R S X (carrier S) q; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> carrier S) (p \<cdot>\<^sub>r q)\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (simp add:Ring.idealprod_whole_r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult2r:"\<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R;
      P_mod R S X I q\<rbrakk>  \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I q\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring[of S],
       frule Ring.whole_ideal[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I q; Subring R S; Ring S; ideal S (carrier S)\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (frule P_mod_whole[of p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I q; Subring R S; Ring S; ideal S (carrier S); P_mod R S X (carrier S) p\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (frule P_mod_mult1[of "carrier S" I p q], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; P_mod R S X I q; Subring R S; Ring S; ideal S (carrier S); P_mod R S X (carrier S) p; P_mod R S X (carrier S \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> I) (p \<cdot>\<^sub>r q)\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<cdot>\<^sub>r q)
[PROOF STEP]
apply (simp add:Ring.idealprod_whole_l)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) csrp_fn_pol_coeff:"\<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y;
       pol_coeff (S /\<^sub>r P) (n,  c')\<rbrakk> \<Longrightarrow>
                          pol_coeff S (n, (cmp (csrp_fn S P) c'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c')\<rbrakk> \<Longrightarrow> pol_coeff S (n, cmp (csrp_fn S P) c')
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (n, cmp (csrp_fn S P) c')
[PROOF STEP]
apply (simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y; \<forall>j\<le>n. c' j \<in> carrier (S /\<^sub>r P); Subring R S; Ring S\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (csrp_fn S P) c' j \<in> carrier S
[PROOF STEP]
apply (rule allI, rule impI, simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y; \<forall>j\<le>n. c' j \<in> carrier (S /\<^sub>r P); Subring R S; Ring S; j \<le> n\<rbrakk> \<Longrightarrow> csrp_fn S P (c' j) \<in> carrier S
[PROOF STEP]
apply (rule Ring.csrp_fn_mem[of S P], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S P; PolynRg R' (S /\<^sub>r P) Y; \<forall>j\<le>n. c' j \<in> carrier (S /\<^sub>r P); Subring R S; Ring S; j \<le> n\<rbrakk> \<Longrightarrow> c' j \<in> carrier (S /\<^sub>r P)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pj_csrp_mem_coeff:"\<lbrakk>ideal S P; pol_coeff (S /\<^sub>r P) (n, c')\<rbrakk>
      \<Longrightarrow> \<forall>j \<le> n. (pj S P) ((csrp_fn S P) (c' j)) = c' j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S P; pol_coeff (S /\<^sub>r P) (n, c')\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. pj S P (csrp_fn S P (c' j)) = c' j
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S P; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. pj S P (csrp_fn S P (c' j)) = c' j
[PROOF STEP]
apply (rule allI, rule impI, simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S P; \<forall>j\<le>n. c' j \<in> carrier (S /\<^sub>r P); Subring R S; Ring S; j \<le> n\<rbrakk> \<Longrightarrow> pj S P (csrp_fn S P (c' j)) = c' j
[PROOF STEP]
apply (simp add:Ring.csrp_pj)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_pj_csrp:"\<lbrakk>Idomain S; ideal S P;
             PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c')\<rbrakk> \<Longrightarrow>
              erH R S X R' (S /\<^sub>r P) Y (pj S P)
                 (polyn_expr R X n (n, (cmp (csrp_fn S P) c')))
                                     = polyn_expr R' Y n (n, c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c')\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X n (n, cmp (csrp_fn S P) c')) = polyn_expr R' Y n (n, c')
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.qring_ring[of "S" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X n (n, cmp (csrp_fn S P) c')) = polyn_expr R' Y n (n, c')
[PROOF STEP]
apply (subst pHom_mem[of R' "(S /\<^sub>r P)" Y "erH R S X R' (S /\<^sub>r P) Y (pj S P)"
      n  "cmp (csrp_fn S P) c'"], assumption+,
      rule erH_rHom[of R' "S /\<^sub>r P" Y "pj S P"],
       assumption+,
      simp add:pj_Hom, simp add:csrp_fn_pol_coeff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> polyn_expr R' Y n (n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c')) = polyn_expr R' Y n (n, c')
[PROOF STEP]
apply (rule PolynRg.polyn_exprs_eq[of R' "S /\<^sub>r P" Y
       "(n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c'))"
       "(n, c')" n], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> pol_coeff (S /\<^sub>r P) (n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c'))
 2. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> pol_coeff (S /\<^sub>r P) (n, c')
 3. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> n \<le> min (fst (n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c'))) (fst (n, c'))
 4. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. snd (n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c')) j = snd (n, c') j
[PROOF STEP]
apply (frule csrp_fn_pol_coeff[of P R' Y n c'], assumption+,
       frule erH_rHom [of R' "S /\<^sub>r P" Y "pj S P"], assumption+,
       simp add:pj_Hom,
       rule cmp_pol_coeff_e[of R' "S /\<^sub>r P" Y "erH R S X R' (S /\<^sub>r P) Y (pj S P)"
       n "cmp (csrp_fn S P) c'"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. snd (n, cmp (erH R S X R' (S /\<^sub>r P) Y (pj S P)) (cmp (csrp_fn S P) c')) j = snd (n, c') j
[PROOF STEP]
apply (rule allI, rule impI, simp add:cmp_def,
       frule_tac c = "(n, c')" and j = j in
             PolynRg.pol_coeff_mem[of R' "S /\<^sub>r P" Y], assumption+, simp+,
       frule_tac x = "c' j" in Ring.csrp_fn_mem[of S P], assumption+,
       frule_tac s = "csrp_fn S P (c' j)" in
            erH_rHom_cf[of R' "S /\<^sub>r P" Y "pj S P"], assumption+,
            simp add:pj_Hom, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; pol_coeff (S /\<^sub>r P) (n, c'); Subring R S; Ring S; Ring (S /\<^sub>r P); j \<le> n; c' j \<in> carrier (S /\<^sub>r P); csrp_fn S P (c' j) \<in> carrier S; erH R S X R' (S /\<^sub>r P) Y (pj S P) (csrp_fn S P (c' j)) = pj S P (csrp_fn S P (c' j))\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) (csrp_fn S P (c' j)) = c' j
[PROOF STEP]
apply (simp add:pj_csrp_mem_coeff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) ext_csrp_fn_nonzero:"\<lbrakk>Idomain S; ideal S P;
      PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub> \<rbrakk> \<Longrightarrow>
      polyn_expr R X (deg_n R' (S /\<^sub>r P) Y g') ((deg_n R' (S /\<^sub>r P) Y g'),
          (cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr R X (deg_n R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.qring_ring[of "S" "P"], assumption+,
       frule pj_Hom[of "S" "P"], assumption+,
       frule PolynRg.s_cf_expr[of R' "S /\<^sub>r P" Y g'], assumption+,
       (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr R X (deg_n R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<noteq> \<zero>
[PROOF STEP]
apply (simp add:PolynRg.s_cf_deg[THEN sym, of R' "S /\<^sub>r P" Y g'],
       frule csrp_fn_pol_coeff[of P R' Y "deg_n R' (S /\<^sub>r P) Y g'"
                  "snd (s_cf R' (S /\<^sub>r P) Y g')"], assumption+,
       simp add:PolynRg.s_cf_deg[of R' "S /\<^sub>r P" Y g'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (deg_n R' (S /\<^sub>r P) Y g') (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g') \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; pol_coeff S (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))\<rbrakk> \<Longrightarrow> polyn_expr R X (deg_n R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<noteq> \<zero>
[PROOF STEP]
apply (subst coeff_nonzero_polyn_nonzero[of "(deg_n R' (S /\<^sub>r P) Y g',
             cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))"
             "deg_n R' (S /\<^sub>r P) Y g'"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (deg_n R' (S /\<^sub>r P) Y g') (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g') \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; pol_coeff S (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))\<rbrakk> \<Longrightarrow> \<exists>j\<le>deg_n R' (S /\<^sub>r P) Y g'. snd (deg_n R' (S /\<^sub>r P) Y g', cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) j \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:cmp_def, rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (deg_n R' (S /\<^sub>r P) Y g') (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g') \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; pol_coeff S (deg_n R' (S /\<^sub>r P) Y g', \<lambda>x. csrp_fn S P (snd (s_cf R' (S /\<^sub>r P) Y g') x)); \<forall>j\<le>deg_n R' (S /\<^sub>r P) Y g'. csrp_fn S P (snd (s_cf R' (S /\<^sub>r P) Y g') j) = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac a = "deg_n R' (S /\<^sub>r P) Y g'" in forall_spec, simp,
       frule pj_csrp_mem_coeff[of P "deg_n R' (S /\<^sub>r P) Y g'"
                                "snd (s_cf R' (S /\<^sub>r P) Y g')"],
       simp add:PolynRg.s_cf_deg[of R' "S /\<^sub>r P" Y g'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (deg_n R' (S /\<^sub>r P) Y g') (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g') \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; pol_coeff S (deg_n R' (S /\<^sub>r P) Y g', \<lambda>x. csrp_fn S P (snd (s_cf R' (S /\<^sub>r P) Y g') x)); csrp_fn S P (snd (s_cf R' (S /\<^sub>r P) Y g') (deg_n R' (S /\<^sub>r P) Y g')) = \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>deg_n R' (S /\<^sub>r P) Y g'. pj S P (csrp_fn S P (snd (s_cf R' (S /\<^sub>r P) Y g') j)) = snd (s_cf R' (S /\<^sub>r P) Y g') j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac a = "deg_n R' (S /\<^sub>r P) Y g'" in forall_spec, simp,
       simp,
       frule pj_Hom[of S P], assumption, simp add:rHom_0_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_inv:"\<lbrakk>Idomain S; ideal S P; Ring R';
       PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'\<rbrakk> \<Longrightarrow>
      \<exists>g\<in>carrier R. deg R S X g \<le> (deg R' (S /\<^sub>r P) Y g') \<and>
                (erH R S X R' (S /\<^sub>r P) Y (pj S P)) g = g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.qring_ring[of "S" "P"], assumption+,
       frule pj_Hom[of "S" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (frule erH_rHom[of R' "S /\<^sub>r P" Y "pj S P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (case_tac "g' = \<zero>\<^bsub>R'\<^esub>", simp,
       frule erH_rHom_0[of R' "S /\<^sub>r P" Y "pj S P"], assumption+,
       cut_tac ring_zero,
       subgoal_tac "deg R S X (\<zero>) \<le> deg R' (S /\<^sub>r P) Y g'", blast,
       simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (frule PolynRg.s_cf_expr [of R' "S /\<^sub>r P" Y g'], assumption+,
       (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); g' = polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (frule pHom_pj_csrp[of P R' Y "fst (s_cf R' (S /\<^sub>r P) Y g')"
                      "snd (s_cf R' (S /\<^sub>r P) Y g')"], assumption+,
       simp add:PolynRg.pol_coeff_split[THEN sym],
       drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> \<exists>g\<in>carrier R. deg R S X g \<le> deg R' (S /\<^sub>r P) Y g' \<and> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = g'
[PROOF STEP]
apply (subgoal_tac "deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P)
           Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P)
          (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'",
         subgoal_tac "polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g'))
          (fst (s_cf R' (S /\<^sub>r P) Y g'),
           cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<in> carrier R",
         blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'; deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<in> carrier R
 2. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'
[PROOF STEP]
apply(thin_tac " deg R S X
         (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g'))
         (fst (s_cf R' (S /\<^sub>r P) Y g'),
         cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))))
         \<le> deg R' (S /\<^sub>r P) Y g'",
     thin_tac "polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g'))
         (s_cf R' (S /\<^sub>r P) Y g') = g'",
     thin_tac "erH R S X R' (S /\<^sub>r P) Y (pj S P)
         (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g'))
         (fst (s_cf R' (S /\<^sub>r P) Y g'),
         cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'",
     thin_tac "snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq>
               \<zero>\<^bsub>S /\<^sub>r P\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g')\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<in> carrier R
 2. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'
[PROOF STEP]
apply (rule_tac c = "(fst (s_cf R' (S /\<^sub>r P) Y g'),
         cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))" and
         k = "fst (s_cf R' (S /\<^sub>r P) Y g')" in polyn_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g')\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))
 2. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g')\<rbrakk> \<Longrightarrow> fst (s_cf R' (S /\<^sub>r P) Y g') \<le> fst (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))
 3. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'
[PROOF STEP]
apply (rule csrp_fn_pol_coeff, assumption+,
         simp, simp,
         cut_tac pol_deg_le_n[of "polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g'))
          (fst (s_cf R' (S /\<^sub>r P) Y g'),
          cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))"
            "(fst (s_cf R' (S /\<^sub>r P) Y g'),
          cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'; deg_n R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> fst (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) \<le> deg R' (S /\<^sub>r P) Y g'
 2. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) \<in> carrier R
 3. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))
 4. \<lbrakk>Idomain S; ideal S P; Ring R'; PolynRg R' (S /\<^sub>r P) Y; g' \<in> carrier R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; g' \<noteq> \<zero>\<^bsub>R'\<^esub>; pol_coeff (S /\<^sub>r P) (s_cf R' (S /\<^sub>r P) Y g'); snd (s_cf R' (S /\<^sub>r P) Y g') (fst (s_cf R' (S /\<^sub>r P) Y g')) \<noteq> \<zero>\<^bsub>S /\<^sub>r P\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) = g'; polyn_expr R' Y (fst (s_cf R' (S /\<^sub>r P) Y g')) (s_cf R' (S /\<^sub>r P) Y g') = g'\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R' (S /\<^sub>r P) Y g')) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g'))) = polyn_expr R X (fst (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))) (fst (s_cf R' (S /\<^sub>r P) Y g'), cmp (csrp_fn S P) (snd (s_cf R' (S /\<^sub>r P) Y g')))
[PROOF STEP]
apply (simp,
        simp add:PolynRg.s_cf_deg[THEN sym, of R' "S /\<^sub>r P" Y g'],
        frule ext_csrp_fn_nonzero[of P R' Y g'], assumption+,
        simp add:deg_def, simp add:ale_natle,
        rule polyn_mem, simp add:csrp_fn_pol_coeff, simp,
        simp add:csrp_fn_pol_coeff, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_0:"\<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y;
       g \<in> carrier R\<rbrakk> \<Longrightarrow>
      (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = (P_mod R S X P g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.qring_ring[of "S" "P"], assumption+,
       frule pj_Hom[of "S" "P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (case_tac "g = \<zero>\<^bsub>R\<^esub>",
       cut_tac ring_zero, simp add:P_mod_def,
       rule erH_rHom_0[of R' "S /\<^sub>r P" Y "pj S P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (frule s_cf_expr[of g], assumption+, (erule conjE)+,
       cut_tac polyn_expr_split[of "fst (s_cf R S X g)" "s_cf R S X g"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g))\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (frule erH_map[of R' "S /\<^sub>r P" Y "pj S P" "fst (s_cf R S X g)"
                        "snd (s_cf R S X g)"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g))\<rbrakk> \<Longrightarrow> pol_coeff S (fst (s_cf R S X g), snd (s_cf R S X g))
 2. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g)); erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g))) = polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (subst pol_coeff_split[THEN sym], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g)); erH R S X R' (S /\<^sub>r P) Y (pj S P) (polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), snd (s_cf R S X g))) = polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; erH R S X R' (S /\<^sub>r P) Y (pj S P) g = polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))); polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = g\<rbrakk> \<Longrightarrow> (polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))) = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (thin_tac "erH R S X R' (S /\<^sub>r P) Y (pj S P) g =
       polyn_expr R' Y (fst (s_cf R S X g))
      (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = g\<rbrakk> \<Longrightarrow> (polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))) = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (rotate_tac -1, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g)\<rbrakk> \<Longrightarrow> (polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))) = \<zero>\<^bsub>R'\<^esub>) = P_mod R S X P g
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of P g "s_cf R S X g"], assumption+,
       thin_tac "g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g)",
       frule erH_rHom_coeff[of R' "S /\<^sub>r P" Y "pj S P" "fst (s_cf R S X g)"
       "snd (s_cf R S X g)"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff (S /\<^sub>r P) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))\<rbrakk> \<Longrightarrow> (polyn_expr R' Y (fst (s_cf R S X g)) (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))) = \<zero>\<^bsub>R'\<^esub>) = (\<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P)
[PROOF STEP]
apply (subst PolynRg.coeff_0_pol_0[THEN sym, of R' "S /\<^sub>r P" Y
        "(fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))"
        "fst (s_cf R S X g)"], assumption+, simp,
       thin_tac "pol_coeff (S /\<^sub>r P)
       (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst (s_cf R S X g). snd (fst (s_cf R S X g), cmp (pj S P) (snd (s_cf R S X g))) j = \<zero>\<^bsub>S /\<^sub>r P\<^esub>) = (\<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P)
[PROOF STEP]
apply (simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst (s_cf R S X g). pj S P (snd (s_cf R S X g) j) = \<zero>\<^bsub>S /\<^sub>r P\<^esub>) = (\<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>fst (s_cf R S X g). pj S P (snd (s_cf R S X g) j) = \<zero>\<^bsub>S /\<^sub>r P\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P
 2. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). pj S P (snd (s_cf R S X g) j) = \<zero>\<^bsub>S /\<^sub>r P\<^esub>
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, assumption,
        frule_tac j = j in pol_coeff_mem[of "s_cf R S X g"], assumption+,
        simp add:pj_zero[of S P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> P\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). pj S P (snd (s_cf R S X g) j) = \<zero>\<^bsub>S /\<^sub>r P\<^esub>
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, assumption,
        frule_tac j = j in pol_coeff_mem[of "s_cf R S X g"], assumption+,
        simp add:pj_zero[THEN sym, of S P])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_I_J:"\<lbrakk>p \<in> carrier R; ideal S I; ideal S J;
          I \<subseteq> J;  P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X J p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X J p
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I \<zero>; p = \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X J \<zero>
 2. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I p; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X J p
[PROOF STEP]
apply (simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I p; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X J p
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I p; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X J p
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I p "s_cf R S X p"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; P_mod R S X I p; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X I p = (\<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I)\<rbrakk> \<Longrightarrow> P_mod R S X J p
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of J p "s_cf R S X p"], assumption+,
        thin_tac "p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)",
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; ideal S I; ideal S J; I \<subseteq> J; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X I p\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> J
[PROOF STEP]
apply (rule allI, rule impI, drule_tac a = j in forall_spec, assumption,
        simp add:subsetD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_n_1:"\<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R;
       P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc n)\<^esup>)) g\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.npClose[of S t n], assumption+,
       frule Ring.npClose[of S t "Suc n"], assumption+,
       frule Ring.principal_ideal[of S t], assumption+,
       frule Ring.principal_ideal[of S "t^\<^bsup>S (Suc n)\<^esup>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (case_tac "g = \<zero>\<^bsub>R\<^esub>", simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)); g \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (frule s_cf_expr[of g], assumption,
        (erule conjE)+,
       subst P_mod_mod[THEN sym, of "S \<diamondsuit>\<^sub>p t" "g" "s_cf R S X g"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (frule_tac P_mod_mod[THEN sym, of "S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc n)\<^esup>)" g "s_cf R S X g"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g = (\<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>))\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (simp del:npow_suc,
       thin_tac "g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>); Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (rule allI, rule impI,
       drule_tac a = j in forall_spec, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; Subring R S; Ring S; t^\<^bsup>S n\<^esup> \<in> carrier S; t^\<^bsup>S Suc n\<^esup> \<in> carrier S; ideal S (S \<diamondsuit>\<^sub>p t); ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)); g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; j \<le> fst (s_cf R S X g); snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)\<rbrakk> \<Longrightarrow> snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (simp add:Rxa_def, erule bexE, simp,
       simp add:Ring.ring_tOp_assoc[THEN sym, of S],
       frule_tac x = r and y = "t^\<^bsup>S n\<^esup>" in Ring.ring_tOp_closed, assumption+,
       blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_n_m:"\<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R;
      m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc n)\<^esup>)) g\<rbrakk> \<Longrightarrow>
               P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) g
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) g
[PROOF STEP]
apply (rule P_mod_I_J[of g "S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc n)\<^esup>)" "S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)"],
       assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>))
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>))
 3. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>) \<subseteq> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)
 4. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (rule Ring.principal_ideal, assumption+,
        rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> ideal S (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>))
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>) \<subseteq> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)
 3. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (rule Ring.principal_ideal, assumption+,
        rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>) \<subseteq> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc n)\<^esup>)) g")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S\<rbrakk> \<Longrightarrow> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>) \<subseteq> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S; x \<in> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)\<rbrakk> \<Longrightarrow> x \<in> S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (simp del:npow_suc add:Rxa_def, erule bexE, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S; r \<in> carrier S; x = r \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc n\<^esup>\<rbrakk> \<Longrightarrow> \<exists>ra\<in>carrier S. r \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc n\<^esup> = ra \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (frule Ring.npMulDistr[THEN sym, of S t "Suc n - Suc m" "Suc m"],
          assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S; r \<in> carrier S; x = r \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc n\<^esup>; t^\<^bsup>S (Suc n - Suc m + Suc m)\<^esup> = t^\<^bsup>S (Suc n - Suc m)\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>\<rbrakk> \<Longrightarrow> \<exists>ra\<in>carrier S. r \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc n\<^esup> = ra \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (simp del:npow_suc,
          thin_tac "t^\<^bsup>S (Suc n)\<^esup> = t^\<^bsup>S (n - m)\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S (Suc m)\<^esup>",
          thin_tac "x = r \<cdot>\<^sub>r\<^bsub>S\<^esub> (t^\<^bsup>S (n - m)\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S (Suc m)\<^esup>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S; r \<in> carrier S\<rbrakk> \<Longrightarrow> \<exists>ra\<in>carrier S. r \<cdot>\<^sub>r\<^bsub>S\<^esub> (t^\<^bsup>S (n - m)\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>) = ra \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (subst Ring.ring_tOp_assoc[THEN sym, of S], assumption+,
          (rule Ring.npClose, assumption+)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; Subring R S; Ring S; r \<in> carrier S\<rbrakk> \<Longrightarrow> \<exists>ra\<in>carrier S. r \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S (n - m)\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup> = ra \<cdot>\<^sub>r\<^bsub>S\<^esub> t^\<^bsup>S Suc m\<^esup>
 2. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply (frule_tac x = r and y = "t^\<^bsup>S (n - m)\<^esup>" in Ring.ring_tOp_closed,
           assumption+,
          rule Ring.npClose, assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; m \<le> n; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc n\<^esup>)) g
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_diff:"\<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y;
       g \<in> carrier R; h \<in> carrier R\<rbrakk> \<Longrightarrow>
    (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = (erH R S X R' (S /\<^sub>r P) Y (pj S P) h))
     = (P_mod R S X P (g \<plusminus> -\<^sub>a h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h) = P_mod R S X P (g \<plusminus> -\<^sub>a h)
[PROOF STEP]
apply (cut_tac ring_is_ag,
       frule PolynRg.is_Ring[of R'],
       cut_tac subring,
       frule subring_Ring,
       frule Ring.qring_ring[of S P], assumption+,
       frule pj_Hom[of "S" "P"], assumption+,
       frule erH_rHom[of R' "S /\<^sub>r P" Y "pj S P"],
       assumption+,
       frule Ring.ring_is_ag[of R'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h) = P_mod R S X P (g \<plusminus> -\<^sub>a h)
[PROOF STEP]
apply (frule erH_mem[of R' "S /\<^sub>r P" Y "pj S P" g], assumption+,
       frule erH_mem[of R' "S /\<^sub>r P" Y "pj S P" h], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'\<rbrakk> \<Longrightarrow> (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h) = P_mod R S X P (g \<plusminus> -\<^sub>a h)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h\<rbrakk> \<Longrightarrow> P_mod R S X P (g \<plusminus> -\<^sub>a h)
 2. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; P_mod R S X P (g \<plusminus> -\<^sub>a h)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h
[PROOF STEP]
apply (frule_tac a = "erH R S X R' (S /\<^sub>r P) Y (pj S P) g" and
                 b = "erH R S X R' (S /\<^sub>r P) Y (pj S P) h" in
       aGroup.ag_eq_diffzero[of R'], assumption+, simp,
       simp add:erH_minus[THEN sym, of R' "S /\<^sub>r P" Y "pj S P" h],
       drule sym, simp,
       thin_tac "erH R S X R' (S /\<^sub>r P) Y (pj S P) h =
                        erH R S X R' (S /\<^sub>r P) Y (pj S P) g",
       frule_tac x = h in aGroup.ag_mOp_closed, assumption+,
       simp add:erH_add[THEN sym, of  R' "S /\<^sub>r P" Y "pj S P" g "-\<^sub>a h"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) (g \<plusminus> -\<^sub>a h) = \<zero>\<^bsub>R'\<^esub>; -\<^sub>a h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X P (g \<plusminus> -\<^sub>a h)
 2. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; P_mod R S X P (g \<plusminus> -\<^sub>a h)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h
[PROOF STEP]
apply (subst P_mod_0[THEN sym, of P R' Y "g \<plusminus> -\<^sub>a h"], assumption+,
         rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; P_mod R S X P (g \<plusminus> -\<^sub>a h)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h
[PROOF STEP]
apply (frule_tac a = "erH R S X R' (S /\<^sub>r P) Y (pj S P) g" and
                 b = "erH R S X R' (S /\<^sub>r P) Y (pj S P) h" in
       aGroup.ag_eq_diffzero[of R'], assumption+, simp,
       simp add:erH_minus[THEN sym, of R' "S /\<^sub>r P" Y "pj S P" h])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; P_mod R S X P (g \<plusminus> -\<^sub>a h); (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h) = (erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r P) Y (pj S P) (-\<^sub>a h) = \<zero>\<^bsub>R'\<^esub>)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r P) Y (pj S P) (-\<^sub>a h) = \<zero>\<^bsub>R'\<^esub>
[PROOF STEP]
apply (subst erH_add[THEN sym, of  R' "S /\<^sub>r P" Y "pj S P" g "-\<^sub>a h"],
          assumption+,
          rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; h \<in> carrier R; aGroup R; Ring R'; Subring R S; Ring S; Ring (S /\<^sub>r P); pj S P \<in> rHom S (S /\<^sub>r P); erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y; aGroup R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<in> carrier R'; erH R S X R' (S /\<^sub>r P) Y (pj S P) h \<in> carrier R'; P_mod R S X P (g \<plusminus> -\<^sub>a h); (erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) h) = (erH R S X R' (S /\<^sub>r P) Y (pj S P) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r P) Y (pj S P) (-\<^sub>a h) = \<zero>\<^bsub>R'\<^esub>)\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) (g \<plusminus> -\<^sub>a h) = \<zero>\<^bsub>R'\<^esub>
[PROOF STEP]
apply (subst P_mod_0[of P R' Y "g \<plusminus> -\<^sub>a h"], assumption+,
          rule aGroup.ag_pOp_closed, assumption+,
          rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_erH:"\<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y;
        g \<in> carrier R; v \<in> carrier R; t \<in> P \<rbrakk> \<Longrightarrow>
        (erH R S X R' (S /\<^sub>r P) Y (pj S P) g =
                  (erH R S X R' (S /\<^sub>r P) Y (pj S P) (g \<plusminus> (t \<cdot>\<^sub>r v))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; v \<in> carrier R; t \<in> P\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) (g \<plusminus> t \<cdot>\<^sub>r v)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag,
       frule Ring.ideal_subset[of S P t], assumption+,
       frule mem_subring_mem_ring[of S t], assumption+,
       frule ring_tOp_closed[of t v], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; v \<in> carrier R; t \<in> P; Subring R S; Ring S; aGroup R; t \<in> carrier S; t \<in> carrier R; t \<cdot>\<^sub>r v \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) g = erH R S X R' (S /\<^sub>r P) Y (pj S P) (g \<plusminus> t \<cdot>\<^sub>r v)
[PROOF STEP]
apply (subst P_mod_diff[of P R' Y g "g \<plusminus> (t \<cdot>\<^sub>r v)"], assumption+,
       rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; v \<in> carrier R; t \<in> P; Subring R S; Ring S; aGroup R; t \<in> carrier S; t \<in> carrier R; t \<cdot>\<^sub>r v \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X P (g \<plusminus> -\<^sub>a (g \<plusminus> t \<cdot>\<^sub>r v))
[PROOF STEP]
apply (simp add:aGroup.ag_p_inv,
       frule aGroup.ag_mOp_closed[of R g], assumption+,
       frule aGroup.ag_mOp_closed[of R "t \<cdot>\<^sub>r v"], assumption+,
       subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
       simp add:aGroup.ag_r_inv1, simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S P; PolynRg R' (S /\<^sub>r P) Y; g \<in> carrier R; v \<in> carrier R; t \<in> P; Subring R S; Ring S; aGroup R; t \<in> carrier S; t \<in> carrier R; t \<cdot>\<^sub>r v \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a t \<cdot>\<^sub>r v \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X P (-\<^sub>a t \<cdot>\<^sub>r v)
[PROOF STEP]
apply (rule P_mod_minus[of P "t \<cdot>\<^sub>r v"], assumption+,
       frule P_mod_mult1[of P "carrier S" t v],
       simp add:Ring.whole_ideal, assumption+,
       subst P_mod_coeffTr[of P t], assumption+,
       rule P_mod_whole[of v], assumption+,
       simp add:Ring.idealprod_whole_r[of S P])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) coeff_principalTr:"\<lbrakk>t \<in> carrier S\<rbrakk> \<Longrightarrow>
    \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j \<le> n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow>
          (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j \<le> n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> (f' j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> carrier S \<Longrightarrow> \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j))
[PROOF STEP]
apply (induct_tac n,
       rule allI, rule impI, erule conjE,
       simp add:Rxa_def, erule bexE,
       simp add:Ring.ring_tOp_commute[of S _ t],
       subgoal_tac "pol_coeff S (0, (\<lambda>j. r))",
       subgoal_tac "t \<cdot>\<^sub>r\<^bsub>S\<^esub> r = t \<cdot>\<^sub>r\<^bsub>S\<^esub> ((\<lambda>j. r) 0)", blast,
       simp,
       simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j))\<rbrakk> \<Longrightarrow> \<forall>f. pol_coeff S (Suc n, f) \<and> (\<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (Suc n, f') \<and> (\<forall>j\<le>Suc n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j))
[PROOF STEP]
apply (rule allI, rule impI, erule conjE,
       frule_tac n = n and f = f in pol_coeff_pre,
       subgoal_tac "\<forall>j \<le> n. f j \<in> S \<diamondsuit>\<^sub>p t",
       drule_tac a = f in forall_spec, simp,
       erule exE, erule conjE,
       frule_tac c = "(Suc n, f)" and j = "Suc n" in
        pol_coeff_mem, simp, simp,
        drule_tac x = "Suc n" in spec, simp,
        simp add:Rxa_def,
        erule bexE, simp add:Ring.ring_tOp_commute[of "S" _ "t"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f f' r. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); pol_coeff S (n, f); \<forall>j\<le>n. \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; pol_coeff S (n, f'); \<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; t \<cdot>\<^sub>r\<^bsub>S\<^esub> r \<in> carrier S; r \<in> carrier S; f (Suc n) = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r\<rbrakk> \<Longrightarrow> \<exists>f'. pol_coeff S (Suc n, f') \<and> (\<forall>j\<le>Suc n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)
 2. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)); pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (subgoal_tac "pol_coeff S ((Suc n), (\<lambda>j. if j \<le> n then (f' j) else r))
         \<and>
        (\<forall>j \<le> (Suc n). f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> ((\<lambda>j. if j \<le> n then (f' j) else r) j))",
       blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f f' r. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); pol_coeff S (n, f); \<forall>j\<le>n. \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; pol_coeff S (n, f'); \<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; t \<cdot>\<^sub>r\<^bsub>S\<^esub> r \<in> carrier S; r \<in> carrier S; f (Suc n) = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r\<rbrakk> \<Longrightarrow> pol_coeff S (Suc n, \<lambda>j. if j \<le> n then f' j else r) \<and> (\<forall>j\<le>Suc n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> (if j \<le> n then f' j else r))
 2. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)); pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (rule conjI, simp add:pol_coeff_def,
         rule allI, rule impI,
         case_tac "j \<le> n", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f f' r j. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); pol_coeff S (n, f); \<forall>j\<le>n. \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; pol_coeff S (n, f'); \<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; t \<cdot>\<^sub>r\<^bsub>S\<^esub> r \<in> carrier S; r \<in> carrier S; f (Suc n) = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; j \<le> Suc n; \<not> j \<le> n\<rbrakk> \<Longrightarrow> f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> (if j \<le> n then f' j else r)
 2. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)); pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f f' r j. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); pol_coeff S (n, f); \<forall>j\<le>n. \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; pol_coeff S (n, f'); \<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; t \<cdot>\<^sub>r\<^bsub>S\<^esub> r \<in> carrier S; r \<in> carrier S; f (Suc n) = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; j \<le> Suc n; \<not> j \<le> n\<rbrakk> \<Longrightarrow> f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r
 2. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)); pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (drule_tac y = j and x = n in not_le_imp_less,
         drule_tac m = n and n = j in Suc_leI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f f' r j. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); pol_coeff S (n, f); \<forall>j\<le>n. \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; pol_coeff S (n, f'); \<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; t \<cdot>\<^sub>r\<^bsub>S\<^esub> r \<in> carrier S; r \<in> carrier S; f (Suc n) = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r; j \<le> Suc n; Suc n \<le> j\<rbrakk> \<Longrightarrow> f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> r
 2. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; \<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow> (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)); pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (frule_tac m = j and n = "Suc n" in le_antisym, assumption, simp,
         thin_tac "\<forall>f. pol_coeff S (n, f) \<and> (\<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t) \<longrightarrow>
                  (\<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>t \<in> carrier S; Subring R S; Ring S; aGroup R; pol_coeff S (Suc n, f); \<forall>j\<le>Suc n. f j \<in> S \<diamondsuit>\<^sub>p t; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (rule allI, rule impI,
         drule_tac a = j in forall_spec, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) coeff_principal:"\<lbrakk>t \<in> carrier S; pol_coeff S (n, f);
          \<forall>j \<le> n. f j \<in> S \<diamondsuit>\<^sub>p t\<rbrakk> \<Longrightarrow>
          \<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j \<le> n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> (f' j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; pol_coeff S (n, f); \<forall>j\<le>n. f j \<in> S \<diamondsuit>\<^sub>p t\<rbrakk> \<Longrightarrow> \<exists>f'. pol_coeff S (n, f') \<and> (\<forall>j\<le>n. f j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j)
[PROOF STEP]
apply (simp add:coeff_principalTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done