[STATEMENT]
lemma (in PolynRg) erH_multTr1:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
      pol_coeff S c; pol_coeff S d;  pol_coeff S e; fst e = fst c + fst d;
    (polyn_expr R X (fst c) c) \<cdot>\<^sub>r (polyn_expr R X (fst d) d) =
     polyn_expr R X ((fst c) + (fst d)) e \<rbrakk> \<Longrightarrow>
 (polyn_expr A Y (fst c) (cf_h h c)) \<cdot>\<^sub>r\<^bsub>A\<^esub> (polyn_expr A Y (fst d) (cf_h h d))
  =  (polyn_expr A Y (fst e) (cf_h h e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; pol_coeff S e; fst e = fst c + fst d; polyn_expr R X (fst c) c \<cdot>\<^sub>r polyn_expr R X (fst d) d = polyn_expr R X (fst c + fst d) e\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) \<cdot>\<^sub>r\<^bsub>A\<^esub> polyn_expr A Y (fst d) (cf_h h d) = polyn_expr A Y (fst e) (cf_h h e)
[PROOF STEP]
by (cases d, cases e) (simp add: erH_multTr)


[STATEMENT]
lemma (in PolynRg) erHomTr0:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R\<rbrakk>
      \<Longrightarrow> erH R S X A B Y h (-\<^sub>a x) = -\<^sub>a\<^bsub>A\<^esub> (erH R S X A B Y h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h (-\<^sub>a x) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h x
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring, frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule Ring.ring_is_ag[of A],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h (-\<^sub>a x) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h x
[PROOF STEP]
apply (case_tac "x = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_inv_zero,
       simp add:erH_rHom_0[of A B Y h],
       frule Ring.ring_is_ag[of A], simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (-\<^sub>a x) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h x
[PROOF STEP]
apply (simp add:erH_def erh_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (-\<^sub>a x \<in> carrier R \<longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))) \<and> (-\<^sub>a x \<notin> carrier R \<longrightarrow> undefined = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (simp add:aGroup.ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (frule_tac p = x in s_cf_expr, assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (frule_tac x = x in aGroup.ag_mOp_closed, assumption+,
       frule_tac p = "-\<^sub>a x" in s_cf_expr,
       thin_tac "x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x)",
       rule contrapos_pp, simp+,
       frule_tac x = x in aGroup.ag_inv_inv, simp, simp add:aGroup.ag_inv_zero,
       (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); -\<^sub>a x = polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (frule_tac c = "s_cf R S X (-\<^sub>a x)" in cf_h_coeff[of A B Y h],
         assumption+,
         frule_tac c = "s_cf R S X x" in cf_h_coeff[of A B Y h],
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); -\<^sub>a x = polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (frule polyn_minus_m_cf[of "s_cf R S X x" "fst (s_cf R S X x)"],
          simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); -\<^sub>a x = polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); -\<^sub>a polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (cut_tac a = "-\<^sub>a x" and
          b = "polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x))"
     and  c = "polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x))"
          in box_equation, assumption, simp,
          thin_tac "x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x)",
          thin_tac "-\<^sub>a x =
         polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x))",
          thin_tac "-\<^sub>a (polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x)) =
         polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x))",
         frule m_cf_pol_coeff[of "s_cf R S X x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = -\<^sub>a\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x))
[PROOF STEP]
apply (subst PolynRg.polyn_minus_m_cf[of A B Y], assumption+,
         simp add:cf_h_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x)) (m_cf B (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (frule_tac c = "cf_h h (s_cf R S X x)" in
                   PolynRg.m_cf_pol_coeff[of A B Y], assumption,
         frule PolynRg.pol_expr_unique2[of A B Y "cf_h h (s_cf R S X (-\<^sub>a x))"
         "m_cf B (cf_h h (s_cf R S X x))"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x)))\<rbrakk> \<Longrightarrow> fst (cf_h h (s_cf R S X (-\<^sub>a x))) = fst (m_cf B (cf_h h (s_cf R S X x)))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); (polyn_expr A Y (fst (cf_h h (s_cf R S X (-\<^sub>a x)))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (m_cf B (cf_h h (s_cf R S X x)))) (m_cf B (cf_h h (s_cf R S X x)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (-\<^sub>a x))). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (m_cf B (cf_h h (s_cf R S X x))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x)) (m_cf B (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (simp add:cf_h_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x)))\<rbrakk> \<Longrightarrow> fst (s_cf R S X (-\<^sub>a x)) = fst (m_cf B (cf_h h (s_cf R S X x)))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); (polyn_expr A Y (fst (cf_h h (s_cf R S X (-\<^sub>a x)))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (m_cf B (cf_h h (s_cf R S X x)))) (m_cf B (cf_h h (s_cf R S X x)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (-\<^sub>a x))). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (m_cf B (cf_h h (s_cf R S X x))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x)) (m_cf B (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (simp add:PolynRg.m_cf_len cf_h_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x)))\<rbrakk> \<Longrightarrow> fst (s_cf R S X (-\<^sub>a x)) = fst (s_cf R S X x)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); (polyn_expr A Y (fst (cf_h h (s_cf R S X (-\<^sub>a x)))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (m_cf B (cf_h h (s_cf R S X x)))) (m_cf B (cf_h h (s_cf R S X x)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (-\<^sub>a x))). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (m_cf B (cf_h h (s_cf R S X x))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x)) (m_cf B (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (simp add:s_cf_deg[THEN sym, of x],
         cut_tac ring_zero,
         frule aGroup.ag_inv_inj[of R x \<zero>], assumption+,
         simp only:aGroup.ag_inv_zero,
         subst s_cf_deg[THEN sym, of "-\<^sub>a x"], assumption+,
         simp add:deg_minus_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); (polyn_expr A Y (fst (cf_h h (s_cf R S X (-\<^sub>a x)))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (m_cf B (cf_h h (s_cf R S X x)))) (m_cf B (cf_h h (s_cf R S X x)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (-\<^sub>a x))). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (m_cf B (cf_h h (s_cf R S X x))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x))) (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x)) (m_cf B (cf_h h (s_cf R S X x)))
