[STATEMENT]
lemma (in PolynRg) Pmod_0_principal:"\<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R;
            P_mod R S X (S \<diamondsuit>\<^sub>p t) g\<rbrakk> \<Longrightarrow> \<exists>h\<in> carrier R. g = t \<cdot>\<^sub>r h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) g\<rbrakk> \<Longrightarrow> \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) g; Subring R S; Ring S\<rbrakk> \<Longrightarrow> \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h
[PROOF STEP]
apply (case_tac "g = \<zero>\<^bsub>R\<^esub>",
       cut_tac ring_zero,
       frule mem_subring_mem_ring[of S t], assumption+,
       frule ring_times_x_0[THEN sym, of t], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) g; Subring R S; Ring S; g \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h
[PROOF STEP]
apply (frule s_cf_expr[of g], assumption+,
        (erule conjE)+, frule Ring.principal_ideal[of S t], assumption,
       simp add:P_mod_mod[THEN sym, of "S \<diamondsuit>\<^sub>p t" g],
       frule coeff_principal[of t "fst (s_cf R S X g)" "snd (s_cf R S X g)"],
         simp add:pol_coeff_split[THEN sym], assumption+,
       erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f'. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t; Subring R S; Ring S; g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); pol_coeff S (fst (s_cf R S X g), f'); \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j\<rbrakk> \<Longrightarrow> \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h
