[STATEMENT]
lemma (in PolynRg) P_mod_add:"\<lbrakk>ideal S I; p \<in> carrier R;
      q \<in> carrier R; P_mod R S X I p; P_mod R S X I q\<rbrakk> \<Longrightarrow>
               P_mod R S X I (p \<plusminus> 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; P_mod R S X I q\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (cut_tac subring,
       frule subring_Ring,
       cut_tac ring_is_ag)
[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; P_mod R S X I q; Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_l_zero,
       case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_r_zero)
[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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (case_tac "p \<plusminus>\<^bsub>R\<^esub> q = \<zero>\<^bsub>R\<^esub>", simp add:P_mod_def)
[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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> 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; p \<in> carrier R; q \<in> carrier R; P_mod R S X I p; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> 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 (p \<plusminus> q)
[PROOF STEP]
apply (frule polyn_add1[of "s_cf R S X p" "s_cf R S X q"], assumption+,
       drule sym, drule sym, simp, drule sym, simp,
       rotate_tac -1, drule sym)
[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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q) = q; p \<plusminus> q = polyn_expr R X (max (fst (s_cf R S X p)) (fst (s_cf R S X q))) (add_cf S (s_cf R S X p) (s_cf R S X q))\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I p "s_cf R S X p"], assumption+, simp,
       thin_tac "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p",
       frule P_mod_mod[THEN sym, of I q "s_cf R S X q"], assumption+, simp,
       thin_tac "polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q) = 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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; p \<plusminus> q = polyn_expr R X (max (fst (s_cf R S X p)) (fst (s_cf R S X q))) (add_cf S (s_cf R S X p) (s_cf R S X q)); 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); P_mod R S X I q = (\<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I)\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (frule aGroup.ag_pOp_closed[of R 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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; p \<plusminus> q = polyn_expr R X (max (fst (s_cf R S X p)) (fst (s_cf R S X q))) (add_cf S (s_cf R S X p) (s_cf R S X q)); 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); P_mod R S X I q = (\<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I); p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X I (p \<plusminus> q)
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of I "p \<plusminus> q"
             "add_cf S (s_cf R S X p) (s_cf R S X q)"], assumption+,
       simp add:add_cf_pol_coeff, simp, simp add:add_cf_len,
       thin_tac "p \<plusminus> q =
         polyn_expr R X (max (fst (s_cf R S X p)) (fst (s_cf R S X q)))
         (add_cf S (s_cf R S X p) (s_cf R S X 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; P_mod R S X I q; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p = (\<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I); P_mod R S X I q = (\<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I); p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (add_cf S (s_cf R S X p) (s_cf R S X q)). snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (add_cf S (s_cf R S X p) (s_cf R S X q)). snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (subst add_cf_len, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>j\<le>max (fst (s_cf R S X p)) (fst (s_cf R S X q)). snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q))\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (cut_tac x = "fst (s_cf R S X p)" and y = "fst (s_cf R S X q)" in
       less_linear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) < fst (s_cf R S X q) \<or> fst (s_cf R S X p) = fst (s_cf R S X q) \<or> fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) < fst (s_cf R S X q)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
 2. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) = fst (s_cf R S X q) \<or> fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (simp, subst add_cf_def, simp,
       (rule impI,
        drule_tac a = j in forall_spec, assumption,
        drule_tac x = j in spec,
        frule_tac x = j and y = "fst (s_cf R S X p)" and
           z = "fst (s_cf R S X q)" in le_less_trans, assumption+,
        frule_tac x = j and y = "fst (s_cf R S X q)" in less_imp_le, simp))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; fst (s_cf R S X p) < fst (s_cf R S X q); j \<le> fst (s_cf R S X p); snd (s_cf R S X p) j \<in> I; snd (s_cf R S X q) j \<in> I\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) j \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X q) j \<in> I
 2. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) = fst (s_cf R S X q) \<or> fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (rule Ring.ideal_pOp_closed[of S I], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) = fst (s_cf R S X q) \<or> fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X p) = fst (s_cf R S X q)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
 2. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (simp, subst add_cf_def, simp,
        drule_tac a = j in forall_spec, assumption,
        drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> fst (s_cf R S X q); fst (s_cf R S X p) = fst (s_cf R S X q); snd (s_cf R S X p) j \<in> I; snd (s_cf R S X q) j \<in> I\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) j \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X q) j \<in> I
 2. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (rule Ring.ideal_pOp_closed[of S I], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; \<forall>j\<le>fst (s_cf R S X q). snd (s_cf R S X q) j \<in> I; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; j \<le> max (fst (s_cf R S X p)) (fst (s_cf R S X q)); fst (s_cf R S X q) < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (add_cf S (s_cf R S X p) (s_cf R S X q)) j \<in> I
[PROOF STEP]
apply (simp add: max.absorb1 max.absorb2, subst add_cf_def, simp, rule impI,
        drule_tac x = j in spec,
        drule_tac a = j in forall_spec, assumption,
        frule_tac x = j and y = "fst (s_cf R S X q)" and
           z = "fst (s_cf R S X p)" in le_less_trans, assumption+,
        frule_tac x = j and y = "fst (s_cf R S X p)" in less_imp_le, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; q \<in> carrier R; Subring R S; Ring S; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 p; P_mod R S X I q; p \<plusminus> q \<in> carrier R; fst (s_cf R S X q) < fst (s_cf R S X p); j \<le> fst (s_cf R S X q); snd (s_cf R S X p) j \<in> I; snd (s_cf R S X q) j \<in> I\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) j \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X q) j \<in> I
