[STATEMENT]
lemma (in PolynRg) erh_polyn_exprs:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
       pol_coeff S c; pol_coeff S d;
       polyn_expr R X (fst c) c = polyn_expr R X (fst d) d\<rbrakk>  \<Longrightarrow>
       erh R S X A B Y h (fst c) c  = erh R S X A B Y h (fst d) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> erh R S X A B Y h (fst c) c = erh R S X A B Y h (fst d) d
[PROOF STEP]
apply (cut_tac subring,
       frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> erh R S X A B Y h (fst c) c = erh R S X A B Y h (fst d) d
[PROOF STEP]
apply (simp add:erh_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (cut_tac less_linear[of "fst c" "fst d"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst c < fst d \<or> fst c = fst d \<or> fst d < fst c\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (erule disjE,
       frule pol_expr_unique3[of c d], assumption+, simp,
       thin_tac "polyn_expr R X (fst c) c = polyn_expr R X (fst d) d",
       frule cf_h_coeff[of A B Y h c], assumption+,
       frule cf_h_coeff[of A B Y h d], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; (\<forall>j\<le>fst c. snd c j = snd d j) \<and> (\<forall>j\<in>nset (Suc (fst c)) (fst d). snd d j = \<zero>\<^bsub>S\<^esub>); Subring R S; Ring S; Ring A; Subring A B; Ring B; fst c < fst d; pol_coeff B (cf_h h c); pol_coeff B (cf_h h d)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst c = fst d \<or> fst d < fst c\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique3[of A B Y "cf_h h c" "cf_h h d"],
        assumption+, simp add:cf_h_len, simp add:cf_h_len,
       thin_tac "(polyn_expr A Y (fst c) (cf_h h c) =
       polyn_expr A Y (fst d) (cf_h h d)) =
       ((\<forall>j\<le>fst c. snd (cf_h h c) j = snd (cf_h h d) j) \<and>
       (\<forall>j\<in>nset (Suc (fst c)) (fst d). snd (cf_h h d) j = \<zero>\<^bsub>B\<^esub>))",
       simp add:cf_h_def cmp_def, simp add:rHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst c = fst d \<or> fst d < fst c\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (erule disjE,
       frule pol_expr_unique2[of c d], assumption+, simp,
       thin_tac "polyn_expr R X (fst d) c = polyn_expr R X (fst d) d",
       frule cf_h_coeff[of A B Y h c], assumption+,
       frule cf_h_coeff[of A B Y h d], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst c = fst d; \<forall>j\<le>fst d. snd c j = snd d j; pol_coeff B (cf_h h c); pol_coeff B (cf_h h d)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst d) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst d < fst c\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique2[of A B Y "cf_h h c" "cf_h h d"],
        assumption+, simp add:cf_h_len, simp add:cf_h_len,
       thin_tac "(polyn_expr A Y (fst d) (cf_h h c) =
        polyn_expr A Y (fst d) (cf_h h d)) =
       (\<forall>j\<le>fst d. snd (cf_h h c) j = snd (cf_h h d) j)",
        simp add:cf_h_def cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; polyn_expr R X (fst c) c = polyn_expr R X (fst d) d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst d < fst c\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst c) (cf_h h c) = polyn_expr A Y (fst d) (cf_h h d)
[PROOF STEP]
apply (drule sym, rule sym,
       frule pol_expr_unique3[of d c], assumption+, simp,
       thin_tac "polyn_expr R X (fst d) d = polyn_expr R X (fst c) c",
       frule cf_h_coeff[of A B Y h c], assumption+,
       frule cf_h_coeff[of A B Y h d], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; pol_coeff S d; Subring R S; Ring S; Ring A; Subring A B; Ring B; fst d < fst c; (\<forall>j\<le>fst d. snd d j = snd c j) \<and> (\<forall>j\<in>nset (Suc (fst d)) (fst c). snd c j = \<zero>\<^bsub>S\<^esub>); pol_coeff B (cf_h h c); pol_coeff B (cf_h h d)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst d) (cf_h h d) = polyn_expr A Y (fst c) (cf_h h c)
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique3[of A B Y "cf_h h d" "cf_h h c"],
        assumption+, simp add:cf_h_len, simp add:cf_h_len,
       thin_tac "(polyn_expr A Y (fst d) (cf_h h d) =
       polyn_expr A Y (fst c) (cf_h h c)) =
       ((\<forall>j\<le>fst d. snd (cf_h h d) j = snd (cf_h h c) j) \<and>
       (\<forall>j\<in>nset (Suc (fst d)) (fst c). snd (cf_h h c) j = \<zero>\<^bsub>B\<^esub>))",
       simp add:cf_h_def cmp_def, simp add:rHom_0_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_0:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk>  \<Longrightarrow>
                   (erH R S X A B Y h) \<zero> = \<zero>\<^bsub>A\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<zero> = \<zero>\<^bsub>A\<^esub>
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac PolynRg.is_Ring[of A B Y],
       cut_tac PolynRg.subring[of A B Y],
       cut_tac Ring.subring_Ring[of A B])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<zero> = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (simp add:erH_def erh_def s_cf_def polyn_expr_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> (\<zero> \<in> carrier R \<longrightarrow> snd (cf_h h (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) 0 \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = \<zero>\<^bsub>A\<^esub>) \<and> (\<zero> \<notin> carrier R \<longrightarrow> undefined = \<zero>\<^bsub>A\<^esub>)
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (cut_tac ring_zero,
        simp add:cf_h_def cmp_def rHom_0_0,
        simp add:Ring.Subring_zero_ring_zero,
        frule Ring.ring_zero[of A], simp add:Ring.ring_r_one, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_mem:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R\<rbrakk> \<Longrightarrow>
               erH R S X A B Y h p \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h p \<in> carrier A
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac PolynRg.is_Ring[of A B Y],
       cut_tac PolynRg.subring[of A B Y],
       cut_tac Ring.subring_Ring[of A B])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h p \<in> carrier A
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p = \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h p \<in> carrier A
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h p \<in> carrier A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 6. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (simp add:erH_rHom_0, simp add:Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h p \<in> carrier A
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (simp add:erH_def erh_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X p)) (cf_h h (s_cf R S X p)) \<in> carrier A
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X p)) (cf_h h (s_cf R S X p)) \<in> carrier A
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (rule PolynRg.polyn_mem[of A B Y "cf_h h (s_cf R S X p)"], assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff B (cf_h h (s_cf R S X p))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) \<le> fst (cf_h h (s_cf R S X p))
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 6. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (simp add:cf_h_coeff)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B; Ring B; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) \<le> fst (cf_h h (s_cf R S X p))
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A; Subring A B\<rbrakk> \<Longrightarrow> Subring A B
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S; Ring A\<rbrakk> \<Longrightarrow> PolynRg A B Y
 5. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> PolynRg A B Y