[PROOF STEP]
apply (frule_tac c = "(fst (s_cf R S X g), f')" and k = "fst (s_cf R S X g)"
        in polyn_mem, simp,
        subgoal_tac "g = t \<cdot>\<^sub>r
        (polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), f'))",
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f'. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t; Subring R S; Ring S; g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); pol_coeff S (fst (s_cf R S X g), f'); \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), f') \<in> carrier R\<rbrakk> \<Longrightarrow> g = t \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), f')
[PROOF STEP]
apply (subst scalar_times_pol_expr[of  t "(fst (s_cf R S X g), f')"
           "fst (s_cf R S X g)"], assumption+, simp,
        drule sym,
        subgoal_tac "polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) =
     polyn_expr R X (fst (s_cf R S X g)) (sp_cf S t (fst (s_cf R S X g), f'))",
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f'. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j \<in> S \<diamondsuit>\<^sub>p t; Subring R S; Ring S; g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); snd (s_cf R S X g) (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); pol_coeff S (fst (s_cf R S X g), f'); \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), f') \<in> carrier R; polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = g\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = polyn_expr R X (fst (s_cf R S X g)) (sp_cf S t (fst (s_cf R S X g), f'))
[PROOF STEP]
apply (frule_tac c = "(fst (s_cf R S X g), f')" in sp_cf_pol_coeff[of _ t],
        assumption+,
        frule_tac d = "sp_cf S t (fst (s_cf R S X g), f')" in
         pol_expr_unique2[of "s_cf R S X g"], assumption+,
        simp, simp add:sp_cf_len, simp add:sp_cf_len,
       thin_tac "(g =
           polyn_expr R X (fst (s_cf R S X g))
            (sp_cf S t (fst (s_cf R S X g), f'))) =
          (\<forall>j\<le>fst (s_cf R S X g).
              t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = snd (sp_cf S t (fst (s_cf R S X g), f')) j)",
       thin_tac "polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g) = g",
       thin_tac "polyn_expr R X (fst (s_cf R S X g)) (fst (s_cf R S X g), f')
          \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f'. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<forall>j\<le>fst (s_cf R S X g). t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j \<in> S \<diamondsuit>\<^sub>p t; Subring R S; Ring S; g \<noteq> \<zero>; pol_coeff S (s_cf R S X g); t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' (fst (s_cf R S X g)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); pol_coeff S (fst (s_cf R S X g), f'); \<forall>j\<le>fst (s_cf R S X g). snd (s_cf R S X g) j = t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j; pol_coeff S (sp_cf S t (fst (s_cf R S X g), f'))\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X g). t \<cdot>\<^sub>r\<^bsub>S\<^esub> f' j = snd (sp_cf S t (fst (s_cf R S X g), f')) j
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, assumption+,
        simp add:sp_cf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) Pmod0_principal_rev:"\<lbrakk>Idomain S; t \<in> carrier S;
                     g \<in> carrier R; \<exists>h\<in> carrier R. g = t \<cdot>\<^sub>r  h\<rbrakk> \<Longrightarrow>
                                       P_mod R S X (S \<diamondsuit>\<^sub>p t) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; \<exists>h\<in>carrier R. g = t \<cdot>\<^sub>r h; Subring R S; Ring S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; g = t \<cdot>\<^sub>r h\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (case_tac "t = \<zero>\<^bsub>S\<^esub>",
       frule Subring_zero_ring_zero, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>Idomain S; \<zero> \<in> carrier S; \<zero> \<cdot>\<^sub>r h \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; g = \<zero> \<cdot>\<^sub>r h; t = \<zero>; \<zero>\<^bsub>S\<^esub> = \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p \<zero>) (\<zero> \<cdot>\<^sub>r h)
 2. \<And>h. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; g = t \<cdot>\<^sub>r h; t \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (simp add:ring_times_0_x, simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain S; t \<in> carrier S; g \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; g = t \<cdot>\<^sub>r h; t \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) g
[PROOF STEP]
apply (case_tac "h = \<zero>\<^bsub>R\<^esub>", simp,
       frule mem_subring_mem_ring[of S t], assumption+,
       simp add:ring_times_x_0, simp add:P_mod_def,
       cut_tac polyn_ring_integral, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain R; t \<in> carrier S; t \<cdot>\<^sub>r h \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; g = t \<cdot>\<^sub>r h; t \<noteq> \<zero>\<^bsub>S\<^esub>; h \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r h)
[PROOF STEP]
apply (frule_tac p = h in s_cf_expr, assumption+, (erule conjE)+,
       frule_tac c = "s_cf R S X h" and n = "fst (s_cf R S X h)" in
       scalar_times_pol_expr[of  t], assumption+, simp,
       thin_tac "g = t \<cdot>\<^sub>r h",
       drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain R; t \<in> carrier S; polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)) \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; t \<noteq> \<zero>\<^bsub>S\<^esub>; h \<noteq> \<zero>; Idomain S; pol_coeff S (s_cf R S X h); snd (s_cf R S X h) (fst (s_cf R S X h)) \<noteq> \<zero>\<^bsub>S\<^esub>; t \<cdot>\<^sub>r h = polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)); polyn_expr R X (fst (s_cf R S X h)) (s_cf R S X h) = h\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)))
[PROOF STEP]
apply (frule Ring.principal_ideal[of S t], assumption+,
       frule_tac c1 = "sp_cf S t (s_cf R S X h)" and p1 = "t \<cdot>\<^sub>r h" in
       P_mod_mod[THEN sym],
       frule_tac x = t in mem_subring_mem_ring, assumption,
                 rule ring_tOp_closed, assumption+,
       simp add:sp_cf_pol_coeff, simp add:sp_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain R; t \<in> carrier S; polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)) \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; t \<noteq> \<zero>\<^bsub>S\<^esub>; h \<noteq> \<zero>; Idomain S; pol_coeff S (s_cf R S X h); snd (s_cf R S X h) (fst (s_cf R S X h)) \<noteq> \<zero>\<^bsub>S\<^esub>; t \<cdot>\<^sub>r h = polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)); polyn_expr R X (fst (s_cf R S X h)) (s_cf R S X h) = h; ideal S (S \<diamondsuit>\<^sub>p t); P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r h) = (\<forall>j\<le>fst (sp_cf S t (s_cf R S X h)). snd (sp_cf S t (s_cf R S X h)) j \<in> S \<diamondsuit>\<^sub>p t)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (polyn_expr R X (fst (s_cf R S X h)) (sp_cf S t (s_cf R S X h)))
