[STATEMENT]
lemma (in PolynRg) erHomTr2:"\<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)+,
       frule polyn_deg_add1[of a b], assumption+,
       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 a)) (s_cf R S X a); snd (s_cf R S X a) (fst (s_cf R S X a)) \<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 b)) (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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 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 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 a)) (s_cf R S X a); snd (s_cf R S X a) (fst (s_cf R S X a)) \<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 b)) (s_cf R S X (a \<plusminus> b)); snd (s_cf R S X (a \<plusminus> b)) (fst (s_cf R S X b)) \<noteq> \<zero>\<^bsub>S\<^esub>; 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)) (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 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 (cut_tac a = "a \<plusminus> b" and
       b = "polyn_expr R X (fst (s_cf R S X 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 a)) (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 b))
                            (s_cf R S X (a \<plusminus> b))",
       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 a)) \<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>; 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 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 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 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 a)) \<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>; 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 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 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 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)
[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 a)) \<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>; 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 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))); 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)) = 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)))\<rbrakk> \<Longrightarrow> 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)))
[PROOF STEP]
apply (thin_tac "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)) =
        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 a)) \<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>; 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 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 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+,
       simp add:cf_h_len add_cf_len,
       simp add:PolynRg.add_cf_len cf_h_len,
       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 (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 a)) \<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>; 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 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> \<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 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)"],
       simp add:add_cf_pol_coeff,
       simp add:add_cf_len, simp add:add_cf_len)