[PROOF STEP]
apply (simp add:cf_h_len, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_nonzero:"\<lbrakk>PolynRg A B Y; f \<in> rHom S B;
      p \<in> carrier R; (erH R S X A B Y f) p \<noteq> \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; p \<in> carrier R; erH R S X A B Y f p \<noteq> \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; \<zero> \<in> carrier R; erH R S X A B Y f \<zero> \<noteq> \<zero>\<^bsub>A\<^esub>; p = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:erH_rHom_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHomTr2:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk>  \<Longrightarrow>
        (erH R S X A B Y h) (1\<^sub>r) = (1\<^sub>r\<^bsub>A\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption,
       cut_tac polyn_ring_nonzero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
[PROOF STEP]
apply (cut_tac Subring_one_ring_one[THEN sym, of S],
       frule Ring.ring_one[of S],
       cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (frule s_cf_expr[of "1\<^sub>r"], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r); 1\<^sub>r = polyn_expr R X (fst (s_cf R S X 1\<^sub>r)) (s_cf R S X 1\<^sub>r); snd (s_cf R S X 1\<^sub>r) (fst (s_cf R S X 1\<^sub>r)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> erH R S X A B Y h 1\<^sub>r = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (frule s_cf_deg[THEN sym, of "1\<^sub>r"], assumption, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> erH R S X A B Y h 1\<^sub>r\<^bsub>S\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (cut_tac pol_of_deg0[THEN sym, of "1\<^sub>r"], simp,
        simp add:erH_def erh_def cf_h_def polyn_expr_def,
        frule pol_coeff_mem[of "s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>" 0], simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) 0 \<cdot>\<^sub>r 1\<^sub>r\<^bsub>S\<^esub>; snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) 0 \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = 0; deg_n R S X 1\<^sub>r\<^bsub>S\<^esub> = 0; snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) 0 \<in> carrier S\<rbrakk> \<Longrightarrow> cmp h (snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>)) 0 \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (simp add:Subring_tOp_ring_tOp[THEN sym],
        simp add:Ring.ring_r_one cmp_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) 0; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = 0; deg_n R S X 1\<^sub>r\<^bsub>S\<^esub> = 0\<rbrakk> \<Longrightarrow> h 1\<^sub>r\<^bsub>S\<^esub> \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 4. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (simp add:rHom_one,
        simp add:Ring.Subring_one_ring_one[of A B],
               frule Ring.ring_one[of A], simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 3. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply (simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; 1\<^sub>r = 1\<^sub>r\<^bsub>S\<^esub>; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R; pol_coeff S (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); 1\<^sub>r\<^bsub>S\<^esub> = polyn_expr R X (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>); snd (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) (deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X 1\<^sub>r\<^bsub>S\<^esub>) = deg_n R S X 1\<^sub>r\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 2. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; 1\<^sub>r \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Subring R S
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done