[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx1:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
        maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y;
        f \<in> carrier R; g \<in> carrier R; h \<in> carrier R;
        f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R;
        erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>;
        erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>;
        ra \<in> carrier R;
        f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m;
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) u)
         \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<plusminus>\<^bsub>R'\<^esub>
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) v)
         \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h =
        erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra\<rbrakk>
       \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>))
           (f \<plusminus> -\<^sub>a ((g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) u \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) v \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (cut_tac is_Ring,
       cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag,
       frule PolynRg.is_Ring[of R' "S /\<^sub>r (S \<diamondsuit>\<^sub>p t)" Y],
       frule Ring.ring_is_ag[of R'],
       frule Ring.maximal_ideal_ideal[of "S" "S \<diamondsuit>\<^sub>p t"], assumption+,
       frule Ring.qring_ring[of S "S \<diamondsuit>\<^sub>p t"], assumption+,
       frule erH_rHom[of R' "S /\<^sub>r (S \<diamondsuit>\<^sub>p t)" Y "pj S (S \<diamondsuit>\<^sub>p t)"], assumption+,
       frule mem_subring_mem_ring[of S t], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) u \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) v \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); t \<in> carrier R\<rbrakk> \<Longrightarrow> pj S (S \<diamondsuit>\<^sub>p t) \<in> rHom S (S /\<^sub>r (S \<diamondsuit>\<^sub>p t))
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) u \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) v \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (rule pj_Hom[of S "S \<diamondsuit>\<^sub>p t"], assumption+,
       frule pHom_rHom[of R' "S /\<^sub>r (S \<diamondsuit>\<^sub>p t)" Y
        "erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) u \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) v \<cdot>\<^sub>r\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (simp del:npow_suc add:rHom_tOp[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g) \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (v \<cdot>\<^sub>r h) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (frule_tac ring_tOp_closed[of u g], assumption,
       frule_tac ring_tOp_closed[of v h], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g) \<plusminus>\<^bsub>R'\<^esub> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (v \<cdot>\<^sub>r h) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (simp del:npow_suc add:rHom_add[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; 0 < m; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (rotate_tac 17, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (frule P_mod_diff[of "S \<diamondsuit>\<^sub>p t" R' Y ra  "u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h \<in> carrier R
 2. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)) = P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (frule Pmod_0_principal[of t "ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) \<in> carrier R
 2. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h))
 3. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); \<exists>ha\<in>carrier R. ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
        rule aGroup.ag_mOp_closed, assumption,
        rule aGroup.ag_pOp_closed, assumption+, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))
[PROOF STEP]
apply (frule Ring.npClose[of S t m], assumption+,
       frule mem_subring_mem_ring[of S "t^\<^bsup>S m\<^esup>"], assumption+,
       subst ring_distrib1,
       rule aGroup.ag_pOp_closed, assumption+,
       rule ring_tOp_closed, simp add:mem_subring_mem_ring,
       assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a ((g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r h \<plusminus> (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a ((g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r h \<plusminus> (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))
[PROOF STEP]
apply (subst ring_distrib2, assumption+,
       rule ring_tOp_closed, assumption+ )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))
[PROOF STEP]
apply (frule_tac x = g and y = h in ring_tOp_closed, assumption+,
       frule_tac x = "t^\<^bsup>S m\<^esup>" and y = v in ring_tOp_closed, assumption+,
       frule_tac x = "t^\<^bsup>S m\<^esup>" and y = u in ring_tOp_closed, assumption+,
       frule_tac x = "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v" and y = h in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> (g \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))
[PROOF STEP]
apply (subst ring_distrib2, assumption+,
      frule_tac x = "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v" and y = "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u" in ring_tOp_closed,
      assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))))
[PROOF STEP]
apply (subst aGroup.ag_p_inv, assumption+,
       rule aGroup.ag_pOp_closed, assumption+,
       rule aGroup.ag_pOp_closed, assumption+,
       rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> (-\<^sub>a (g \<cdot>\<^sub>r h \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h) \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))))
[PROOF STEP]
apply (subst aGroup.ag_p_inv, assumption+,
       frule aGroup.ag_mOp_closed[of R "g \<cdot>\<^sub>r h"], assumption+,
       frule aGroup.ag_mOp_closed[of R "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; -\<^sub>a g \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> (-\<^sub>a g \<cdot>\<^sub>r h \<plusminus> -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))))
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[of R "-\<^sub>a (g \<cdot>\<^sub>r h)" " -\<^sub>a (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h)"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; -\<^sub>a g \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)) \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; -\<^sub>a g \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> (-\<^sub>a g \<cdot>\<^sub>r h \<plusminus> (-\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))))
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption,
       rule aGroup.ag_pOp_closed, assumption,
       rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; -\<^sub>a g \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> (-\<^sub>a g \<cdot>\<^sub>r h \<plusminus> (-\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u)))))
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
       rule aGroup.ag_pOp_closed, assumption,
       rule aGroup.ag_mOp_closed, assumption+,
       rule aGroup.ag_mOp_closed, assumption+,
       rule aGroup.ag_pOp_closed, assumption+,
       rule ring_tOp_closed, assumption+, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; -\<^sub>a g \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra \<plusminus> (-\<^sub>a t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r h \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u))))