[PROOF STEP]
apply (simp add:cf_h_len PolynRg.m_cf_len,
         thin_tac "(polyn_expr A Y (fst (s_cf R S X (-\<^sub>a x)))
         (cf_h h (s_cf R S X (-\<^sub>a x))) = polyn_expr A Y (fst (s_cf R S X x))
         (m_cf B (cf_h h (s_cf R S X x)))) =
         (\<forall>j\<le>fst (s_cf R S X (-\<^sub>a x)). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j =
          snd (m_cf B (cf_h h (s_cf R S X x))) j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x)))\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X (-\<^sub>a x)). snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (m_cf B (cf_h h (s_cf R S X x))) j
[PROOF STEP]
apply (rule allI, rule impI,
          subst m_cf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); j \<le> fst (s_cf R S X (-\<^sub>a x))\<rbrakk> \<Longrightarrow> snd (cf_h h (s_cf R S X (-\<^sub>a x))) j = snd (fst (cf_h h (s_cf R S X x)), \<lambda>j. -\<^sub>a\<^bsub>B\<^esub> snd (cf_h h (s_cf R S X x)) j) j
[PROOF STEP]
apply ((subst cf_h_def)+, simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x))); pol_coeff B (cf_h h (s_cf R S X x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); pol_coeff B (m_cf B (cf_h h (s_cf R S X x))); j \<le> fst (s_cf R S X (-\<^sub>a x))\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X (-\<^sub>a x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (thin_tac "snd (s_cf R S X (-\<^sub>a x)) (fst (s_cf R S X (-\<^sub>a x))) \<noteq> \<zero>\<^bsub>S\<^esub>",
          thin_tac "pol_coeff B (cf_h h (s_cf R S X (-\<^sub>a x)))",
          thin_tac "pol_coeff B (cf_h h (s_cf R S X x))",
          thin_tac "pol_coeff B (m_cf B (cf_h h (s_cf R S X x)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); j \<le> fst (s_cf R S X (-\<^sub>a x))\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X (-\<^sub>a x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (frule m_cf_pol_coeff[of "s_cf R S X x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); j \<le> fst (s_cf R S X (-\<^sub>a x)); pol_coeff S (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X (-\<^sub>a x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (frule pol_expr_unique2[of "s_cf R S X (-\<^sub>a x)"
                    "m_cf S (s_cf R S X x)"], assumption+,
          simp add:m_cf_len cf_h_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); j \<le> fst (s_cf R S X (-\<^sub>a x)); pol_coeff S (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> fst (s_cf R S X (-\<^sub>a x)) = fst (s_cf R S X x)
 2. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); pol_coeff S (m_cf S (s_cf R S X x)); j \<le> fst (s_cf R S X (-\<^sub>a x)); pol_coeff S (m_cf S (s_cf R S X x)); (polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (m_cf S (s_cf R S X x))) (m_cf S (s_cf R S X x))) = (\<forall>j\<le>fst (s_cf R S X (-\<^sub>a x)). snd (s_cf R S X (-\<^sub>a x)) j = snd (m_cf S (s_cf R S X x)) j)\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X (-\<^sub>a x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (simp add:s_cf_deg[THEN sym, of x],
         cut_tac ring_zero,
         frule aGroup.ag_inv_inj[of R x \<zero>], assumption+,
         simp only:aGroup.ag_inv_zero,
         subst s_cf_deg[THEN sym, of "-\<^sub>a x"], assumption+,
         simp add:deg_minus_eq, simp add:m_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); polyn_expr R X (fst (s_cf R S X (-\<^sub>a x))) (s_cf R S X (-\<^sub>a x)) = polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x)); j \<le> fst (s_cf R S X (-\<^sub>a x)); pol_coeff S (m_cf S (s_cf R S X x)); \<forall>j\<le>fst (s_cf R S X (-\<^sub>a x)). snd (s_cf R S X (-\<^sub>a x)) j = snd (m_cf S (s_cf R S X x)) j\<rbrakk> \<Longrightarrow> h (snd (m_cf S (s_cf R S X x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (drule_tac a = j in forall_spec, assumption,
         thin_tac "snd (s_cf R S X (-\<^sub>a x)) j = snd (m_cf S (s_cf R S X x)) j",
         thin_tac "polyn_expr R X (fst (s_cf R S X (-\<^sub>a x)))
         (s_cf R S X (-\<^sub>a x)) =
         polyn_expr R X (fst (s_cf R S X x)) (m_cf S (s_cf R S X x))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); j \<le> fst (s_cf R S X (-\<^sub>a x)); pol_coeff S (m_cf S (s_cf R S X x))\<rbrakk> \<Longrightarrow> h (snd (m_cf S (s_cf R S X x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (cut_tac ring_zero,
         frule aGroup.ag_inv_inj[of R x \<zero>], assumption+,
         simp only:aGroup.ag_inv_zero,
           (simp add:s_cf_deg[THEN sym, of "-\<^sub>a x"] deg_minus_eq,
             simp add:s_cf_deg[of x]) )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); j \<le> fst (s_cf R S X x); pol_coeff S (m_cf S (s_cf R S X x)); \<zero> \<in> carrier R; -\<^sub>a x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> h (snd (m_cf S (s_cf R S X x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of "s_cf R S X x"],
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); j \<le> fst (s_cf R S X x); pol_coeff S (m_cf S (s_cf R S X x)); \<zero> \<in> carrier R; -\<^sub>a x \<noteq> \<zero>; snd (s_cf R S X x) j \<in> carrier S\<rbrakk> \<Longrightarrow> h (snd (m_cf S (s_cf R S X x)) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (subst m_cf_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; x \<in> carrier R; aGroup R; Subring R S; Ring S; Ring A; aGroup A; Subring A B; Ring B; x \<noteq> \<zero>; pol_coeff S (s_cf R S X x); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; -\<^sub>a x \<in> carrier R; pol_coeff S (s_cf R S X (-\<^sub>a x)); j \<le> fst (s_cf R S X x); pol_coeff S (m_cf S (s_cf R S X x)); \<zero> \<in> carrier R; -\<^sub>a x \<noteq> \<zero>; snd (s_cf R S X x) j \<in> carrier S\<rbrakk> \<Longrightarrow> h (-\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X x) j) = -\<^sub>a\<^bsub>B\<^esub> h (snd (s_cf R S X x) j)
[PROOF STEP]
apply (simp add:rHom_inv_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erHomTr1:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
      a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>;
      deg_n R S X a = deg_n R S X b\<rbrakk> \<Longrightarrow>
      erH R S X A B Y h (a \<plusminus> b) = erH R S X A B Y h a \<plusminus>\<^bsub>A\<^esub>
                                             (erH R S X A B Y h b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; deg_n R S X a = deg_n R S X b\<rbrakk> \<Longrightarrow> erH R S X A B Y h (a \<plusminus> b) = erH R S X A B Y h a \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h b
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring, frule subring_Ring,
       frule PolynRg.subring[of A B Y],
       frule_tac x = a and y = b in aGroup.ag_pOp_closed[of "R"],
       assumption+,
       simp add:erH_def erh_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; deg_n R S X a = deg_n R S X b; aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X a)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply (frule s_cf_expr[of a], assumption,
       frule s_cf_expr[of b], assumption,
       frule s_cf_expr[of "a \<plusminus> b"], assumption,
       (erule conjE)+,
       simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); a = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X a); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; b = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X b); snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; a \<plusminus> b = polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply (frule polyn_add1[of "s_cf R S X a" "s_cf R S X b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); a = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X a); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; b = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X b); snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; a \<plusminus> b = polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X a)) (s_cf R S X a) \<plusminus> polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X b) = polyn_expr R X (max (fst (s_cf R S X a)) (fst (s_cf R S X b))) (add_cf S (s_cf R S X a) (s_cf R S X b))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply (cut_tac a = "a \<plusminus> b" and
       b = "polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b))" and
       c = "polyn_expr R X (max (fst (s_cf R S X a)) (fst (s_cf R S X b)))
       (add_cf S (s_cf R S X a) (s_cf R S X b))" in box_equation,
       drule sym, drule sym, drule sym, simp,
       drule sym, drule sym, drule sym, simp,
       thin_tac "polyn_expr R X (fst (s_cf R S X a)) (s_cf R S X a) \<plusminus>
        polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X b) =
        polyn_expr R X (max (fst (s_cf R S X a)) (fst (s_cf R S X b)))
        (add_cf S (s_cf R S X a) (s_cf R S X b))",
       thin_tac "a = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X a)",
       thin_tac "b = polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X b)",
       thin_tac "a \<plusminus> b =
         polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (max (fst (s_cf R S X a)) (fst (s_cf R S X b))) (add_cf S (s_cf R S X a) (s_cf R S X b))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply (frule cf_h_coeff[of A B Y h "s_cf R S X a"], assumption+,
       frule cf_h_coeff[of A B Y h "s_cf R S X b"], assumption+,
       frule cf_h_coeff[of A B Y h "s_cf R S X (a \<plusminus> b)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b)))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a)) \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b))
[PROOF STEP]
apply (frule PolynRg.polyn_add1[of A B Y "cf_h h (s_cf R S X a)"
                                "cf_h h (s_cf R S X b)"], assumption+,
       simp add:cf_h_len,
       thin_tac "polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X a))
        \<plusminus>\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X b)) =
             polyn_expr A Y (fst (s_cf R S X b))
               (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))",
       frule PolynRg.add_cf_pol_coeff[of A B Y "cf_h h (s_cf R S X a)"
                "cf_h h (s_cf R S X b)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (case_tac "fst (s_cf R S X (a \<plusminus>\<^bsub>R\<^esub> b)) = fst (s_cf R S X b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique2[of A B Y "cf_h h (s_cf R S X (a \<plusminus> b))"
              "add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> fst (cf_h h (s_cf R S X (a \<plusminus> b))) = fst (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); (polyn_expr A Y (fst (cf_h h (s_cf R S X (a \<plusminus> b)))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (a \<plusminus> b))). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (simp add:cf_h_len add_cf_len,
              simp add:PolynRg.add_cf_len cf_h_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); (polyn_expr A Y (fst (cf_h h (s_cf R S X (a \<plusminus> b)))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) = (\<forall>j\<le>fst (cf_h h (s_cf R S X (a \<plusminus> b))). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (simp add:PolynRg.add_cf_len cf_h_len,
       thin_tac "(polyn_expr A Y (fst (s_cf R S X b)) (cf_h h (s_cf R S X
        (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b))
         (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) =
         (\<forall>j\<le>fst (s_cf R S X b).
          snd (cf_h h (s_cf R S X (a \<plusminus> b))) j =
          snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X b). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule pol_expr_unique2[of "s_cf R S X (a \<plusminus> b)"
              "add_cf S (s_cf R S X a) (s_cf R S X b)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (s_cf R S X a) (s_cf R S X b))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> fst (s_cf R S X (a \<plusminus> b)) = fst (add_cf S (s_cf R S X a) (s_cf R S X b))
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); (polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (add_cf S (s_cf R S X a) (s_cf R S X b))) (add_cf S (s_cf R S X a) (s_cf R S X b))) = (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X b). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (simp add:add_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> fst (s_cf R S X (a \<plusminus> b)) = fst (add_cf S (s_cf R S X a) (s_cf R S X b))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); (polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (add_cf S (s_cf R S X a) (s_cf R S X b))) (add_cf S (s_cf R S X a) (s_cf R S X b))) = (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X b). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (simp add:add_cf_len, simp add:add_cf_len,
       thin_tac "polyn_expr R X (fst (s_cf R S X b)) (s_cf R S X (a \<plusminus> b)) =
                 polyn_expr R X (fst (s_cf R S X b))
                 (add_cf S (s_cf R S X a) (s_cf R S X b))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); \<forall>j\<le>fst (s_cf R S X b). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X b). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (rule allI, rule impI,
       drule_tac a = j in forall_spec, assumption,
       subst add_cf_def, simp add:cf_h_len,
       (subst cf_h_def)+, (subst cmp_def)+, simp,
        thin_tac "snd (s_cf R S X (a \<plusminus> b)) j =
         snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); j \<le> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> h (snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j) = h (snd (s_cf R S X a) j) \<plusminus>\<^bsub>B\<^esub> h (snd (s_cf R S X b) j)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (subst add_cf_def, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) = fst (s_cf R S X b); j \<le> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X a) j \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X b) j) = h (snd (s_cf R S X a) j) \<plusminus>\<^bsub>B\<^esub> h (snd (s_cf R S X b) j)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of "s_cf R S X a"], simp,
       frule_tac j = j in pol_coeff_mem[of "s_cf R S X b"], simp,
       simp add:rHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule s_cf_deg[of a], assumption,
       frule s_cf_deg[of b], assumption,
       frule s_cf_deg[of "a \<plusminus> b"], assumption,
       frule deg_pols_add2[of a b], assumption+,
       simp add:deg_def, simp add:deg_def ale_natle,
       frule_tac m = "fst (s_cf R S X (a \<plusminus> b))" and n = "fst (s_cf R S X b)"
                 in noteq_le_less, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b)) = polyn_expr R X (fst (s_cf R S X b)) (add_cf S (s_cf R S X a) (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); fst (s_cf R S X (a \<plusminus> b)) \<noteq> fst (s_cf R S X b); deg_n R S X a = fst (s_cf R S X b); deg_n R S X b = fst (s_cf R S X b); deg_n R S X (a \<plusminus> b) = fst (s_cf R S X (a \<plusminus> b)); fst (s_cf R S X (a \<plusminus> b)) \<le> fst (s_cf R S X b); fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule pol_expr_unique3[of "s_cf R S X (a \<plusminus> b)"
              "add_cf S (s_cf R S X a) (s_cf R S X b)"],
       simp add:add_cf_pol_coeff,
       simp add:add_cf_len,
       simp add:add_cf_len,
       thin_tac "polyn_expr R X (fst (s_cf R S X (a \<plusminus> b))) (s_cf R S X (a \<plusminus> b))
        =  polyn_expr R X (fst (s_cf R S X b))
                           (add_cf S (s_cf R S X a) (s_cf R S X b))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff B (cf_h h (s_cf R S X a)); pol_coeff B (cf_h h (s_cf R S X b)); pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b))); pol_coeff B (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))); deg_n R S X a = fst (s_cf R S X b); deg_n R S X b = fst (s_cf R S X b); deg_n R S X (a \<plusminus> b) = fst (s_cf R S X (a \<plusminus> b)); fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j) \<and> (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b))) (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b)) (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique3[of A B Y "cf_h h (s_cf R S X (a \<plusminus> b))"
              "add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))"],
         assumption+,
       simp add:cf_h_len PolynRg.add_cf_len,
       simp add:PolynRg.add_cf_len cf_h_len,
       thin_tac "(polyn_expr A Y (fst (s_cf R S X (a \<plusminus> b)))
       (cf_h h (s_cf R S X (a \<plusminus> b))) = polyn_expr A Y (fst (s_cf R S X b))
       (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b)))) =
       ((\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)).
          snd (cf_h h (s_cf R S X (a \<plusminus> b))) j =
          snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j) \<and>
        (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)).
          snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j =
          \<zero>\<^bsub>B\<^esub>))",
        thin_tac "pol_coeff B (cf_h h (s_cf R S X a))",
        thin_tac "pol_coeff B (cf_h h (s_cf R S X b))",
        thin_tac "pol_coeff B (cf_h h (s_cf R S X (a \<plusminus> b)))",
        thin_tac "pol_coeff B (add_cf B (cf_h h (s_cf R S X a))
                                         (cf_h h (s_cf R S X b)))",
        thin_tac "deg_n R S X a = fst (s_cf R S X b)",
        thin_tac "deg_n R S X b = fst (s_cf R S X b)",
        thin_tac "deg_n R S X (a \<plusminus> b) = fst (s_cf R S X (a \<plusminus> b))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j) \<and> (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j) \<and> (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j = \<zero>\<^bsub>B\<^esub>)