[PROOF STEP]
apply (rule Ring.ideal_pOp_closed[of S I], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_minus:"\<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p\<rbrakk> \<Longrightarrow>
                  P_mod R S X I (-\<^sub>a p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X I (-\<^sub>a p)
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring,
       frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p; aGroup R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X I (-\<^sub>a p)
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p; aGroup R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X I (-\<^sub>a p)
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+,
       frule polyn_minus_m_cf[of "s_cf R S X p" "fst (s_cf R S X p)"],
       simp,
       frule aGroup.ag_inv_inj[of R p \<zero>], assumption,
       simp add:ring_zero, assumption, simp add:aGroup.ag_inv_zero,
       frule m_cf_pol_coeff[of "s_cf R S X p"],
       drule sym, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p; aGroup R; Subring R S; Ring S; 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>; -\<^sub>a p \<noteq> \<zero>; pol_coeff S (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)) = -\<^sub>a p\<rbrakk> \<Longrightarrow> P_mod R S X I (-\<^sub>a p)
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of I "-\<^sub>a p" "m_cf S (s_cf R S X p)"],
        assumption+,
      rule aGroup.ag_mOp_closed[of R p], assumption+,
      simp add:m_cf_len,
      thin_tac "polyn_expr R X (fst (s_cf R S X p))
                                 (m_cf S (s_cf R S X p)) = -\<^sub>a p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; P_mod R S X I p; aGroup R; Subring R S; Ring S; 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>; -\<^sub>a p \<noteq> \<zero>; pol_coeff S (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (m_cf S (s_cf R S X p)). snd (m_cf S (s_cf R S X p)) j \<in> I
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I p "s_cf R S X p"], assumption+, simp,
       thin_tac "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p",
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; aGroup R; Subring R S; Ring S; 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>; -\<^sub>a p \<noteq> \<zero>; pol_coeff S (m_cf S (s_cf R S X p)); P_mod R S X I p\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (m_cf S (s_cf R S X p)). snd (m_cf S (s_cf R S X p)) j \<in> I
[PROOF STEP]
apply (rule allI, rule impI,
       drule_tac a = j in forall_spec, simp add:m_cf_len,
       subst m_cf_def, simp,
       rule Ring.ideal_inv1_closed[of S I], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_pre:"\<lbrakk>ideal S I; pol_coeff S ((Suc n), f);
       P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f))\<rbrakk> \<Longrightarrow>
       P_mod R S X I (polyn_expr R X n (n, f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; pol_coeff S (Suc n, f); P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f))\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X n (n, f))
