[STATEMENT]
lemma (in PolynRg) erH_minus:"\<lbrakk>Idomain S; PolynRg A B Y;
       h \<in> rHom S B; p \<in> carrier R\<rbrakk> \<Longrightarrow>
        erH R S X A B Y h (-\<^sub>a p) = -\<^sub>a\<^bsub>A\<^esub> (erH R S X A B Y h p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h (-\<^sub>a p) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h p
[PROOF STEP]
apply (frule erH_rHom[of A B Y h], assumption+,
       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; 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 (-\<^sub>a p) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h p
[PROOF STEP]
apply (frule PolynRg.is_Ring[of A B Y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<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; Ring A\<rbrakk> \<Longrightarrow> erH R S X A B Y h (-\<^sub>a p) = -\<^sub>a\<^bsub>A\<^esub> erH R S X A B Y h p
[PROOF STEP]
apply (rule rHom_inv_inv[of R A p "erH R S X A B Y h"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<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; Ring A\<rbrakk> \<Longrightarrow> Ring R
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<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; Ring A\<rbrakk> \<Longrightarrow> Ring A
 3. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<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; Ring A\<rbrakk> \<Longrightarrow> p \<in> carrier R
 4. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; p \<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; Ring A\<rbrakk> \<Longrightarrow> erH R S X A B Y h \<in> rHom R A
[PROOF STEP]
apply (cut_tac is_Ring, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_mult:"\<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 \<cdot>\<^sub>r q) =
                 (erH R S X A B Y h p) \<cdot>\<^sub>r\<^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 \<cdot>\<^sub>r q) = erH R S X A B Y h p \<cdot>\<^sub>r\<^bsub>A\<^esub> erH R S X A B Y h q
[PROOF STEP]
apply (frule erH_rHom[of A B Y h], assumption+,
       simp add:polyn_Hom_def, (erule conjE)+,
       frule PolynRg.is_Ring[of A B Y],
       cut_tac is_Ring,
       rule rHom_tOp[of R A p q "erH R S X A B Y h"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_cf:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B;
                   s \<in> carrier S\<rbrakk>  \<Longrightarrow> erH R S X A B Y h s = h s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; s \<in> carrier S\<rbrakk> \<Longrightarrow> erH R S X A B Y h s = h s
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.subring[of A B Y],
       frule PolynRg.is_Ring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption,
       frule mem_subring_mem_ring[of S s], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; s \<in> carrier S; Subring R S; Ring S; Subring A B; Ring A; Ring B; s \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X A B Y h s = h s
[PROOF STEP]
apply (case_tac "s = \<zero>\<^bsub>S\<^esub>", simp add:Subring_zero_ring_zero,
       simp add:erH_rHom_0,
       simp add:Subring_zero_ring_zero[THEN sym],
       simp add:rHom_0_0, simp add:Ring.Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; s \<in> carrier S; Subring R S; Ring S; Subring A B; Ring A; Ring B; s \<in> carrier R; s \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> erH R S X A B Y h s = h s
[PROOF STEP]
apply (frule s_cf_expr[of s],simp add:Subring_zero_ring_zero,
       (erule conjE)+,
       simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; s \<in> carrier S; Subring R S; Ring S; Subring A B; Ring A; Ring B; s \<in> carrier R; s \<noteq> \<zero>; pol_coeff S (s_cf R S X s); s = polyn_expr R X (fst (s_cf R S X s)) (s_cf R S X s); snd (s_cf R S X s) (fst (s_cf R S X s)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h s = h s
[PROOF STEP]
apply (frule s_cf_deg[of s], assumption+,
       frule pol_of_deg0[of s], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; s \<in> carrier S; Subring R S; Ring S; Subring A B; Ring A; Ring B; s \<in> carrier R; s \<noteq> \<zero>; pol_coeff S (s_cf R S X s); s = polyn_expr R X 0 (s_cf R S X s); snd (s_cf R S X s) 0 \<noteq> \<zero>; deg_n R S X s = 0; fst (s_cf R S X s) = 0\<rbrakk> \<Longrightarrow> erH R S X A B Y h s = h s
[PROOF STEP]
apply (subst erH_def, simp,
       subst erh_rHom_coeff[of A B Y h "s_cf R S X s"], assumption+,
       simp add:cmp_def polyn_expr_def,
       frule_tac c = "s_cf R S X s" and j = 0 in pol_coeff_mem, simp,
       frule mem_subring_mem_ring[of S "snd (s_cf R S X s) 0"], assumption+,
       simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_coeff:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B;
       pol_coeff S (n, f)\<rbrakk>  \<Longrightarrow> pol_coeff B (n, cmp h f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> pol_coeff B (n, cmp h f)
[PROOF STEP]
apply (simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; \<forall>j\<le>n. f j \<in> carrier S\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp h f j \<in> carrier B
[PROOF STEP]
apply (rule allI, rule impI, drule_tac a = j in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; j \<le> n; f j \<in> carrier S\<rbrakk> \<Longrightarrow> cmp h f j \<in> carrier B
[PROOF STEP]
apply (simp add:cmp_def rHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_unique:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B\<rbrakk>
     \<Longrightarrow>  \<exists>!g. g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow> \<exists>!g. g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac is_Ring,
       frule PolynRg.subring[of A B Y],
       frule PolynRg.is_Ring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption,
       frule Idomain.idom_is_ring[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S\<rbrakk> \<Longrightarrow> \<exists>!g. g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x)
[PROOF STEP]
apply (rule ex_ex1I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S\<rbrakk> \<Longrightarrow> \<exists>g. g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x)
 2. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x); y \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = y x)\<rbrakk> \<Longrightarrow> g = y
[PROOF STEP]
apply (frule erH_rHom[of A B Y h], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> \<exists>g. g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x)
 2. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x); y \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = y x)\<rbrakk> \<Longrightarrow> g = y
[PROOF STEP]
apply (subgoal_tac "\<forall>x\<in>carrier S. h x = (erH R S X A B Y h) x", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. h x = erH R S X A B Y h x
 2. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x); y \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = y x)\<rbrakk> \<Longrightarrow> g = y
[PROOF STEP]
apply (rule ballI, simp add:erH_rHom_cf, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x\<rbrakk> \<Longrightarrow> g = y
[PROOF STEP]
apply (frule pHom_rHom[of A B Y], assumption+,
        frule pHom_rHom[of A B Y], assumption+,
        frule_tac f = g in rHom_func[of _ R A],
        frule_tac f = y in rHom_func[of _ R A])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x; g \<in> rHom R A; y \<in> rHom R A; g \<in> carrier R \<rightarrow> carrier A; y \<in> carrier R \<rightarrow> carrier A\<rbrakk> \<Longrightarrow> g = y
[PROOF STEP]
apply (rule_tac f = g and g = y in funcset_eq[of _ "carrier R"],
        simp add:rHom_def aHom_def, simp add:rHom_def aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x; g \<in> rHom R A; y \<in> rHom R A; g \<in> carrier R \<rightarrow> carrier A; y \<in> carrier R \<rightarrow> carrier A\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. g x = y x
[PROOF STEP]
apply (rule ballI,
        thin_tac "g \<in> carrier R \<rightarrow> carrier A",
        thin_tac "y \<in> carrier R \<rightarrow> carrier A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R\<rbrakk> \<Longrightarrow> g x = y x
[PROOF STEP]
apply (case_tac "x = \<zero>\<^bsub>R\<^esub>", simp,
        subst rHom_0_0[of R A], assumption+, rule sym,
        subst rHom_0_0[of R A], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> g x = y x
[PROOF STEP]
apply (subst pHom_pol_mem[of A B Y], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = y x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> polyn_expr A Y (deg_n R S X x) (cf_h g (s_cf R S X x)) = y x
[PROOF STEP]
apply (frule_tac f = y and p = x in pHom_pol_mem[of A B Y], assumption+,
        simp,
        frule_tac f = g and c = "s_cf R S X x" in polyn_Hom_coeff_to_coeff,
        assumption+, simp add:s_cf_pol_coeff,
        frule_tac f = y and c = "s_cf R S X x" in polyn_Hom_coeff_to_coeff,
        assumption+, simp add:s_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (deg_n R S X x) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (deg_n R S X x) (cf_h g (s_cf R S X x)) = polyn_expr A Y (deg_n R S X x) (cf_h y (s_cf R S X x))
[PROOF STEP]
apply (simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x)) (cf_h g (s_cf R S X x)) = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x))
[PROOF STEP]
apply (frule_tac f = g and c = "s_cf R S X x" in cf_h_len1[of A B Y h],
         assumption+, rule ballI, rule sym, simp, rule s_cf_pol_coeff,
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x)); fst (cf_h g (s_cf R S X x)) = fst (cf_h h (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x)) (cf_h g (s_cf R S X x)) = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x))
[PROOF STEP]
apply (frule_tac f = y and c = "s_cf R S X x" in cf_h_len1[of A B Y h],
         assumption+, rule ballI, rule sym, simp, rule s_cf_pol_coeff,
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x)); fst (cf_h g (s_cf R S X x)) = fst (cf_h h (s_cf R S X x)); fst (cf_h y (s_cf R S X x)) = fst (cf_h h (s_cf R S X x))\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x)) (cf_h g (s_cf R S X x)) = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x))
[PROOF STEP]
apply (frule_tac c = "cf_h g (s_cf R S X x)" and d = "cf_h y (s_cf R S X x)"
         in PolynRg.pol_expr_unique2[of A B Y], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x)); fst (cf_h g (s_cf R S X x)) = fst (cf_h h (s_cf R S X x)); fst (cf_h y (s_cf R S X x)) = fst (cf_h h (s_cf R S X x)); (polyn_expr A Y (fst (cf_h g (s_cf R S X x))) (cf_h g (s_cf R S X x)) = polyn_expr A Y (fst (cf_h y (s_cf R S X x))) (cf_h y (s_cf R S X x))) = (\<forall>j\<le>fst (cf_h g (s_cf R S X x)). snd (cf_h g (s_cf R S X x)) j = snd (cf_h y (s_cf R S X x)) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y (fst (s_cf R S X x)) (cf_h g (s_cf R S X x)) = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x))
[PROOF STEP]
apply (frule_tac p = x in s_cf_pol_coeff, simp add:cf_h_len,
        thin_tac "(polyn_expr A Y (fst (s_cf R S X x)) (cf_h g (s_cf R S X x))
         = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x))) =
        (\<forall>j\<le>fst (s_cf R S X x).
            snd (cf_h g (s_cf R S X x)) j = snd (cf_h y (s_cf R S X x)) j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x)); fst (cf_h g (s_cf R S X x)) = fst (s_cf R S X x); fst (cf_h y (s_cf R S X x)) = fst (s_cf R S X x); pol_coeff S (s_cf R S X x)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X x). snd (cf_h g (s_cf R S X x)) j = snd (cf_h y (s_cf R S X x)) j
[PROOF STEP]
apply (rule allI, rule impI,
        (subst cf_h_def)+, (subst cmp_def)+, simp,
        frule_tac c = "s_cf R S X x" and j = j in pol_coeff_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g y x j. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring R; Subring A B; Ring A; Ring B; Ring S; g \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. y x = g x; y \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. h x = g x; g \<in> rHom R A; y \<in> rHom R A; x \<in> carrier R; x \<noteq> \<zero>; y x = polyn_expr A Y (fst (s_cf R S X x)) (cf_h y (s_cf R S X x)); pol_coeff B (cf_h g (s_cf R S X x)); pol_coeff B (cf_h y (s_cf R S X x)); fst (cf_h g (s_cf R S X x)) = fst (s_cf R S X x); fst (cf_h y (s_cf R S X x)) = fst (s_cf R S X x); pol_coeff S (s_cf R S X x); j \<le> fst (s_cf R S X x); snd (s_cf R S X x) j \<in> carrier S\<rbrakk> \<Longrightarrow> g (snd (s_cf R S X x) j) = y (snd (s_cf R S X x) j)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_rHom_unique1:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B;
       f \<in> pHom R S X, A B Y; \<forall>x \<in> carrier S. f x = h x\<rbrakk> \<Longrightarrow>
       f = (erH R S X A B Y h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; f \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. f x = h x\<rbrakk> \<Longrightarrow> f = erH R S X A B Y h
[PROOF STEP]
apply (frule erH_rHom_unique[of A B Y h], assumption+,
       erule ex1E,
       frule_tac x = f in spec,
       drule_tac x = "erH R S X A B Y h" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; f \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. f x = h x; g \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = g x); f \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = f x) \<longrightarrow> f = g; erH R S X A B Y h \<in> pHom R S X, A B Y \<and> (\<forall>x\<in>carrier S. h x = erH R S X A B Y h x) \<longrightarrow> erH R S X A B Y h = g\<rbrakk> \<Longrightarrow> f = erH R S X A B Y h
[PROOF STEP]
apply (frule erH_rHom[of A B Y h], assumption+,
        simp add:erH_rHom_cf[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_dec_deg:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
       p \<in> carrier R\<rbrakk> \<Longrightarrow>
                  deg A B Y (f p) \<le> deg R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R\<rbrakk> \<Longrightarrow> deg A B Y (f p) \<le> deg R S X p
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.subring[of A B Y],
       cut_tac is_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R\<rbrakk> \<Longrightarrow> deg A B Y (f p) \<le> deg R S X p
[PROOF STEP]
apply (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>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B\<rbrakk> \<Longrightarrow> deg A B Y (f p) \<le> deg R S X p
[PROOF STEP]
apply (case_tac "f p = \<zero>\<^bsub>A\<^esub>",
       case_tac "p = \<zero>\<^bsub>R\<^esub>",
       simp add:deg_def, simp add:deg_def an_def,
       simp add:deg_def, subst ale_natle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> an (deg_n A B Y (f \<zero>)) \<le> - \<infinity>) \<and> (p \<noteq> \<zero> \<longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p)
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>",
       frule pHom_rHom[of A B Y f], assumption+,
       rule conjI, rule impI, frule rHom_0_0[of R A f], assumption+,
       simp, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> an (deg_n A B Y (f \<zero>)) \<le> - \<infinity>) \<and> (p \<noteq> \<zero> \<longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p
[PROOF STEP]
apply (frule pHom_pol_mem[of A B Y f p], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p
[PROOF STEP]
apply (cut_tac polyn_Hom_coeff_to_coeff[of A B Y f "s_cf R S X p"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p)); pol_coeff B (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p
 2. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> PolynRg A B Y
 3. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> f \<in> pHom R S X, A B Y
 4. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply (frule PolynRg.pol_deg_le_n[of A B Y "f p" "cf_h f (s_cf R S X p)"],
        frule pHom_rHom[of A B Y f], assumption+,
        rule rHom_mem[of f R A p], assumption+,
        frule s_cf_pol_coeff[of p],
        subst cf_h_len2[of A B Y f "s_cf R S X p"], assumption+,
        simp add:s_cf_deg,
       thin_tac "f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; pol_coeff B (cf_h f (s_cf R S X p)); deg_n A B Y (f p) \<le> fst (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> deg_n A B Y (f p) \<le> deg_n R S X p
 2. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> PolynRg A B Y
 3. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> f \<in> pHom R S X, A B Y
 4. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; f p \<noteq> \<zero>\<^bsub>A\<^esub>; p \<noteq> \<zero>; f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply (frule s_cf_pol_coeff[of p], simp add:cf_h_len2,
              simp add:s_cf_deg[THEN sym],
              assumption+,
              simp add:s_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erH_map:"\<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B;
       pol_coeff S (n, c)\<rbrakk> \<Longrightarrow>
      (erH R S X A B Y h) (polyn_expr R X n (n, c)) =
                           polyn_expr A Y n (n, (cmp h c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.subring[of A B Y],
       cut_tac is_Ring,
       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 S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (case_tac "polyn_expr R X n (n, c) = \<zero>\<^bsub>R\<^esub>", simp add:erH_rHom_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) = \<zero>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> = polyn_expr A Y n (n, cmp h c)
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (frule coeff_0_pol_0[THEN sym, of "(n, c)" n], simp, simp,
        thin_tac "polyn_expr R X n (n, c) = \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; \<forall>j\<le>n. c j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> = polyn_expr A Y n (n, cmp h c)
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (frule cf_h_coeff[of A B Y h "(n, c)"], assumption+,
        simp add:cf_h_pol_coeff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; \<forall>j\<le>n. c j = \<zero>\<^bsub>S\<^esub>; pol_coeff B (n, cmp h c)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> = polyn_expr A Y n (n, cmp h c)
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (rule sym,
        frule_tac PolynRg.coeff_0_pol_0[THEN sym, of A B Y "(n, cmp h c)" n],
        simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; \<forall>j\<le>n. c j = \<zero>\<^bsub>S\<^esub>; pol_coeff B (n, cmp h c); (polyn_expr A Y n (n, cmp h c) = \<zero>\<^bsub>A\<^esub>) = (\<forall>j\<le>n. cmp h c j = \<zero>\<^bsub>B\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp h c j = \<zero>\<^bsub>B\<^esub>
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (rule allI, rule impI, simp add:cmp_def, simp add:rHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> erH R S X A B Y h (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[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; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; 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 (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (subst pHom_mem[of A B Y "erH R S X A B Y h" n c], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp (erH R S X A B Y h) c) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique2[of A B Y
        "(n, cmp (erH R S X A B Y h) c)" "(n, cmp h c)"],
       simp add:cmp_pol_coeff_e, simp add:cmp_pol_coeff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> fst (n, cmp (erH R S X A B Y h) c) = fst (n, cmp h c)
 2. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; erH R S X A B Y h \<in> pHom R S X, A B Y; (polyn_expr A Y (fst (n, cmp (erH R S X A B Y h) c)) (n, cmp (erH R S X A B Y h) c) = polyn_expr A Y (fst (n, cmp h c)) (n, cmp h c)) = (\<forall>j\<le>fst (n, cmp (erH R S X A B Y h) c). snd (n, cmp (erH R S X A B Y h) c) j = snd (n, cmp h c) j)\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp (erH R S X A B Y h) c) = polyn_expr A Y n (n, cmp h c)
[PROOF STEP]
apply (simp, simp,
        thin_tac "(polyn_expr A Y n (n, cmp (erH R S X A B Y h) c) =
        polyn_expr A Y n (n, cmp h c)) =
       (\<forall>j\<le>n. cmp (erH R S X A B Y h) c j = cmp h c j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; erH R S X A B Y h \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (erH R S X A B Y h) c j = cmp h c j
[PROOF STEP]
apply (rule allI, rule impI,
        frule_tac j = j in pol_coeff_mem[of "(n, c)"], simp,
        simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>Idomain S; PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, c); Subring R S; Ring S; Subring A B; Ring R; Ring A; Ring B; polyn_expr R X n (n, c) \<noteq> \<zero>; erH R S X A B Y h \<in> pHom R S X, A B Y; j \<le> n; c j \<in> carrier S\<rbrakk> \<Longrightarrow> erH R S X A B Y h (c j) = h (c j)
[PROOF STEP]
apply (simp add:erH_rHom_cf)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) divisionTr0:"\<lbrakk>Idomain S; p \<in> carrier R;
       c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow>
                     lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> (lcf R S X p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X p
[PROOF STEP]
apply (cut_tac polyn_ring_integral, simp,
       cut_tac subring, frule subring_Ring,
       cut_tac polyn_ring_X_nonzero,
       cut_tac X_mem_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X p
[PROOF STEP]
apply (frule mem_subring_mem_ring[of S c], assumption+,
      frule npClose[of X n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X p
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp,
       frule ring_tOp_closed[of c "X^\<^bsup>R n\<^esup>"], assumption+,
       simp add:ring_times_x_0 lcf_val_0,
       simp add:Ring.ring_times_x_0[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X p
[PROOF STEP]
apply (frule_tac x = c and y = " X^\<^bsup>R n\<^esup>" in Idomain.idom_tOp_nonzeros[of R],
      assumption+,
      simp add:Subring_zero_ring_zero,
      frule Idomain.idom_potent_nonzero[of R X n], assumption+,
      frule_tac x = c and y = " X^\<^bsup>R n\<^esup>" in ring_tOp_closed, assumption+,
      frule_tac x = "c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup>" and y = p in Idomain.idom_tOp_nonzeros[of R],
      assumption+,
      frule_tac x = "c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup>" and y = p in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R\<rbrakk> \<Longrightarrow> lcf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X p
[PROOF STEP]
apply (simp add:lcf_val)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (fst (s_cf R S X (c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+,
       simp add:ring_tOp_assoc[of c _ p],
       frule low_deg_terms_zero1[THEN sym, of "s_cf R S X p" n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; 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>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (cut_tac a = "X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r
                    polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)" and
               b = "X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p" and
               c = "polyn_expr R X (fst (s_cf R S X p) + n)
                     (ext_cf S n (s_cf R S X p))" in box_equation,
       simp, assumption,
   thin_tac "p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)",
   thin_tac "X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) =
     polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p = polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (frule ext_cf_pol_coeff[of "s_cf R S X p" n],
       frule scalar_times_pol_expr[of c "ext_cf S n (s_cf R S X p)"
            "fst (s_cf R S X p) + n"], assumption+,
       simp add:ext_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p = polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p)); pol_coeff S (ext_cf S n (s_cf R S X p)); c \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p)) = polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p)))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (frule sp_cf_pol_coeff[of "ext_cf S n (s_cf R S X p)" c],
          assumption+,
     cut_tac a = "c \<cdot>\<^sub>r
     polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p))"
     and b = "c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)" and
         c = "polyn_expr R X (fst (s_cf R S X p) + n)
              (sp_cf S c (ext_cf S n (s_cf R S X p)))" in box_equation,
     simp, simp,
     thin_tac "X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p =
        polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p))",
     thin_tac "c \<cdot>\<^sub>r
        polyn_expr R X (fst (s_cf R S X p) + n) (ext_cf S n (s_cf R S X p)) =
        polyn_expr R X (fst (s_cf R S X p) + n)
        (sp_cf S c (ext_cf S n (s_cf R S X p)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p)))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (frule s_cf_expr[of "c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)"], assumption+,
         (erule conjE)+,
         drule_tac a = "c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)" and
         b = "polyn_expr R X (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))))
                       (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))" and
         c = "polyn_expr R X (fst (s_cf R S X p) + n)
             (sp_cf S c (ext_cf S n (s_cf R S X p)))" in box_equation,
       assumption,
       thin_tac "c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) =
          polyn_expr R X (fst (s_cf R S X p) + n)
          (sp_cf S c (ext_cf S n (s_cf R S X p)))",
       frule pol_expr_unique2[of "s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))"
               "sp_cf S c (ext_cf S n (s_cf R S X p))"], assumption+,
       subst s_cf_deg[THEN sym], assumption+,
        frule_tac Idomain.idom_potent_nonzero[of R X n], assumption+,
        frule_tac x = "X^\<^bsup>R n\<^esup>" and y = p in Idomain.idom_tOp_nonzeros[of R],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) = fst (sp_cf S c (ext_cf S n (s_cf R S X p)))
 2. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (fst (sp_cf S c (ext_cf S n (s_cf R S X p)))) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j)\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (subst deg_mult_pols, assumption+, simp add:Subring_zero_ring_zero,
        simp add:ring_tOp_closed, assumption+,
        subst deg_mult_pols, assumption+,
        simp add:deg_to_X_d,
        cut_tac pol_of_deg0[THEN sym, of c], simp,
        simp add:sp_cf_len ext_cf_len s_cf_deg, assumption+,
        simp add:Subring_zero_ring_zero,
        simp add:sp_cf_len ext_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (fst (s_cf R S X p) + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + fst (s_cf R S X p)) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j)\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (fst (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
apply (subst s_cf_deg[THEN sym], assumption+,
        frule_tac Idomain.idom_potent_nonzero[of R X n], assumption+,
        frule_tac x = "X^\<^bsup>R n\<^esup>" and y = p in Idomain.idom_tOp_nonzeros[of R],
        assumption+,
        simp add:s_cf_deg[THEN sym],
        frule_tac x = "X^\<^bsup>R n\<^esup>" and y = p in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R\<rbrakk> \<Longrightarrow> snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (deg_n R S X p)
[PROOF STEP]
apply (frule deg_mult_pols[of c "X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p"], assumption+,
        simp add:Subring_zero_ring_zero, assumption+, (erule conjE)+, simp,
        thin_tac "deg_n R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) =
                          deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)",
        cut_tac pol_of_deg0[THEN sym, of c], simp,
        frule deg_mult_pols[of "X^\<^bsup>R n\<^esup>" p], assumption+, (erule conjE)+,
             simp,
      thin_tac "deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) = deg_n R S X (X^\<^bsup>R n\<^esup>) + deg_n R S X p",
      simp add:deg_to_X_d, simp add:add.commute[of n],
      thin_tac "polyn_expr R X (deg_n R S X p + n)
          (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n)
                                      (sp_cf S c (ext_cf S n (s_cf R S X p)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain R; p \<in> carrier R; deg_n R S X c = 0; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (sp_cf S c (ext_cf S n (s_cf R S X p))) (deg_n R S X p + n) \<noteq> \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>deg_n R S X p + n. snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<in> carrier S; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> snd (sp_cf S c (ext_cf S n (s_cf R S X p))) (deg_n R S X p + n) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (deg_n R S X p)
 2. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<in> carrier R
 3. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<noteq> \<zero>
[PROOF STEP]
apply (subst sp_cf_def, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain R; p \<in> carrier R; deg_n R S X c = 0; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (sp_cf S c (ext_cf S n (s_cf R S X p))) (deg_n R S X p + n) \<noteq> \<zero>\<^bsub>S\<^esub>; \<forall>j\<le>deg_n R S X p + n. snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>; c \<in> carrier S; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (ext_cf S n (s_cf R S X p)) (deg_n R S X p + n) = c \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X p) (deg_n R S X p)
 2. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<in> carrier R
 3. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<noteq> \<zero>
[PROOF STEP]
apply (subst ext_cf_def, simp add:sliden_def, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Idomain S; Subring R S; Ring S; X \<noteq> \<zero>; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R n\<^esup> \<in> carrier R; p \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<noteq> \<zero>; c \<cdot>\<^sub>r X^\<^bsup>R n\<^esup> \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<in> carrier R; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (deg_n R S X p) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S n (s_cf R S X p)); pol_coeff S (sp_cf S c (ext_cf S n (s_cf R S X p))); pol_coeff S (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))); snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p)) (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) = polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))); (polyn_expr R X (deg_n R S X p + n) (sp_cf S c (ext_cf S n (s_cf R S X p))) = polyn_expr R X (n + deg_n R S X p) (sp_cf S c (ext_cf S n (s_cf R S X p)))) = (\<forall>j\<le>deg_n R S X c + deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p). snd (s_cf R S X (c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p))) j = snd (sp_cf S c (ext_cf S n (s_cf R S X p))) j); X^\<^bsup>R n\<^esup> \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p \<in> carrier R; c \<cdot>\<^sub>r (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r p) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<noteq> \<zero>
[PROOF STEP]
apply (simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done