[PROOF STEP]
apply (subst aGroup.ag_p_inv, assumption,
       rule ring_tOp_closed, assumption+,
       simp del:npow_suc add:ring_tOp_assoc[of "t^\<^bsup>S m\<^esup>" v h],
       simp add:del:npow_suc add:ring_tOp_commute[of g "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u"],
       simp del:npow_suc add:ring_tOp_assoc[of "t^\<^bsup>S m\<^esup>" u g],
       simp del:npow_suc add:ring_inv1_2,
       subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
                            rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u)) \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<plusminus> (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
              (rule ring_tOp_closed, assumption+)+,
              rule aGroup.ag_mOp_closed, assumption+,
              (rule ring_tOp_closed, assumption+)+,
              rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<plusminus> (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (subst ring_distrib1[THEN sym, of "t^\<^bsup>S m\<^esup>" ra  "v \<cdot>\<^sub>r (-\<^sub>a h)"],
             assumption+,
             rule ring_tOp_closed, assumption+, rule aGroup.ag_mOp_closed,
             assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h)) \<plusminus> (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
             rule ring_tOp_closed, assumption+,
             rule aGroup.ag_pOp_closed, assumption+,
             rule ring_tOp_closed, assumption+, rule aGroup.ag_mOp_closed,
             assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u)) \<in> carrier R
 3. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u)))
[PROOF STEP]
apply ((rule ring_tOp_closed, assumption+)+,
              rule aGroup.ag_mOp_closed, assumption+,
             (rule ring_tOp_closed, assumption+)+,
             rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u)))
[PROOF STEP]
apply (subst ring_distrib1[THEN sym, of "t^\<^bsup>S m\<^esup>"],
               assumption+,
               rule aGroup.ag_pOp_closed, assumption+,
               rule ring_tOp_closed, assumption+,
               rule aGroup.ag_mOp_closed, assumption+,
               rule ring_tOp_closed, assumption+,
               rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u)))