[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 a)) \<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>; 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 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))); \<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
[PROOF STEP]
apply (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 (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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); \<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
[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,
        subst add_cf_def, simp)
[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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); 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> (j \<le> fst (s_cf R S X a) \<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)) \<and> (\<not> j \<le> fst (s_cf R S X a) \<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 b) j))
[PROOF STEP]
apply (case_tac "j \<le> fst (s_cf R S X a)", 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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); 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; j \<le> fst (s_cf R S X a)\<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. \<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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); 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; \<not> j \<le> fst (s_cf R S X a)\<rbrakk> \<Longrightarrow> (j \<le> fst (s_cf R S X a) \<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)) \<and> (\<not> j \<le> fst (s_cf R S X a) \<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 b) j))
[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. \<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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); 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; \<not> j \<le> fst (s_cf R S X a)\<rbrakk> \<Longrightarrow> (j \<le> fst (s_cf R S X a) \<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)) \<and> (\<not> j \<le> fst (s_cf R S X a) \<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 b) j))
[PROOF STEP]
apply simp
[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>; 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 a)) \<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>; fst (s_cf R S X (a \<plusminus> b)) = fst (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))); 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; \<not> j \<le> fst (s_cf R S X a)\<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 b) j)
[PROOF STEP]
apply (subst add_cf_def, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B\<rbrakk>
   \<Longrightarrow> erH R S X A B Y h \<in> pHom R S X, A B Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> pHom R S X, A B Y
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"],
       cut_tac subring,
       cut_tac polyn_ring_integral, simp,
       frule PolynRg.subring[of A B Y],
       frule PolynRg.is_Ring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> pHom R S X, A B Y
[PROOF STEP]
apply (simp add:polyn_Hom_def,
       rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h ` carrier S \<subseteq> carrier B \<and> erH R S X A B Y h X = Y
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h ` carrier S \<subseteq> carrier B \<and> erH R S X A B Y h X = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (cut_tac polyn_ring_X_nonzero,
       cut_tac X_mem_R, rule conjI,
       rule subsetI, simp add:image_def,
       erule bexE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; xa \<in> carrier S; x = erH R S X A B Y h xa\<rbrakk> \<Longrightarrow> x \<in> carrier B
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h X = Y
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (case_tac "xa = \<zero>\<^bsub>S\<^esub>",
       simp add:Subring_zero_ring_zero,
       simp add:erH_rHom_0,
       simp add:Ring.Subring_zero_ring_zero[THEN sym, of A B],
       simp add:Ring.ring_zero[of B])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; xa \<in> carrier S; x = erH R S X A B Y h xa; xa \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> x \<in> carrier B
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h X = Y
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (simp add:Subring_zero_ring_zero,
       frule_tac x = xa in mem_subring_mem_ring, assumption,
       frule_tac p = xa in s_cf_expr, assumption+, (erule conjE)+,
       frule_tac p1 = xa in s_cf_deg[THEN sym], assumption+,
       frule_tac p1 = xa in pol_of_deg0[THEN sym], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; deg_n R S X xa = 0; x = erH R S X A B Y h xa; xa \<noteq> \<zero>; xa \<in> carrier R; pol_coeff S (s_cf R S X xa); xa = polyn_expr R X 0 (s_cf R S X xa); snd (s_cf R S X xa) 0 \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X xa) = 0; xa \<in> carrier S\<rbrakk> \<Longrightarrow> erH R S X A B Y h xa \<in> carrier B
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h X = Y
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (simp add:erH_def erh_def, subst polyn_expr_def, simp,
       frule_tac c = "s_cf R S X xa" in cf_h_coeff[of A B Y h], assumption+,
       frule_tac c = "cf_h h (s_cf R S X xa)" and j = 0 in
                         PolynRg.pol_coeff_mem[of A B Y], assumption, simp,
       frule_tac c = "cf_h h (s_cf R S X xa)" and j = 0 in
                         PolynRg.pol_coeff_mem_R[of A B Y], assumption, simp,
       simp add:Ring.ring_r_one[of A])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h X = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (cut_tac pol_expr_of_X,
       cut_tac special_cf_pol_coeff,
       frule ext_cf_pol_coeff[of "C\<^sub>0 S" "Suc 0"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> erH R S X A B Y h X = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (simp add:erH_def erh_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X X)) (cf_h h (s_cf R S X X)) = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (cut_tac deg_n_of_X)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); deg_n R S X X = Suc 0\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X X)) (cf_h h (s_cf R S X X)) = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (frule s_cf_expr[of X], assumption+, (erule conjE)+,
        frule_tac a = X and
        b = "polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))" and
        c = "polyn_expr R X (fst (s_cf R S X X)) (s_cf R S X X)" in
        box_equation, assumption+,
        thin_tac "X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))",
        thin_tac "X = polyn_expr R X (fst (s_cf R S X X)) (s_cf R S X X)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); deg_n R S X X = Suc 0; 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>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (fst (s_cf R S X X)) (s_cf R S X X)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X X)) (cf_h h (s_cf R S X X)) = Y
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (rule sym, subst PolynRg.pol_expr_of_X[of A B Y], assumption+,
        frule s_cf_deg[of X], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (frule pol_expr_unique2[of "ext_cf S (Suc 0) (C\<^sub>0 S)" "s_cf R S X X"],
        assumption+, simp add:ext_cf_len special_cf_len,
        simp add:ext_cf_len special_cf_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd (s_cf R S X X) j\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (frule cf_h_coeff[of A B Y h "ext_cf S (Suc 0) (C\<^sub>0 S)"], assumption+,
        frule cf_h_coeff[of A B Y h "s_cf R S X X"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd (s_cf R S X X) j; pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))); pol_coeff B (cf_h h (s_cf R S X X))\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique2[of A B Y
          "cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))" "cf_h h (s_cf R S X X)"],
        assumption+,
        simp add:cf_h_len ext_cf_len special_cf_len,
        simp add:cf_h_len ext_cf_len special_cf_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd (s_cf R S X X) j; pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))); pol_coeff B (cf_h h (s_cf R S X X)); (polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))) = (\<forall>j\<le>Suc 0. snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (cf_h h (s_cf R S X X)) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (simp add:cf_h_special_cf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd (s_cf R S X X) j; pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))); pol_coeff B (cf_h h (s_cf R S X X)); (polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) = polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))) = (\<forall>j\<le>Suc 0. snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (cf_h h (s_cf R S X X)) j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc 0. snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (cf_h h (s_cf R S X X)) j
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (thin_tac "(polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B)) =
        polyn_expr A Y (Suc 0) (cf_h h (s_cf R S X X))) =
         (\<forall>j\<le>Suc 0.
           snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j =
           snd (cf_h h (s_cf R S X X)) j)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; X \<noteq> \<zero>; X \<in> carrier R; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); fst (s_cf R S X X) = Suc 0; pol_coeff S (s_cf R S X X); snd (s_cf R S X X) (Suc 0) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) (s_cf R S X X); deg_n R S X X = Suc 0; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd (s_cf R S X X) j; pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))); pol_coeff B (cf_h h (s_cf R S X X))\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc 0. snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (cf_h h (s_cf R S X X)) j
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, assumption,
        (subst cf_h_def)+, (subst cmp_def)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (subst rHom_def, simp,
       cut_tac ring_is_ag,
       frule Ring.ring_is_ag[of A])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> aHom R A \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> aHom R A
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (subst aHom_def, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> carrier R \<rightarrow> carrier A \<and> erH R S X A B Y h \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. 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)
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> carrier R \<rightarrow> carrier A
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. 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)
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:erH_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. 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)
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (rule conjI, simp add:erH_def erh_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R. \<forall>b\<in>carrier R. 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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R\<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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (case_tac "a = \<zero>\<^bsub>R\<^esub>",
          case_tac "b = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; \<zero> \<in> carrier R; a = \<zero>; b = \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (\<zero> \<plusminus> \<zero>) = erH R S X A B Y h \<zero> \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h \<zero>
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a = \<zero>; b \<noteq> \<zero>\<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
 3. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>\<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
 4. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:erH_rHom_0,
         frule Ring.ring_is_ag[of A], frule Ring.ring_zero[of A],
         simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; \<zero> \<in> carrier R; a = \<zero>; b = \<zero>; aGroup A; \<zero>\<^bsub>A\<^esub> \<in> carrier A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<zero> = \<zero>\<^bsub>A\<^esub>
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a = \<zero>; b \<noteq> \<zero>\<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
 3. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>\<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
 4. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:erH_rHom_0, simp add:erH_rHom_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; \<zero> \<in> carrier R; b \<in> carrier R; a = \<zero>; b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (\<zero> \<plusminus> b) = \<zero>\<^bsub>A\<^esub> \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h b
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>\<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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (frule_tac p = b in erH_mem[of A B Y h], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; \<zero> \<in> carrier R; b \<in> carrier R; a = \<zero>; b \<noteq> \<zero>; erH R S X A B Y h b \<in> carrier A\<rbrakk> \<Longrightarrow> erH R S X A B Y h (\<zero> \<plusminus> b) = \<zero>\<^bsub>A\<^esub> \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h b
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>\<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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>\<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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (case_tac "b = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; \<zero> \<in> carrier R; a \<noteq> \<zero>; b = \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (a \<plusminus> \<zero>) = erH R S X A B Y h a \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h \<zero>
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>\<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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:erH_rHom_0,
          frule_tac p = a in erH_mem[of A B Y h], assumption+,
          simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>\<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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (case_tac "a \<plusminus>\<^bsub>R\<^esub> b = \<zero>\<^bsub>R\<^esub>", simp add:erH_rHom_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b = \<zero>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> = erH R S X A B Y h a \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h b
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>\<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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (frule_tac x = a and y = b in aGroup.ag_inv_unique[of R],
          assumption+, simp,
          thin_tac "b = -\<^sub>a a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; -\<^sub>a a \<in> carrier R; a \<noteq> \<zero>; -\<^sub>a a \<noteq> \<zero>; a \<plusminus> -\<^sub>a a = \<zero>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> = erH R S X A B Y h a \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h (-\<^sub>a a)
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>\<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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (subst erHomTr0[of A B Y h], assumption+,
          frule_tac p = a in erH_mem[of A B Y h], assumption+,
          simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; a \<in> carrier R; b \<in> carrier R; a \<noteq> \<zero>; b \<noteq> \<zero>; a \<plusminus> b \<noteq> \<zero>\<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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (case_tac "deg_n R S X a = deg_n R S X b",
          simp add:erHomTr1[of A B Y h])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; 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 \<noteq> 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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (cut_tac y = "deg_n R S X a" and x = "deg_n R S X b" in less_linear,
          simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; 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 \<noteq> deg_n R S X b; deg_n R S X b < deg_n R S X a \<or> 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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; 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 \<noteq> deg_n R S X b; deg_n R S X b < deg_n R S X a\<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
 2. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; 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 \<noteq> deg_n R S X b; 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
 3. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (subst aGroup.ag_pOp_commute, assumption+,
          frule_tac p = a in erH_mem[of A B Y h], assumption+,
          frule_tac p = b in erH_mem[of A B Y h], assumption+,
          subst aGroup.ag_pOp_commute[of A], assumption+,
          rule erHomTr2[of A B Y h], assumption+,
          simp add:aGroup.ag_pOp_commute, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; 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 \<noteq> deg_n R S X b; 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
 2. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply(rule erHomTr2[of A B Y h], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y) \<and> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (simp add:erH_rHomTr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (case_tac "x = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_0_x erH_rHom_0,
        frule_tac p = y in erH_mem[of A B Y h], assumption+,
        simp add:Ring.ring_times_0_x[of A])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (case_tac "y = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_x_0 erH_rHom_0,
        frule_tac p = x in erH_mem[of A B Y h], assumption+,
        simp add:Ring.ring_times_x_0[of A])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (frule_tac p = x in s_cf_expr, assumption+,
        frule_tac p = y in s_cf_expr, assumption+,
        frule_tac x = x and y = y in ring_tOp_closed, assumption+,
        frule_tac p = "x \<cdot>\<^sub>r y" in s_cf_expr,
        simp add:Idomain.idom_tOp_nonzeros, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (frule_tac c = "s_cf R S X x" and d = "s_cf R S X y" in
                  polyn_expr_tOp_c, assumption+, erule exE, (erule conjE)+,
        cut_tac a = "x \<cdot>\<^sub>r y" and
        b = "polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y))"
        and c = "polyn_expr R X (fst e) e" in box_equation)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y))
 2. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = polyn_expr R X (fst e) e
 3. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst e) e\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = polyn_expr R X (fst e) e
 2. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst e) e\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (thin_tac "x \<cdot>\<^sub>r y =
        polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = polyn_expr R X (fst e) e
 2. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst e) e\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (drule sym, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); 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>; y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; x \<cdot>\<^sub>r y = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst e) e\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply (thin_tac "x = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x)",
          thin_tac "y = polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)",
         thin_tac "x \<cdot>\<^sub>r y =
        polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst e) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst e) e\<rbrakk> \<Longrightarrow> erH R S X A B Y h (x \<cdot>\<^sub>r y) = erH R S X A B Y h x \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h y
[PROOF STEP]
apply ((subst erH_def)+, (subst erh_def)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>A\<^esub> polyn_expr A Y (fst (s_cf R S X y)) (cf_h h (s_cf R S X y))
[PROOF STEP]
apply (frule_tac c = "s_cf R S X x" and d = "s_cf R S X y" and e = e in
        erH_multTr1[of A B Y h], assumption+, simp, simp,
     thin_tac "polyn_expr A Y (fst (s_cf R S X x)) (cf_h h (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>A\<^esub>
     polyn_expr A Y (fst (s_cf R S X y)) (cf_h h (s_cf R S X y)) =
     polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp,
       thin_tac "polyn_expr R X (fst (s_cf R S X x)) (s_cf R S X x) \<cdot>\<^sub>r
        polyn_expr R X (fst (s_cf R S X y)) (s_cf R S X y) =
        polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y))",
       rotate_tac -1, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)
[PROOF STEP]
apply (frule_tac p = x in s_cf_deg, assumption,
         frule_tac p = y in s_cf_deg, assumption,
         frule_tac x = x and y = y in Idomain.idom_tOp_nonzeros[of R],
         assumption+,
         frule_tac p = "x \<cdot>\<^sub>r y" in s_cf_deg, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e; deg_n R S X x = fst (s_cf R S X x); deg_n R S X y = fst (s_cf R S X y); x \<cdot>\<^sub>r y \<noteq> \<zero>; deg_n R S X (x \<cdot>\<^sub>r y) = fst (s_cf R S X (x \<cdot>\<^sub>r y))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)
[PROOF STEP]
apply (frule_tac p = x and q = y in deg_mult_pols, assumption+,
         (erule conjE)+, simp,
         thin_tac "deg_n R S X x = fst (s_cf R S X x)",
         thin_tac "deg_n R S X y = fst (s_cf R S X y)",
         thin_tac "deg_n R S X (x \<cdot>\<^sub>r y) = fst (s_cf R S X (x \<cdot>\<^sub>r y))",
         rotate_tac -2, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>x \<cdot>\<^sub>r y \<noteq> \<zero>; Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X (x \<cdot>\<^sub>r y))) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X (x \<cdot>\<^sub>r y)); snd e (fst (s_cf R S X (x \<cdot>\<^sub>r y))) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X (x \<cdot>\<^sub>r y))) e; fst (s_cf R S X (x \<cdot>\<^sub>r y)) = fst (s_cf R S X x) + fst (s_cf R S X y)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X (x \<cdot>\<^sub>r y))) (cf_h h e)