[PROOF STEP]
apply (rule conjI, erule conjE,
      thin_tac "\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)).
         snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); \<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (cf_h h (s_cf R S X (a \<plusminus> b))) j = snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j) \<and> (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j = \<zero>\<^bsub>B\<^esub>
[PROOF STEP]
apply (rule allI, rule impI,
          drule_tac a = j in forall_spec, assumption,
          (subst cf_h_def)+, (subst cmp_def)+, simp,
          (subst add_cf_def)+, simp,
         frule_tac j = j in pol_coeff_mem[of "s_cf R S X a"], simp,
         frule_tac j = j in pol_coeff_mem[of "s_cf R S X b"], simp,
         simp add:rHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); (\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j = snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j) \<and> (\<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j = \<zero>\<^bsub>B\<^esub>
[PROOF STEP]
apply (erule conjE,
       thin_tac "\<forall>j\<le>fst (s_cf R S X (a \<plusminus> b)). snd (s_cf R S X (a \<plusminus> b)) j =
        snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (add_cf S (s_cf R S X a) (s_cf R S X b)) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); \<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf S (s_cf R S X a) (s_cf R S X b)) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)). snd (add_cf B (cf_h h (s_cf R S X a)) (cf_h h (s_cf R S X b))) j = \<zero>\<^bsub>B\<^esub>