[PROOF STEP]
apply (subst ring_tOp_assoc[of "t^\<^bsup>S m\<^esup>" v], assumption+,
                rule ring_tOp_closed, assumption+,
                rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g)) \<plusminus> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (subst ring_distrib1[THEN sym, of "t^\<^bsup>S m\<^esup>"],
                assumption+,
                rule aGroup.ag_pOp_closed, assumption+,
                rule aGroup.ag_pOp_closed, assumption+,
                rule ring_tOp_closed, assumption,
                rule aGroup.ag_mOp_closed, assumption+,
                rule ring_tOp_closed, assumption,
                rule aGroup.ag_mOp_closed, assumption+,
                (rule ring_tOp_closed, assumption+)+,
                rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> -\<^sub>a (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) \<plusminus> v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (frule ring_tOp_closed[of u g], assumption+,
           frule ring_tOp_closed[of v h], assumption+,
           simp del:npow_suc add:aGroup.ag_p_inv[of R "u \<cdot>\<^sub>r g" "v \<cdot>\<^sub>r h"],
           simp del:npow_suc add:add:ring_inv1_2,
           frule aGroup.ag_mOp_closed[of R g], assumption+,
                  frule aGroup.ag_mOp_closed[of R h], assumption+,
           frule ring_tOp_closed[of u "-\<^sub>a g"], assumption+,
                  frule ring_tOp_closed[of v "-\<^sub>a h"], assumption+,
           simp del:npow_suc add:aGroup.ag_pOp_commute[of R
                  "u \<cdot>\<^sub>r (-\<^sub>a g)" "v \<cdot>\<^sub>r (-\<^sub>a h)"],
           simp del:npow_suc add:aGroup.ag_pOp_assoc[THEN sym,
                  of R ra "v \<cdot>\<^sub>r (-\<^sub>a h)" "u \<cdot>\<^sub>r (-\<^sub>a g)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (t \<cdot>\<^sub>r ha \<plusminus> v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (-\<^sub>a u))))
[PROOF STEP]
apply (subst ring_tOp_assoc[THEN sym, of v "t^\<^bsup>S m\<^esup>" "-\<^sub>a u"], assumption+,
         rule aGroup.ag_mOp_closed, assumption+,
         simp only:ring_tOp_commute[of v "t^\<^bsup>S m\<^esup>"],
         subgoal_tac "t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)",
         simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (t \<cdot>\<^sub>r ha \<plusminus> t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (-\<^sub>a u)))
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (subst ring_tOp_assoc[of t],
         frule mem_subring_mem_ring[of S t], assumption+,
         rule ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> t^\<^bsup>S (m - Suc 0)\<^esup> \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> v \<in> carrier R
 3. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> -\<^sub>a u \<in> carrier R
 4. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (t \<cdot>\<^sub>r ha \<plusminus> t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u))))
 5. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (frule Ring.npClose[of S t "m - Suc 0"], assumption+,
          simp add:mem_subring_mem_ring, assumption,
          rule aGroup.ag_mOp_closed, assumption+,
          subst ring_distrib1[THEN sym, of t],
          simp add:mem_subring_mem_ring, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u) \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (t \<cdot>\<^sub>r (ha \<plusminus> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u))))
 3. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply ((rule ring_tOp_closed)+,
          frule Ring.npClose[of S t "m - Suc 0"], assumption+,
          simp add:mem_subring_mem_ring, assumption,
          rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (t \<cdot>\<^sub>r (ha \<plusminus> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u))))
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (subst ring_tOp_assoc[THEN sym],
         frule Ring.npClose[of S t "m - Suc 0"], assumption+,
         simp add:mem_subring_mem_ring)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> ha \<plusminus> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u) \<in> carrier R
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r t \<cdot>\<^sub>r (ha \<plusminus> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u)))
 3. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
         rule ring_tOp_closed,
         frule Ring.npClose[of S t "m - Suc 0"], assumption+,
         rule ring_tOp_closed, simp add:mem_subring_mem_ring,
         assumption, rule aGroup.ag_mOp_closed, assumption+,
         simp add:Subring_tOp_ring_tOp[THEN sym],
         simp only:npow_suc[THEN sym, of S t m])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v) \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (t^\<^bsup>S Suc m\<^esup> \<cdot>\<^sub>r (ha \<plusminus> t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (-\<^sub>a u)))
 2. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (rule Pmod0_principal_rev1[of "t^\<^bsup>S (Suc m)\<^esup>"], assumption+,
         rule Ring.npClose, assumption+,
         rule aGroup.ag_pOp_closed, assumption+,
         (rule ring_tOp_closed)+,
         frule Ring.npClose[of S t "m - Suc 0"], assumption+,
         simp add:mem_subring_mem_ring, assumption,
         rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha. \<lbrakk>0 < m; Ring R; Subring R S; Ring S; aGroup R; Ring R'; aGroup R'; ideal S (S \<diamondsuit>\<^sub>p t); Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> rHom R R'; Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; f \<noteq> \<zero>; g \<noteq> \<zero>; h \<noteq> \<zero>; u \<in> carrier R; v \<in> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g \<noteq> \<zero>\<^bsub>R'\<^esub>; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h \<noteq> \<zero>\<^bsub>R'\<^esub>; ra \<in> carrier R; f \<plusminus> g \<cdot>\<^sub>r (-\<^sub>a h) = t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r ra; P_mod R S X (S \<diamondsuit>\<^sub>p t) (t \<cdot>\<^sub>r ha); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) ra = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (u \<cdot>\<^sub>r g \<plusminus> v \<cdot>\<^sub>r h); ha \<in> carrier R; ra \<plusminus> v \<cdot>\<^sub>r (-\<^sub>a h) \<plusminus> u \<cdot>\<^sub>r (-\<^sub>a g) = t \<cdot>\<^sub>r ha; t^\<^bsup>S m\<^esup> \<in> carrier S; t^\<^bsup>S m\<^esup> \<in> carrier R; g \<cdot>\<^sub>r h \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v \<cdot>\<^sub>r (t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r u) \<in> carrier R; g \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R; t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r (v \<cdot>\<^sub>r (-\<^sub>a h)) \<in> carrier R; u \<cdot>\<^sub>r g \<in> carrier R; v \<cdot>\<^sub>r h \<in> carrier R; -\<^sub>a g \<in> carrier R; -\<^sub>a h \<in> carrier R; u \<cdot>\<^sub>r (-\<^sub>a g) \<in> carrier R; v \<cdot>\<^sub>r (-\<^sub>a h) \<in> carrier R\<rbrakk> \<Longrightarrow> t^\<^bsup>S m\<^esup> \<cdot>\<^sub>r v = t \<cdot>\<^sub>r (t^\<^bsup>S (m - Suc 0)\<^esup> \<cdot>\<^sub>r v)
[PROOF STEP]
apply (frule Ring.npClose[of S t "m - Suc 0"], assumption+,
         frule mem_subring_mem_ring[of S t], assumption,
         frule mem_subring_mem_ring[of S "t^\<^bsup>S (m - Suc 0)\<^esup>"], assumption,
         simp add:ring_tOp_assoc[THEN sym],
         simp add:ring_tOp_commute[of t "t^\<^bsup>S (m - Suc 0)\<^esup>"],
         subgoal_tac "t^\<^bsup>S m\<^esup> = t^\<^bsup>S (Suc (m - Suc 0))\<^esup>",
         simp del:Suc_pred add:Subring_tOp_ring_tOp,
         simp only:Suc_pred)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done