[PROOF STEP]
apply (simp add:cf_h_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>x \<cdot>\<^sub>r y \<noteq> \<zero>; Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X x) + fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e; fst (s_cf R S X (x \<cdot>\<^sub>r y)) = fst (s_cf R S X x) + fst (s_cf R S X y)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)
[PROOF STEP]
apply (frule_tac c = "s_cf R S X (x \<cdot>\<^sub>r y)" in cf_h_coeff[of A B Y h],
          assumption+,
         frule_tac c = e in cf_h_coeff[of A B Y h], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>x \<cdot>\<^sub>r y \<noteq> \<zero>; Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X x) + fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e; fst (s_cf R S X (x \<cdot>\<^sub>r y)) = fst (s_cf R S X x) + fst (s_cf R S X y); pol_coeff B (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))); pol_coeff B (cf_h h e)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) = polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y)) (cf_h h e)
[PROOF STEP]
apply (frule_tac c = "cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))" and d = "cf_h h e" in
         PolynRg.pol_expr_unique2[of A B Y], assumption+,
         simp add:cf_h_len, simp add:cf_h_len,
         thin_tac "(polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y))
          (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) =
           polyn_expr A Y (fst (s_cf R S X x) + fst (s_cf R S X y))
          (cf_h h e)) =
          (\<forall>j\<le>fst (s_cf R S X x) + fst (s_cf R S X y).
            snd (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) j = snd (cf_h h e) j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>x \<cdot>\<^sub>r y \<noteq> \<zero>; Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X (x \<cdot>\<^sub>r y)) (fst (s_cf R S X x) + fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) (s_cf R S X (x \<cdot>\<^sub>r y)) = polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e; fst (s_cf R S X (x \<cdot>\<^sub>r y)) = fst (s_cf R S X x) + fst (s_cf R S X y); pol_coeff B (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))); pol_coeff B (cf_h h e)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X x) + fst (s_cf R S X y). snd (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) j = snd (cf_h h e) j