[PROOF STEP]
apply (rule ballI,
         drule_tac x = j in bspec, assumption,
         simp add:add_cf_def cf_h_len,
         simp add:cf_h_def cmp_def,
         frule_tac j = j in pol_coeff_mem[of "s_cf R S X a"],
         simp add:nset_def,
         frule_tac j = j in pol_coeff_mem[of "s_cf R S X b"],
         simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>; fst (s_cf R S X a) = fst (s_cf R S X b); aGroup R; Subring R S; Ring S; Subring A B; a \<plusminus> b \<in> carrier R; pol_coeff S (s_cf R S X a); pol_coeff S (s_cf R S X b); pol_coeff S (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X a) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X b) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X a) (fst (s_cf R S X (a \<plusminus> b))) \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X b) (fst (s_cf R S X (a \<plusminus> b))) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X (a \<plusminus> b)) < fst (s_cf R S X b); j \<in> nset (Suc (fst (s_cf R S X (a \<plusminus> b)))) (fst (s_cf R S X b)); snd (s_cf R S X a) j \<plusminus>\<^bsub>S\<^esub> snd (s_cf R S X b) j = \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X a) j \<in> carrier S; snd (s_cf R S X b) j \<in> carrier S\<rbrakk> \<Longrightarrow> h (snd (s_cf R S X a) j) \<plusminus>\<^bsub>B\<^esub> h (snd (s_cf R S X b) j) = \<zero>\<^bsub>B\<^esub>
[PROOF STEP]
apply (subst rHom_add[THEN sym, of h S B], assumption+, simp,
         (frule PolynRg.is_Ring[of A B Y],
          frule Ring.subring_Ring[of A B], assumption),
         simp add:rHom_0_0[of S B])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done