[PROOF STEP]
apply (frule pol_coeff_pre[of n f],
       frule polyn_mem[of "(n, f)" n],simp,
       frule polyn_mem[of "(Suc n, f)" "Suc n"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; pol_coeff S (Suc n, f); P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f)); pol_coeff S (n, f); polyn_expr R X n (n, f) \<in> carrier R; polyn_expr R X (Suc n) (Suc n, f) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X n (n, f))
[PROOF STEP]
apply (case_tac "polyn_expr R X n (n, f) = \<zero>\<^bsub>R\<^esub>", simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; pol_coeff S (Suc n, f); P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f)); pol_coeff S (n, f); polyn_expr R X n (n, f) \<in> carrier R; polyn_expr R X (Suc n) (Suc n, f) \<in> carrier R; polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X n (n, f))
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of I
                  "polyn_expr R X n (n, f)" "(n, f)"], assumption+, simp,
       frule P_mod_mod[THEN sym, of I "polyn_expr R X (Suc n) (Suc n, f)"
               "(Suc n, f)"], assumption+, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_pre1:"\<lbrakk>ideal S I; pol_coeff S ((Suc n), f);
       P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f))\<rbrakk> \<Longrightarrow>
       P_mod R S X I (polyn_expr R X n (Suc n, f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; pol_coeff S (Suc n, f); P_mod R S X I (polyn_expr R X (Suc n) (Suc n, f))\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X n (Suc n, f))
[PROOF STEP]
by (simp add:polyn_expr_restrict[of n f], simp add:P_mod_pre)


[STATEMENT]
lemma (in PolynRg) P_mod_coeffTr:"\<lbrakk>ideal S I; d \<in> carrier S\<rbrakk> \<Longrightarrow>
                   (P_mod R S X I d) = (d \<in> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; d \<in> carrier S\<rbrakk> \<Longrightarrow> P_mod R S X I d = (d \<in> I)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       subst monomial_P_mod_mod[of I d "d \<cdot>\<^sub>r X^\<^bsup>R 0\<^esup>" 0], assumption+,
       simp, simp,
       frule mem_subring_mem_ring[of _ d], assumption+,
       simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult_const:"\<lbrakk>ideal S I; ideal S J;
     pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f));
     pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g))\<rbrakk> \<Longrightarrow>
       P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) ((polyn_expr R X n (n, f)) \<cdot>\<^sub>r
                                        (polyn_expr R X 0 (0, g)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (frule_tac c = "(n, f)" in polyn_mem[of _ n], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (frule Ring.ideal_prod_ideal[of S I J], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J)\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (case_tac "polyn_expr R X n (n, f) = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I \<zero>; pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S; \<zero> \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) = \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (\<zero> \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
 2. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (frule_tac c = "(0, g)" in polyn_mem[of _ 0], simp,
        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; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (polyn_expr R X 0 (0, g)); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
[PROOF STEP]
apply (simp add:polyn_expr_def [of _ _ "0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (g 0 \<cdot>\<^sub>r 1\<^sub>r); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (g 0 \<cdot>\<^sub>r 1\<^sub>r))
[PROOF STEP]
apply (frule pol_coeff_mem[of "(0, g)" 0], simp, simp,
        frule mem_subring_mem_ring[of S "g 0"], assumption,
        simp add:ring_r_one,
        simp add:ring_tOp_commute[of _ "g 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (g 0); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (g 0 \<cdot>\<^sub>r polyn_expr R X n (n, f))
[PROOF STEP]
apply (frule sp_cf_pol_coeff[of "(n, f)" "g 0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (g 0); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R; pol_coeff S (sp_cf S (g 0) (n, f))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (g 0 \<cdot>\<^sub>r polyn_expr R X n (n, f))
[PROOF STEP]
apply (subst scalar_times_pol_expr[of "g 0" "(n, f)" n], assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (g 0); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R; pol_coeff S (sp_cf S (g 0) (n, f))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (sp_cf S (g 0) (n, f)))
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of "I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J"
        "polyn_expr R X n (sp_cf S (g 0) (n, f))" "sp_cf S (g 0) (n, f)"],
         assumption+,
         simp add:polyn_mem, simp add:sp_cf_pol_coeff,
         rule polyn_mem, simp add:sp_cf_pol_coeff,
         simp add:sp_cf_len, simp,
         simp add:sp_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); pol_coeff S (0, g); P_mod R S X J (g 0); Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R; pol_coeff S (sp_cf S (g 0) (n, f))\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (sp_cf S (g 0) (n, f)). snd (sp_cf S (g 0) (n, f)) j \<in> I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I "polyn_expr R X n (n, f)"
         "(n, f)"], assumption+, simp, simp,
        simp add:sp_cf_len, subst sp_cf_def, simp,
        simp add:P_mod_coeffTr[of J "g 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); \<forall>j\<le>n. f j \<in> I; pol_coeff S (0, g); g 0 \<in> J; Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R; pol_coeff S (sp_cf S (g 0) (n, f)); P_mod R S X I (polyn_expr R X n (n, f))\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. g 0 \<cdot>\<^sub>r\<^bsub>S\<^esub> f j \<in> I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, assumption,
        frule_tac h = "f j" in Ring.ideal_subset[of S I], assumption+,
        simp add:Ring.ring_tOp_commute[of S "g 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); pol_coeff S (0, g); g 0 \<in> J; Subring R S; Ring S; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; g 0 \<in> carrier S; g 0 \<in> carrier R; pol_coeff S (sp_cf S (g 0) (n, f)); P_mod R S X I (polyn_expr R X n (n, f)); j \<le> n; f j \<in> I; f j \<in> carrier S\<rbrakk> \<Longrightarrow> f j \<cdot>\<^sub>r\<^bsub>S\<^esub> g 0 \<in> I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J
[PROOF STEP]
apply (simp add:Ring.prod_mem_prod_ideals[of S I J])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult_const1:"\<lbrakk>ideal S I; ideal S J;
       pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f));
       d \<in> J\<rbrakk> \<Longrightarrow>
       P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) ((polyn_expr R X n (n, f)) \<cdot>\<^sub>r d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); d \<in> J\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r d)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); d \<in> J; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r d)
[PROOF STEP]
apply (frule P_mod_coeffTr[THEN sym, of J d],
       simp add:Ring.ideal_subset, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); P_mod R S X J d; Subring R S; Ring S; d \<in> J\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r d)
[PROOF STEP]
apply (frule P_mod_mult_const[of I J n f "\<lambda>j. d"], assumption+,
       simp add:pol_coeff_def, simp add:Ring.ideal_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); P_mod R S X J d; Subring R S; Ring S; d \<in> J\<rbrakk> \<Longrightarrow> P_mod R S X J (polyn_expr R X 0 (0, \<lambda>j. d))
 2. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); P_mod R S X J d; Subring R S; Ring S; d \<in> J; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, \<lambda>j. d))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r d)