[PROOF STEP]
apply (frule_tac c = "s_cf R S X (x \<cdot>\<^sub>r y)" and d = e in
         pol_expr_unique2, assumption+, simp, simp,
         thin_tac "polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y))
         (s_cf R S X (x \<cdot>\<^sub>r y)) =
         polyn_expr R X (fst (s_cf R S X x) + fst (s_cf R S X y)) e")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y e. \<lbrakk>x \<cdot>\<^sub>r y \<noteq> \<zero>; Idomain R; PolynRg A B Y; h \<in> rHom S B; Ring S; Subring R S; Idomain S; Subring A B; Ring A; Ring B; aGroup R; aGroup A; x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y \<in> carrier R; pol_coeff S (s_cf R S X x); pol_coeff S (s_cf R S X y); pol_coeff S (s_cf R S X (x \<cdot>\<^sub>r y)); snd (s_cf R S X x) (fst (s_cf R S X x)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X x) + fst (s_cf R S X y); snd e (fst (s_cf R S X x) + fst (s_cf R S X y)) = snd (s_cf R S X x) (fst (s_cf R S X x)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X y) (fst (s_cf R S X y)); fst (s_cf R S X (x \<cdot>\<^sub>r y)) = fst (s_cf R S X x) + fst (s_cf R S X y); pol_coeff B (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))); pol_coeff B (cf_h h e); \<forall>j\<le>fst (s_cf R S X x) + fst (s_cf R S X y). snd (s_cf R S X (x \<cdot>\<^sub>r y)) j = snd e j\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X x) + fst (s_cf R S X y). snd (cf_h h (s_cf R S X (x \<cdot>\<^sub>r y))) j = snd (cf_h h e) j
[PROOF STEP]
apply (rule allI, rule impI, drule_tac a = j in forall_spec, assumption,
         subst cf_h_def, subst cmp_def, simp,
         subst cf_h_def, subst cmp_def, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_q_rHom:"\<lbrakk>Idomain S; maximal_ideal S P;
       PolynRg R' (S /\<^sub>r P) Y\<rbrakk> \<Longrightarrow>
       erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' (S /\<^sub>r P) Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; maximal_ideal S P; PolynRg R' (S /\<^sub>r P) Y\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r P) Y (pj S P) \<in> pHom R S X, R' S /\<^sub>r P Y
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"],
       frule Ring.qring_ring[of S P], simp add:Ring.maximal_ideal_ideal,
       rule erH_rHom[of R' "S /\<^sub>r P" Y "pj S P"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; maximal_ideal S P; PolynRg R' (S /\<^sub>r P) Y; Ring S; Ring (S /\<^sub>r P)\<rbrakk> \<Longrightarrow> pj S P \<in> rHom S (S /\<^sub>r P)
[PROOF STEP]
apply (rule pj_Hom[of S P], assumption+,
       simp add:Ring.maximal_ideal_ideal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_add:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B;
                   p \<in> carrier R; q \<in> carrier R\<rbrakk> \<Longrightarrow>
          erH R S X A B Y h (p \<plusminus> q) =
                 (erH R S X A B Y h p) \<plusminus>\<^bsub>A\<^esub> (erH R S X A B Y h q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; q \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h (p \<plusminus> q) = erH R S X A B Y h p \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h q
[PROOF STEP]
apply (frule erH_rHom[of A B Y h], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; q \<in> carrier R; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> erH R S X A B Y h (p \<plusminus> q) = erH R S X A B Y h p \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h q
[PROOF STEP]
apply (simp add:polyn_Hom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; q \<in> carrier R; erH R S X A B Y h \<in> rHom R A; erH R S X A B Y h ` carrier S \<subseteq> carrier B; erH R S X A B Y h X = Y\<rbrakk> \<Longrightarrow> erH R S X A B Y h (p \<plusminus> q) = erH R S X A B Y h p \<plusminus>\<^bsub>A\<^esub> erH R S X A B Y h q
[PROOF STEP]
apply (simp add:rHom_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done