[PROOF STEP]
apply (drule sym, simp,
       thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r h) =
         (\<forall>j\<le>fst (sp_cf S t (s_cf R S X h)).
             snd (sp_cf S t (s_cf R S X h)) j \<in> S \<diamondsuit>\<^sub>p t)",
       thin_tac "polyn_expr R X (fst (s_cf R S X h))
                     (sp_cf S t (s_cf R S X h)) = t \<cdot>\<^sub>r h",
       thin_tac "polyn_expr R X (fst (s_cf R S X h)) (s_cf R S X h) = h")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>Idomain R; t \<in> carrier S; t \<cdot>\<^sub>r h \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; t \<noteq> \<zero>\<^bsub>S\<^esub>; h \<noteq> \<zero>; Idomain S; pol_coeff S (s_cf R S X h); snd (s_cf R S X h) (fst (s_cf R S X h)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (sp_cf S t (s_cf R S X h)). snd (sp_cf S t (s_cf R S X h)) j \<in> S \<diamondsuit>\<^sub>p t
[PROOF STEP]
apply (rule allI, rule impI, simp add:sp_cf_len,
       subst sp_cf_def, simp, subst Rxa_def, simp,
       frule_tac c = "s_cf R S X h" and j = j in pol_coeff_mem,
       assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h j. \<lbrakk>Idomain R; t \<in> carrier S; t \<cdot>\<^sub>r h \<in> carrier R; Subring R S; Ring S; h \<in> carrier R; t \<noteq> \<zero>\<^bsub>S\<^esub>; h \<noteq> \<zero>; Idomain S; pol_coeff S (s_cf R S X h); snd (s_cf R S X h) (fst (s_cf R S X h)) \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); j \<le> fst (s_cf R S X h); snd (s_cf R S X h) j \<in> carrier S\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier S. t \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X h) j = r \<cdot>\<^sub>r\<^bsub>S\<^esub> t
[PROOF STEP]
apply (simp add:Ring.ring_tOp_commute[of S t], blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) Pmod0_principal_rev1:"\<lbrakk>Idomain S; t \<in> carrier S;
                     h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r h)
[PROOF STEP]
apply (rule Pmod0_principal_rev[of t "t \<cdot>\<^sub>r h"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; h \<in> carrier R\<rbrakk> \<Longrightarrow> t \<cdot>\<^sub>r h \<in> carrier R
 2. \<lbrakk>Idomain S; t \<in> carrier S; h \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>ha\<in>carrier R. t \<cdot>\<^sub>r h = t \<cdot>\<^sub>r ha
[PROOF STEP]
apply (cut_tac subring,
       frule mem_subring_mem_ring[of S t], assumption+,
       simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; h \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>ha\<in>carrier R. t \<cdot>\<^sub>r h = t \<cdot>\<^sub>r ha
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) Pmod0_principal_erH_vanish_t:"\<lbrakk>Idomain S; ideal S (S \<diamondsuit>\<^sub>p t);
 t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y \<rbrakk> \<Longrightarrow>
      erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) t = \<zero>\<^bsub>R'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S (S \<diamondsuit>\<^sub>p t); t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) t = \<zero>\<^bsub>R'\<^esub>
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule mem_subring_mem_ring[of S t], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S (S \<diamondsuit>\<^sub>p t); t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; Subring R S; Ring S; t \<in> carrier R\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) t = \<zero>\<^bsub>R'\<^esub>
[PROOF STEP]
apply (subst P_mod_0[of "S \<diamondsuit>\<^sub>p t" R' Y t], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S (S \<diamondsuit>\<^sub>p t); t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; Subring R S; Ring S; t \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) t
[PROOF STEP]
apply (rule Pmod0_principal_rev[of t t], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; ideal S (S \<diamondsuit>\<^sub>p t); t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; Subring R S; Ring S; t \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>carrier R. t = t \<cdot>\<^sub>r h
[PROOF STEP]
apply (cut_tac ring_one,
        frule ring_r_one[THEN sym, of t], blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done