[PROOF STEP]
apply (subst polyn_expr_def, simp,
       frule Ring.ideal_subset[of S  J d], assumption+,
       frule mem_subring_mem_ring[of S d], assumption,
       simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); P_mod R S X J d; Subring R S; Ring S; d \<in> J; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, \<lambda>j. d))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r d)
[PROOF STEP]
apply (simp add:polyn_expr_def[of _ _ 0],
       frule Ring.ideal_subset[of S  J d], assumption+,
       frule mem_subring_mem_ring[of S d], assumption,
       simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult_monomial:"\<lbrakk>ideal S I; p \<in> carrier R\<rbrakk> \<Longrightarrow>
           (P_mod R S X I p ) = (P_mod R S X I (p \<cdot>\<^sub>r X^\<^bsup>R m\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X I p = P_mod R S X I (p \<cdot>\<^sub>r X^\<^bsup>R m\<^esup>)
[PROOF STEP]
apply (cut_tac X_mem_R,
       cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X I p = P_mod R S X I (p \<cdot>\<^sub>r X^\<^bsup>R m\<^esup>)
[PROOF STEP]
apply (frule npClose[of X m],
       simp add:ring_tOp_commute[of p ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X I p = P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X I p = P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+,
       cut_tac low_deg_terms_zero[THEN sym, of "fst (s_cf R S X p)"
               "snd (s_cf R S X p)" m],
       simp add:polyn_expr_split[THEN sym],
       thin_tac "X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p =
       polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p))",
       frule ext_cf_pol_coeff[of "s_cf R S X p" m])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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>; pol_coeff S (ext_cf S m (s_cf R S X p))\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p)))
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 3. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I 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 (3 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; 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>; pol_coeff S (ext_cf S m (s_cf R S X p)); P_mod R S X I p\<rbrakk> \<Longrightarrow> P_mod R S X I (polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p)))
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 3. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I "polyn_expr R X (fst (s_cf R S X p) +
          m) (ext_cf S m (s_cf R S X p))" "ext_cf S m (s_cf R S X p)"],
       rule polyn_mem, assumption, simp add:ext_cf_def,
       assumption, simp add:ext_cf_len add.commute, simp,
       thin_tac "P_mod R S X I (polyn_expr R X (fst (s_cf R S X p) + m)
        (ext_cf S m (s_cf R S X p))) = (\<forall>j\<le>fst (ext_cf S m (s_cf R S X p)).
         snd (ext_cf S m (s_cf R S X p)) j \<in> I)",
       thin_tac "snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; pol_coeff S (s_cf R S X p); pol_coeff S (ext_cf S m (s_cf R S X p)); P_mod R S X I p\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (ext_cf S m (s_cf R S X p)). snd (ext_cf S m (s_cf R S X p)) j \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 3. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (rule allI, rule impI, simp add:ext_cf_len)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; pol_coeff S (s_cf R S X p); pol_coeff S (ext_cf S m (s_cf R S X p)); P_mod R S X I p; j \<le> m + fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (ext_cf S m (s_cf R S X p)) j \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 3. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (
       subst ext_cf_def, simp add:sliden_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; pol_coeff S (s_cf R S X p); pol_coeff S (ext_cf S m (s_cf R S X p)); P_mod R S X I p; j \<le> m + fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> \<not> m \<le> j \<longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 3. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (rule impI,
       simp add:Ring.ideal_zero[of S])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I p; 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (simp add:pol_coeff_split[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p)\<rbrakk> \<Longrightarrow> P_mod R S X I p
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+,
       cut_tac low_deg_terms_zero[THEN sym, of "fst (s_cf R S X p)"
               "snd (s_cf R S X p)" m],
       simp add:polyn_expr_split[THEN sym],
       thin_tac "X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p =
       polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p))",
       frule ext_cf_pol_coeff[of "s_cf R S X p" m])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p))); 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>; pol_coeff S (ext_cf S m (s_cf R S X p))\<rbrakk> \<Longrightarrow> P_mod R S X I p
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p); 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
[PROOF STEP]
apply (frule P_mod_mod[THEN sym, of I "polyn_expr R X (fst (s_cf R S X p) +
          m) (ext_cf S m (s_cf R S X p))" "ext_cf S m (s_cf R S X p)"],
       rule polyn_mem, assumption, simp add:ext_cf_def,
       assumption, simp add:ext_cf_len add.commute, simp,
       thin_tac "p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)",
       thin_tac "P_mod R S X I
       (polyn_expr R X (fst (s_cf R S X p) + m) (ext_cf S m (s_cf R S X p)))",
       thin_tac "snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>fst (ext_cf S m (s_cf R S X p)). snd (ext_cf S m (s_cf R S X p)) j \<in> I; pol_coeff S (s_cf R S X p); pol_coeff S (ext_cf S m (s_cf R S X p))\<rbrakk> \<Longrightarrow> P_mod R S X I p
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p); 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of I p "s_cf R S X p"], assumption+,
       cut_tac s_cf_expr[of p], simp, assumption+,
       rule allI, rule impI,
       thin_tac "pol_coeff S (ext_cf S m (s_cf R S X p))",
       simp add:ext_cf_len, simp add:ext_cf_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; \<forall>j\<le>m + fst (s_cf R S X p). (if m \<le> j then snd (s_cf R S X p) (sliden m j) else \<zero>\<^bsub>S\<^esub>) \<in> I; pol_coeff S (s_cf R S X p); j \<le> fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) j \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p); 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
[PROOF STEP]
apply (drule_tac x = "m + j" in spec,
       frule_tac i = j and j = "fst (s_cf R S X p)" and k = m and l = m in
       add_le_mono, simp, simp only:add.commute[of _ m],
       thin_tac "j \<le> fst (s_cf R S X p)", simp,
       simp add:sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; X \<in> carrier R; Subring R S; Ring S; X^\<^bsup>R m\<^esup> \<in> carrier R; p \<noteq> \<zero>; P_mod R S X I (X^\<^bsup>R m\<^esup> \<cdot>\<^sub>r p); 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> pol_coeff S (fst (s_cf R S X p), snd (s_cf R S X p))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_multTr:"\<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f);
       P_mod R S X I (polyn_expr R X n (n, f))\<rbrakk> \<Longrightarrow> \<forall>g. ((pol_coeff S (m, g)
       \<and> (P_mod R S X J (polyn_expr R X m (m, g))))  \<longrightarrow>
          P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J)
           ((polyn_expr R X n (n, f)) \<cdot>\<^sub>r (polyn_expr R X m (m, g))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f))\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag, cut_tac X_mem_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (frule polyn_mem[of "(n, f)" n], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (frule Ring.ideal_prod_ideal[of "S" "I" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J)\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (case_tac "polyn_expr R X n (n, f) = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I \<zero>; Subring R S; Ring S; aGroup R; X \<in> carrier R; \<zero> \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) = \<zero>\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (\<zero> \<cdot>\<^sub>r polyn_expr R X m (m, g))
 2. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I \<zero>; Subring R S; Ring S; aGroup R; X \<in> carrier R; \<zero> \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) = \<zero>; pol_coeff S (m, g); P_mod R S X J (polyn_expr R X m (m, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (\<zero> \<cdot>\<^sub>r polyn_expr R X m (m, g))
 2. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (frule_tac c = "(m, g)" in polyn_mem[of _ m], simp,
        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; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (m, g) \<and> P_mod R S X J (polyn_expr R X m (m, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X m (m, g))
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (0, g) \<and> P_mod R S X J (polyn_expr R X 0 (0, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X 0 (0, g))
 2. \<And>na. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; \<forall>g. pol_coeff S (na, g) \<and> P_mod R S X J (polyn_expr R X na (na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (Suc na, g) \<and> P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
apply (rule allI, rule impI, erule conjE,
        rule_tac g = g in P_mod_mult_const[of I J n f], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; \<forall>g. pol_coeff S (na, g) \<and> P_mod R S X J (polyn_expr R X na (na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (Suc na, g) \<and> P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
(* case m = 0 done *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; \<forall>g. pol_coeff S (na, g) \<and> P_mod R S X J (polyn_expr R X na (na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> \<forall>g. pol_coeff S (Suc na, g) \<and> P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; \<forall>g. pol_coeff S (na, g) \<and> P_mod R S X J (polyn_expr R X na (na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
apply (frule_tac n = na and f = g in pol_coeff_pre,
       frule_tac n = na and f = g in P_mod_pre[of J], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; \<forall>g. pol_coeff S (na, g) \<and> P_mod R S X J (polyn_expr R X na (na, g)) \<longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
apply (drule_tac a = g in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X (Suc na) (Suc na, g))
[PROOF STEP]
apply (frule_tac n = na and f = g in polyn_Suc_split, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X (Suc na) (Suc na, g) = polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
[PROOF STEP]
apply (thin_tac "polyn_expr R X (Suc na) (Suc na, g) =
        polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R (Suc na)\<^esup>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
[PROOF STEP]
apply (frule_tac c = "(na, g)" and k = na in polyn_mem, simp,
       subgoal_tac "(g (Suc na)) \<cdot>\<^sub>r (X^\<^bsup>R (Suc na)\<^esup>) \<in> carrier R",
       subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (frule_tac p = "(polyn_expr R X n (n, f)) \<cdot>\<^sub>r (polyn_expr R X na (na, g))"
       and  q = "(polyn_expr R X n (n, f)) \<cdot>\<^sub>r
                      ((g (Suc na)) \<cdot>\<^sub>r (X^\<^bsup>R (Suc na)\<^esup>))" in
        P_mod_add[of "I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<in> carrier R
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>) \<in> carrier R
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))
 4. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 5. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 6. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (simp add:ring_tOp_closed, rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (frule_tac c = "(Suc na, g)" and j = "Suc na" in pol_coeff_mem_R,
        simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; snd (Suc na, g) (Suc na) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (subst ring_tOp_assoc[THEN sym], assumption+, simp,
        rule npClose, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; snd (Suc na, g) (Suc na) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>)
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (subst P_mod_mult_monomial[THEN sym, of "I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J"], assumption,
       rule ring_tOp_closed, assumption+, simp add:pol_coeff_mem_R)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; snd (Suc na, g) (Suc na) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r g (Suc na))
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (rule P_mod_mult_const1, assumption+,
       thin_tac "P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J)
         (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; snd (Suc na, g) (Suc na) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<in> J
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (cut_tac n1 = na and c1 = "(Suc na, g)" in polyn_Suc[THEN sym], simp,
        simp,
        frule_tac c = "(Suc na, g)" and k = na in polyn_expr_short,
        simp,  simp,
              thin_tac "P_mod R S X J (polyn_expr R X na (na, g))",
              thin_tac "polyn_expr R X na (na, g) \<in> carrier R",
              thin_tac "polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r (X^\<^bsup>R na\<^esup> \<cdot>\<^sub>r X)
                       =  polyn_expr R X (Suc na) (Suc na, g)",
              thin_tac "polyn_expr R X na (Suc na, g) =
                                         polyn_expr R X na (na, g)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X (Suc na) (Suc na, g)); pol_coeff S (na, g); g (Suc na) \<cdot>\<^sub>r (X^\<^bsup>R na\<^esup> \<cdot>\<^sub>r X) \<in> carrier R; g (Suc na) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<in> J
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 3. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (frule_tac p1 = "polyn_expr R X (Suc na) (Suc na, g)" and
                c1 = "(Suc na, g)" in P_mod_mod[THEN sym, of J],
        simp add:polyn_mem, assumption, simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R; g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R; P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g) \<plusminus> polyn_expr R X n (n, f) \<cdot>\<^sub>r (g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>))
 2. \<And>na g. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, f); P_mod R S X I (polyn_expr R X n (n, f)); Subring R S; Ring S; aGroup R; X \<in> carrier R; polyn_expr R X n (n, f) \<in> carrier R; ideal S (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J); polyn_expr R X n (n, f) \<noteq> \<zero>; pol_coeff S (Suc na, g); P_mod R S X J (polyn_expr R X na (na, g) \<plusminus> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup>); pol_coeff S (na, g); P_mod R S X J (polyn_expr R X na (na, g)); P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, f) \<cdot>\<^sub>r polyn_expr R X na (na, g)); polyn_expr R X na (na, g) \<in> carrier R\<rbrakk> \<Longrightarrow> g (Suc na) \<cdot>\<^sub>r X^\<^bsup>R Suc na\<^esup> \<in> carrier R
[PROOF STEP]
apply (simp,
        rule ring_tOp_closed,
        cut_tac c = "(Suc na, g)" and j = "Suc na" in pol_coeff_mem_R,
               assumption, simp, simp, rule npClose, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_mult:"\<lbrakk>ideal S I; ideal S J; pol_coeff S (n, c);
      pol_coeff S (m, d); P_mod R S X I (polyn_expr R X n (n, c));
      P_mod R S X J (polyn_expr R X m (m, d))\<rbrakk>  \<Longrightarrow>
      P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) ((polyn_expr R X n (n, c)) \<cdot>\<^sub>r
                                        (polyn_expr R X m (m, d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; ideal S J; pol_coeff S (n, c); pol_coeff S (m, d); P_mod R S X I (polyn_expr R X n (n, c)); P_mod R S X J (polyn_expr R X m (m, d))\<rbrakk> \<Longrightarrow> P_mod R S X (I \<diamondsuit>\<^sub>r\<^bsub>S\<^esub> J) (polyn_expr R X n (n, c) \<cdot>\<^sub>r polyn_expr R X m (m, d))
[PROOF STEP]
apply (simp add:P_mod_multTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done