Theory Algebra8

(**        Algebra8  
                            author Hidetsune Kobayashi
                            Group You Santo
                            Department of Mathematics
                            Nihon University
                            hikoba@math.cst.nihon-u.ac.jp
                            May 3, 2004.
                            April 6, 2007 (revised)
  
   chapter 5. Modules
    section 4. nsum and Generators(continued)
    section 5. existence of homomorphism
    section 6. Nakayama's lemma
    section 7. direct sum and direct products of modules
    
   **)

theory Algebra8 imports Algebra7 begin


section "nsum and Generators (continued)" 

lemma (in Module) unique_expression_last:" ⟦free_generator R M H; 
        f ∈ {j. j ≤ Suc n} → H; s ∈ {j. j ≤ Suc n} → carrier R;
        g ∈ {j. j ≤ Suc n} → H; t ∈ {j. j ≤ Suc n} → carrier R;
        l_comb R M (Suc n) s f = l_comb R M (Suc n) t g; 
        inj_on f {j. j ≤ Suc n}; inj_on g {j. j ≤ Suc n}; 
        f (Suc n) = g (Suc n)⟧  ⟹ s (Suc n) = t (Suc n)"
apply (cut_tac sc_Ring, frule Ring.whole_ideal, frule free_generator_sub)
apply (frule l_comb_mem[of "carrier R" H s "Suc n" f], assumption+,
       frule l_comb_mem[of "carrier R" H t "Suc n" g], assumption+)
apply (frule ag_r_inv1[of "l_comb R M (Suc n) t g"],
       simp only:linear_span_iOp_closedTr2,
             thin_tac "l_comb R M (Suc n) t g ∈ carrier M",
       frule sym, 
             thin_tac "l_comb R M (Suc n) s f = l_comb R M (Suc n) t g",
             simp,
             thin_tac "l_comb R M (Suc n) t g = l_comb R M (Suc n) s f",
       subgoal_tac "(λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)) ∈ 
                                      {j. j ≤ Suc n} → carrier R",
            simp add:l_comb_Suc,
       frule funcset_mem[of s "{j. j ≤ Suc n}" "carrier R" "Suc n"], 
                  simp,
       frule funcset_mem[of t "{j. j ≤ Suc n}" "carrier R" "Suc n"], 
                  simp,
       frule funcset_mem[of g "{j. j ≤ Suc n}" H "Suc n"], 
                  simp,
       frule subsetD[of H "carrier M" "g (Suc n)"], assumption+,
       frule func_pre[of s], frule func_pre[of t], frule func_pre[of f],
            frule func_pre[of g], 
            frule func_pre[of "λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)"],
       frule l_comb_mem[of "carrier R" H s n f], assumption+,
       frule l_comb_mem[of "carrier R" H "λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)" 
               n g], assumption+,
       frule sc_mem[of "s (Suc n)" "g (Suc n)"], assumption+,
         cut_tac sc_mem[of "-⇩a⇘R⇙ (t (Suc n))" "g (Suc n)"],
       simp add:pOp_assocTr43[of "l_comb R M n s f" "s (Suc n) ⋅⇩s g (Suc n)"],
         simp add:ag_pOp_commute[of "s (Suc n) ⋅⇩s g (Suc n)"],
         simp add:pOp_assocTr43[THEN sym, of "l_comb R M n s f"])
  apply (frule Ring.ring_is_ag[of R],
         frule aGroup.ag_mOp_closed[of R "t (Suc n)"], assumption+,
         simp add:sc_l_distr[THEN sym],
         simp add:l_comb_add[THEN sym, of "carrier R" H s n f 
                  "λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)" n g])
  apply (frule jointfun_hom[of f n H g n H], assumption+,
         frule jointfun_hom[of s n "carrier R" "λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)"
          n "carrier R"], assumption+, simp)
  apply (subgoal_tac "(s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))) ⋅⇩s g (Suc n) = 
            l_comb R M 0 (λx∈{0::nat}. (s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))))
               (λx∈{0::nat}. (g (Suc n)))",
         simp,
         thin_tac "(s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))) ⋅⇩s g (Suc n) =
     l_comb R M 0 (λx∈{0}. s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n)))
      (λx∈{0}. g (Suc n))") 
   apply (subgoal_tac "(λx∈{0::nat}. (s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n)))) ∈ 
           {j. j ≤ (0::nat)} → carrier R",
          subgoal_tac "(λx∈{0::nat}. g (Suc n)) ∈  {j. j ≤ (0::nat)} → H") 
   apply (simp add:l_comb_add[THEN sym] del: Pi_split_insert_domain)
apply (cut_tac unique_expression3_1[of H "jointfun (Suc (n + n)) 
         (jointfun n f n g) 0 (λx∈{0}. g (Suc n))" "Suc (n + n)" 
      "jointfun (Suc (n + n))
        (jointfun n s n (λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x))) 0
        (λx∈{0}. s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n)))"], simp del: Pi_split_insert_domain,
   thin_tac "l_comb R M (Suc (Suc (n + n)))
   (jointfun (Suc (n + n)) (jointfun n s n (λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x))) 0
   (λx∈{0}. s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))))
      (jointfun (Suc (n + n)) (jointfun n f n g) 0 (λx∈{0}. g (Suc n))) =
     𝟬",
     thin_tac "(λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)) ∈ {j. j ≤ Suc n} → carrier R",
     thin_tac "l_comb R M n s f ∈ carrier M",
     thin_tac "jointfun n f n g ∈ {j. j ≤ Suc (n + n)} → H",
     thin_tac "jointfun n s n (λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x))
                     ∈ {j. j ≤ Suc (n + n)} → carrier R",
     thin_tac "(λx∈{0}. s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))) ∈ {0} → carrier R")
apply (thin_tac " (-⇩a⇘R⇙ (t (Suc n))) ⋅⇩s g (Suc n) ∈ carrier M",
        thin_tac "-⇩a⇘R⇙ (t (Suc n)) ∈ carrier R",
        thin_tac "l_comb R M n (λx∈{j. j ≤ Suc n}. -⇩a⇘R⇙ (t x)) g ∈ carrier M")
 apply ((erule exE)+, (erule conjE)+, erule exE, (erule conjE)+)
   apply (frule_tac s = ta and n = m and m = ga in unique_expression1[of H],
          assumption+, simp)
   apply (drule_tac x = m in bspec, simp)
    apply (simp add:jointfun_def[of "Suc (n + n)"] sliden_def,
          thin_tac "𝟬 = l_comb R M m ta ga",
          thin_tac "ta m = s (Suc n) ±⇘R⇙ -⇩a⇘R⇙ (t (Suc n))",
          frule Ring.ring_is_ag[of R],
          rotate_tac -2, frule sym,
       subst aGroup.ag_eq_diffzero[of R "s (Suc n)" "t (Suc n)"], assumption+)
       apply (rule sym, assumption) apply assumption
   apply (rule Pi_I,
          case_tac "x ≤ Suc (n + n)", simp add:jointfun_def del: Pi_split_insert_domain, 
          simp add:Pi_def del: Pi_split_insert_domain,
          rule impI, simp add:sliden_def del: Pi_split_insert_domain,
          simp add:Pi_def, simp add:jointfun_def sliden_def del: Pi_split_insert_domain)
     apply (rule Pi_I,
          case_tac "x ≤ Suc (n + n)",
          simp add:jointfun_def[of "Suc (n+n)"] del: Pi_split_insert_domain,
          simp add:Pi_def,
          simp add:jointfun_def[of "Suc (n + n)"] sliden_def del: Pi_split_insert_domain,
          rule aGroup.ag_pOp_closed, assumption+,
          simp add: Nset_pre1 del: Pi_split_insert_domain,
          simp add:im_jointfunTr1[of "Suc (n+n)" "jointfun n f n g" 0 
              "λx∈{0}. g (Suc n)"] del: Pi_split_insert_domain,
          simp add:im_jointfun[of f n H g n H] del: Pi_split_insert_domain,
          (subst jointfun_def[of "Suc (n+n)"])+, simp add:sliden_def del: Pi_split_insert_domain)
  apply (rule conjI, frule sym, thin_tac "f (Suc n) = g (Suc n)",
         simp add:inj_on_def[of f],
         rule contrapos_pp, simp+, simp add:image_def, erule exE, 
         erule conjE,
         drule_tac a = "Suc n" in forall_spec, simp,
         drule_tac a = x in forall_spec, simp, simp)
   apply (simp add:inj_on_def[of g],
         rule contrapos_pp, simp+, simp add:image_def, erule exE, 
         erule conjE,
         drule_tac a = "Suc n" in forall_spec, simp,
         drule_tac a = x in forall_spec, simp, simp)
        
    apply (simp)
    apply (rule Pi_I, simp,
           rule aGroup.ag_pOp_closed, assumption+)
    apply (subst l_comb_def, simp,
           rule aGroup.ag_mOp_closed, simp add:Ring.ring_is_ag,
           simp add:Pi_def, simp add:Pi_def)
    apply (rule Pi_I, simp,
           frule Ring.ring_is_ag[of R],
           rule aGroup.ag_mOp_closed[of R], assumption+,
           simp add:Pi_def)
done

lemma (in Module) unique_exprTr7p1:"  ⟦free_generator R M H;
  ∀f s g t m.
   f ∈ {j. j ≤ n} → H ∧ inj_on f {j. j ≤ n} ∧ s ∈ {j. j ≤ n} → carrier R ∧
   g ∈ {j. j ≤ m} → H ∧ inj_on g {j. j ≤ m} ∧ t ∈ {j. j ≤ m} → carrier R ∧
   l_comb R M n s f = l_comb R M m t g ∧ 
         (∀j≤n. s j ≠ 𝟬⇘R⇙) ∧ (∀k≤m. t k ≠ 𝟬⇘R⇙) ⟶
           n = m ∧
   (∃h. h ∈ {j. j ≤ n} → {j. j ≤ n} ∧
                (∀l≤n. cmp f h l = g l ∧ cmp s h l = t l));
   f ∈ {j. j ≤ Suc n} → H; s ∈ {j. j ≤ Suc n} → carrier R;
   g ∈ {j. j ≤ Suc n} → H; t ∈ {j. j ≤ Suc n} → carrier R;
   l_comb R M (Suc n) s f = l_comb R M (Suc n) t g; ∀j≤Suc n. s j ≠ 𝟬⇘R⇙;
   ∀k≤Suc n. t k ≠ 𝟬⇘R⇙; inj_on f {j. j ≤ Suc n}; inj_on g {j. j ≤ Suc n}; 
   f (Suc n) = g (Suc n)⟧ ⟹ ∃h. h ∈ {j. j ≤ Suc n} → {j. j ≤ Suc n} ∧
              (∀l≤Suc n. cmp f h l = g l ∧ cmp s h l = t l)"
apply (cut_tac sc_Ring, frule Ring.whole_ideal,
       frule Ring.ring_is_ag,
       frule free_generator_sub)
  apply (frule_tac f = f and n = n and s = s and g = g and t = t in 
         unique_expression_last[of H], assumption+)
  apply (simp add:l_comb_Suc)
  apply (frule_tac f = f in func_pre, frule_tac f = s in func_pre,
         frule_tac f = g in func_pre, frule_tac f = t in func_pre,
         cut_tac n = n in Nsetn_sub,
         frule_tac f = f and A = "{j. j ≤ Suc n}" and ?A1.0 = "{j. j ≤ n}" in 
         restrict_inj, assumption+,
         frule_tac f = g and A = "{j. j ≤ Suc n}" and ?A1.0 = "{j. j ≤ n}" in 
         restrict_inj, assumption+)
  apply (frule_tac s = s and m = f and n = n in l_comb_mem[of "carrier R" H], 
         assumption+,
         frule_tac s = t and m = g and n = n in l_comb_mem[of "carrier R" H], 
         assumption+,
         frule_tac f = t and A = "{j. j ≤ Suc n}" and B = "carrier R" and 
         x = "Suc n" in funcset_mem, simp,
         frule_tac f = g and A = "{j. j ≤ Suc n}" and B = H and x = "Suc n" 
         in funcset_mem, simp,
         frule_tac c = "g (Suc n)" in subsetD[of H "carrier M"], assumption+,
         frule_tac a = "t (Suc n)" and m = "g (Suc n)" in sc_mem, assumption+)
  apply (frule_tac x = "l_comb R M n s f" and y = "t (Suc n) ⋅⇩s g (Suc n)" and
         z = "-⇩a (t (Suc n) ⋅⇩s g (Suc n))" in ag_pOp_assoc, assumption+,
         rule ag_mOp_closed, assumption, simp add:ag_r_inv1 ag_r_zero,
         frule_tac x = "t (Suc n) ⋅⇩s g (Suc n)" in ag_mOp_closed,
         simp add:ag_pOp_assoc, simp add:ag_r_inv1 ag_r_zero,
         rotate_tac -2, frule sym,
                thin_tac "l_comb R M n t g = l_comb R M n s f")
  apply (drule_tac x = f in spec,
  rotate_tac -1,
  drule_tac x = s in spec,
  rotate_tac -1,
  drule_tac x = g in spec,
  rotate_tac -1, drule_tac x = t in spec,
  rotate_tac -1, drule_tac x = n in spec)
  apply (cut_tac n = n in Nsetn_sub_mem1, simp)
  apply (erule exE, erule conjE)
  apply (subgoal_tac "(jointfun n h 0 (λj. (Suc n))) ∈ 
                       {j. j ≤ Suc n} → {j. j ≤ Suc n}",
        subgoal_tac "∀l≤Suc n. cmp f (jointfun n h 0 (λj. (Suc n))) l = 
          g l ∧ cmp s (jointfun n h 0 (λj. (Suc n))) l = t l",
   thin_tac "∀k≤Suc n. t k ≠ 𝟬⇘R⇙", thin_tac "inj_on f {j. j ≤ Suc n}",
   thin_tac "inj_on g {j. j ≤ Suc n}", thin_tac "f (Suc n) = g (Suc n)",
   thin_tac "s (Suc n) = t (Suc n)",
   thin_tac "f ∈ {j. j ≤ n} → H", thin_tac "s ∈ {j. j ≤ n} → carrier R",
   thin_tac "g ∈ {j. j ≤ n} → H", thin_tac "t ∈ {j. j ≤ n} → carrier R",
   thin_tac "{j. j ≤ n} ⊆ {j. j ≤ Suc n}",
   thin_tac "∀l≤n. cmp f h l = g l ∧ cmp s h l = t l",
   thin_tac "l_comb R M n t g ∈ carrier M", blast)
  apply (rule allI, rule impI, case_tac "l ≤ n", 
                                simp add:cmp_def jointfun_def,
         simp add:cmp_def, simp add:jointfun_def sliden_def,
         frule_tac y = l and x = n in not_le_imp_less, thin_tac "¬ l ≤ n",
         frule_tac m = n and n = l in Suc_leI,
         frule_tac m = l and n = "Suc n" in Nat.le_antisym, assumption,
         simp)
  apply (rule Pi_I,
         case_tac "xa ≤ n", simp add:jointfun_def, rule impI,
         frule_tac x = x and f = h and A = "{j. j ≤ n}" and 
         B = "{j. j ≤ n}" in funcset_mem, simp, simp,
         simp add:jointfun_def, rule impI,frule_tac x = x and f = h and 
         A = "{j. j ≤ n}" and B = "{j. j ≤ n}" in funcset_mem, simp, simp)
done

lemma (in Module) unique_expression7:"free_generator R M H ⟹
 ∀f s g t m. f ∈ {j. j ≤ (n::nat)} → H ∧ inj_on f {j. j ≤ n} ∧
    s ∈ {j. j ≤ n} → carrier R ∧
    g ∈ {j. j ≤ (m::nat)} → H ∧ inj_on g {j. j ≤ m} ∧
    t ∈ {j. j ≤ m} → carrier R ∧ l_comb R M n s f = l_comb R M m t g ∧
    (∀j ∈ {j. j ≤ n}. s j ≠ 𝟬⇘R⇙) ∧ (∀k ∈ {j. j ≤ m}. t k ≠ 𝟬⇘R⇙ ) ⟶ n = m ∧ 
    (∃h. h ∈ {j. j ≤ n} → {j. j ≤ n} ∧ (∀l ∈ {j. j ≤ n}. (cmp f h) l = g l
      ∧ (cmp s h) l = t l))"
apply (cut_tac sc_Ring,
        frule Ring.ring_is_ag[of R],
        frule free_generator_sub[of H])
apply (induct_tac n)
 apply (rule allI)+
 apply (rule impI, (erule conjE)+)
 apply (frule_tac H = H and f = f and n = 0 and s = s and g = g and m = m 
        and t = t in unique_expression7_1, assumption+, simp del: Pi_split_insert_domain)
 apply (frule_tac H = H and f = f and n = 0 and s = s and g = g and m = m 
        and t = t in  unique_expression6, (simp del: Pi_split_insert_domain) +)
 apply (simp add:l_comb_def del: Pi_split_insert_domain)
 apply (frule_tac f = s in funcset_mem[of _ "{0}" "carrier R" 0], simp del: Pi_split_insert_domain,
        frule_tac f = t in funcset_mem[of _ "{0}" "carrier R" 0], simp del: Pi_split_insert_domain,
        frule_tac f = g in funcset_mem[of _ "{0}" H 0], simp del: Pi_split_insert_domain,
        frule_tac c = "g 0" in subsetD[of "H" "carrier M"], assumption+)
 apply (frule_tac a = "s 0" and m = "g 0" in sc_mem, assumption+, 
        frule_tac a = "t 0" and m = "g 0" in sc_mem, assumption+,
        frule_tac a = "s 0 ⋅⇩s g 0" and b = "t 0 ⋅⇩s g 0" in ag_eq_diffzero)
  apply assumption
 apply (simp only:sc_minus_am1, 
        thin_tac "(s 0 ⋅⇩s g 0 = t 0 ⋅⇩s g 0) = (𝟬 = 𝟬)")
 apply (frule_tac x = "t 0" in aGroup.ag_mOp_closed[of R], assumption+)
 apply (simp add:sc_l_distr[THEN sym],
        frule_tac h = "g 0" and a = "s 0 ±⇘R⇙ -⇩a⇘R⇙ (t 0)" in 
        free_gen_coeff_zero[of H],
        assumption+,
        rule aGroup.ag_pOp_closed[of R], assumption+) 
apply (simp add:aGroup.ag_eq_diffzero[THEN sym, of R],
        simp add:cmp_def,
        cut_tac Pi_I[of "{0::nat}" "id" "%_. {0::nat}"],
        subgoal_tac "f (id 0) = g 0 ∧ s (id 0) = t 0", blast,
        simp add:id_def, simp add:id_def)
(** n = 0 done **)
apply ((rule allI)+, rule impI)
 apply (erule conjE)+
  apply (frule_tac H = H and f = f and n = "Suc n" and s = s and g = g and 
       m = m and t = t in unique_expression6, assumption+)
  apply (cut_tac k = "Suc n" in finite_Collect_le_nat,
         frule_tac A = "{j. j ≤ Suc n}" and f = f in inj_on_iff_eq_card,
         simp)
  apply (cut_tac k = m in finite_Collect_le_nat,
         frule_tac A = "{j. j ≤ m}" and f = g in inj_on_iff_eq_card,
         simp,
         thin_tac "card (g ` {j. j ≤ m}) = Suc m")
  apply (frule sym, thin_tac "Suc n = m", simp)  
  apply (cut_tac a = "Suc n" and A = "{j. j ≤ Suc n}" and f = g in 
         mem_in_image2) apply simp apply (
         rotate_tac -6) apply ( frule sym,
         thin_tac "f ` {j. j ≤ Suc n} = g ` {j. j ≤ Suc n}", simp,
         simp add:image_def) apply ( erule exE, erule conjE)
  apply (case_tac "x = Suc n", simp, thin_tac "x = Suc n",
         rotate_tac -1, frule sym, thin_tac "g (Suc n) = f (Suc n)") 
  apply (rule_tac n = n and f = f and s = s and g = g and t = t in 
          unique_exprTr7p1[of H], assumption+)

 apply (rotate_tac -2, frule sym, thin_tac "g (Suc n) = f x")
 apply (frule Ring.whole_ideal)
  apply (frule_tac s = s and n = n and f = f and j = x in 
         l_comb_transpos1[of "carrier R" H], assumption+,
         rule noteq_le_less, assumption+, simp) apply (
         thin_tac "l_comb R M (Suc n) s f = l_comb R M (Suc n) t g")
  apply (frule_tac f = "cmp f (transpos x (Suc n))" and n = n and 
         s = "cmp s (transpos x (Suc n))" and g = g and t = t in 
         unique_exprTr7p1[of H], assumption+)
  apply (rule Pi_I,
         simp add:cmp_def, rule_tac f = f and A = "{j. j ≤ Suc n}" and B = H 
         and x = "transpos x (Suc n) xa" in funcset_mem, simp,
         simp add:transpos_mem)
  apply (rule Pi_I,
         simp add:cmp_def, rule_tac f = s and A = "{j. j ≤ Suc n}" and 
         B = "carrier R" and x = "transpos x (Suc n) xa" in funcset_mem, simp,
         simp add:transpos_mem)
   apply assumption+
   apply (rule allI, rule impI, simp add:cmp_def)
   apply (cut_tac i = x and n = "Suc n" and j = "Suc n" and l = j in 
              transpos_mem, simp+)
   apply (cut_tac i = x and n = "Suc n" and j = "Suc n" in transpos_inj,
          simp+)
   apply (cut_tac  i = x and n = "Suc n" and j = "Suc n" in 
              transpos_hom, simp+)    
   apply (rule_tac f = "transpos x (Suc n)" and A = "{j. j ≤ Suc n}" and 
          B = "{j. j ≤ Suc n}" and g = f and C = H in cmp_inj,
          assumption+)
   apply (simp add:cmp_def transpos_ij_2)
 apply (erule exE, erule conjE)  
   apply (cut_tac  i = x and n = "Suc n" and j = "Suc n" in 
              transpos_hom, simp+)
   apply (simp add:cmp_assoc[THEN sym]) 
   apply (frule_tac f = h and A = "{j. j ≤ Suc n}" and B = "{j. j ≤ Suc n}" 
          and g = "transpos x (Suc n)" and C = "{j. j ≤ Suc n}" in 
          cmp_fun, assumption+)
   apply (thin_tac "∀f s g t m. f ∈ {j. j ≤ n} → H ∧ inj_on f {j. j ≤ n} ∧
   s ∈ {j. j ≤ n} → carrier R ∧ g ∈ {j. j ≤ m} → H ∧ inj_on g {j. j ≤ m} ∧
   t ∈ {j. j ≤ m} → carrier R ∧ l_comb R M n s f = l_comb R M m t g ∧
   (∀j≤n. s j ≠ 𝟬⇘R⇙) ∧ (∀k≤m. t k ≠ 𝟬⇘R⇙) ⟶  n = m ∧
   (∃h. h ∈ {j. j ≤ n} → {j. j ≤ n} ∧ 
               (∀l≤n. cmp f h l = g l ∧ cmp s h l = t l))",
    thin_tac "∀j≤Suc n. s j ≠ 𝟬⇘R⇙", thin_tac "∀k≤Suc n. t k ≠ 𝟬⇘R⇙",
    thin_tac "{y. ∃x≤Suc n. y = g x} = {y. ∃x≤Suc n. y = f x}")
  apply blast
done

lemma (in Module) gen_mHom_eq:"⟦R module N; generator R M H; f ∈ mHom R M N;
       g ∈ mHom R M N; ∀h∈H. f h = g h ⟧ ⟹ f = g"
apply (rule mHom_eq[of N], assumption+)
 apply (rule ballI)
 apply (unfold generator_def, frule conjunct2, fold generator_def)
 apply (frule sym, thin_tac "linear_span R M (carrier R) H = carrier M",
        simp,
        thin_tac "carrier M = linear_span R M (carrier R) H")
 apply (simp add:linear_span_def)
 apply (case_tac "H = {}", simp, simp add:mHom_0, simp)
 apply (erule exE, (erule bexE)+)
 apply (unfold generator_def, frule conjunct1, fold generator_def)
apply (cut_tac sc_Ring, frule Ring.whole_ideal)
 apply simp
  apply (simp add: linmap_im_lincomb [of "carrier R" N])
 apply (frule_tac s = s and n = n and f = "cmp f fa" and g = "cmp g fa" in 
         Module.linear_comb_eq[of N R "f ` H"])
  apply (simp add: mHom_def aHom_def cong del: image_cong)
       apply (erule conjE)+
       apply (simp add: image_sub [of f "carrier M" "carrier N" H] cong del: image_cong)
      apply assumption
    apply (rule Pi_I, simp add:cmp_def,
         simp add:image_def, 
         frule_tac f = fa and A = "{j. j ≤ n}" and B = H and x = x in 
         funcset_mem, simp, blast)
  apply (rule Pi_I, simp add:cmp_def,
         simp add:image_def, 
         frule_tac f = fa and A = "{j. j ≤ n}" and B = H and x = x in 
         funcset_mem, simp, blast)
  apply (rule ballI, simp add:cmp_def,
         frule_tac f = fa and A = "{j. j ≤ n}" and B = H and x = j in 
         funcset_mem, simp)
   apply blast
 apply assumption
done

section "Existence of homomorphism"

definition
  fgs :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, 'a set]  ⇒
       'a set" where
  (* free generator span, A is a subset of free generator *)
  "fgs R M A = linear_span R M (carrier R) A"
 
definition
  fsp :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, 
  ('b, 'r, 'm2) Module_scheme, 'a ⇒ 'b, 'a set, 'a set, 'a ⇒ 'b] ⇒ bool" where
  "fsp R M N f H A g ⟷ g ∈ mHom R (mdl M (fgs R M A)) N ∧ (∀z∈A. f z = g z) ∧ A ⊆ H" 
 (* f ∈ H → N (not a module hom), free span pair condition *)

definition
  fsps :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, 
   ('b, 'r, 'm2) Module_scheme, 'a ⇒ 'b, 'a set] ⇒ 
                                      (('a set) * ('a ⇒ 'b)) set" where
  "fsps R M N f H = {Z. ∃A g. Z = (A, g) ∧ fsp R M N f H A g}"
         (* free span pairs *)

definition
  od_fm_fun :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, 
 ('b, 'r, 'm2) Module_scheme, 'a ⇒ 'b, 'a set] ⇒ 
                          (('a set) * ('a ⇒ 'b)) Order" where
  "od_fm_fun R M N f H = ⦇carrier = fsps R M N f H, 
     rel = {Y. Y ∈ (fsps R M N f H) × (fsps R M N f H) ∧ 
                              (fst (fst Y)) ⊆ (fst (snd Y))} ⦈" 
 (* ordered set free module with function f *)

lemma (in Module) od_fm_fun_carrier:"carrier (od_fm_fun R M N f H) = 
                    fsps R M N f H"
by (simp add:od_fm_fun_def)

lemma (in Module) fgs_submodule:"a ⊆ carrier M ⟹ 
              submodule R M (fgs R M a)"
apply (cut_tac sc_Ring, frule Ring.whole_ideal)
apply (subst fgs_def) 
apply (rule linear_span_subModule, assumption, assumption)
done

lemma (in Module) fgs_sub_carrier:"a ⊆ carrier M ⟹ (fgs R M a) ⊆ carrier M" 
by (frule fgs_submodule[of a], 
       rule submodule_subset, assumption+)

lemma (in Module) elem_fgs:"⟦a ⊆ carrier M; x ∈ a⟧ ⟹ x ∈ fgs R M a"
apply (simp add:fgs_def)
apply (frule l_span_cont_H[of a])
apply (simp add:subsetD)
done

lemma (in Module) fst_chain_subset:"⟦R module N; free_generator R M H;
 f ∈ H → carrier N; C ⊆ fsps R M N f H; (a, b) ∈ C⟧  ⟹ a ⊆ carrier M"
apply (subgoal_tac "a ⊆ H", frule free_generator_sub)
 apply (rule subset_trans, assumption+)
 apply (frule_tac A = C and B = "fsps R M N f H" and c = "(a, b)" in subsetD, 
        assumption+) 
 apply (simp add:fsps_def fsp_def)
done 

lemma (in Module) empty_fsp:"⟦R module N; free_generator R M H; 
     f ∈ H → carrier N⟧ ⟹ ({}, (λx∈{𝟬⇘M⇙}. 𝟬⇘N⇙)) ∈ fsps R M N f H"
apply (simp add:fsps_def fsp_def,
       simp add:fgs_def linear_span_def,
       cut_tac submodule_0,
       frule mdl_is_module[of "{𝟬}"])
apply (rule Module.mHom_test, assumption+)
apply (rule conjI)
 apply (rule Pi_I, simp add:mdl_carrier,
        rule Module.module_inc_zero[of N R], assumption+)
 apply (simp add:mdl_carrier)
 apply (simp add:mdl_def, fold mdl_def)
 apply (cut_tac ag_inc_zero, simp add:ag_l_zero,
        frule Module.module_is_ag[of N R],
        frule aGroup.ag_inc_zero[of N], simp add:aGroup.ag_l_zero[of N])
 apply (rule ballI, frule_tac a = a in sc_a_0, simp)
 apply (simp add:Module.sc_a_0)
done
  
lemma (in Module) mem_fgs_l_comb:"⟦K ≠ {}; K ⊆ carrier M; x ∈ fgs R M K⟧ ⟹ 
        ∃(n::nat).  
        ∃f ∈ {j. j ≤ (n::nat)} → K. ∃s ∈ {j. j ≤ n} → carrier R.
                    x = l_comb R M n s f" 
apply (simp add:fgs_def linear_span_def)
done

lemma PairE_lemma: "∃x y. p = (x, y)" by auto

lemma (in Module) fsps_chain_boundTr1:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; C ⊆ fsps R M N f H; 
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; ∀a b. (a, b) ∈ C ⟶ 
              (a, b) ∈ fsps R M N f H; ∃x. (∃b. (x, b) ∈ C) ∧ x ≠ {}⟧ ⟹ 
      fa ∈ {j. j ≤ (n::nat)} → ⋃{a. ∃b. (a, b) ∈ C} 
                       ⟶ (∃(c, d) ∈ C. fa ` {j. j ≤ n} ⊆ c)"  
apply (induct_tac n)
 apply (rule impI, simp del: Pi_split_insert_domain)
 apply ((erule exE)+, erule conjE, erule exE)
 apply (frule_tac f = fa and A = "{0}" and B = "⋃{a. ∃b. (a, b) ∈ C}" and 
                      ?A1.0 = "{0}" in image_sub, simp, simp) 
 apply blast

apply (rule impI)
 apply (frule func_pre, simp) 
 apply (frule_tac f = fa and A = "{j. j ≤ (Suc n)}" and 
        B = "⋃{a. ∃b. (a, b) ∈ C}" and x = "Suc n" in funcset_mem, simp) 
 apply simp

 apply ((erule exE)+, erule conjE, erule exE, erule conjE, erule exE)
 apply (erule bexE)
 apply (drule_tac x = "(xa, ba)" in bspec, assumption, 
        drule_tac x = xb in bspec, assumption+)
 apply (erule disjE, simp)
 apply (subgoal_tac "(λ(c, d). fa ` {j. j ≤ Suc n} ⊆ c) xb")
 apply auto[1]
 apply (subgoal_tac "(λ(c, d). fa ` {j. j ≤ Suc n} ⊆ c) xb")
 apply (blast,
        cut_tac p = xb in PairE_lemma,
        (erule exE)+, simp, rule subsetI, simp add:image_def,
           erule exE, erule conjE,
        case_tac "xe = Suc n", simp, simp add:subsetD,
        frule_tac m = xe and n = "Suc n" in noteq_le_less, assumption,
        frule_tac x = xe and n = n in Suc_less_le,
        thin_tac "xe ≤ Suc n", thin_tac "xe < Suc n",
        cut_tac c = xd and A = "{y. ∃x≤n. y = fa x}" and B = xc in
           subsetD, simp, simp, blast, assumption)
 apply (subgoal_tac "(λ(c, d). fa ` {j. j ≤ Suc n} ⊆ c) (xa, ba)")
 apply auto[1]
   apply (simp, rule subsetI, simp add:image_def, erule exE, erule conjE,
         case_tac "xd = Suc n", simp,
         frule_tac m = xd and n = "Suc n" in noteq_le_less, assumption,
           frule_tac x = xd and n = n in Suc_less_le,
           thin_tac "xd ≤ Suc n", thin_tac "xd < Suc n",
         cut_tac p = xb in PairE_lemma, (erule exE)+, simp,
         cut_tac c = "fa xd" and A = "{y. ∃x≤n. y = fa x}" and B = xe in 
          subsetD, assumption, simp, blast)
   apply (rule_tac c = "fa xd" and A = xe and B = xa in subsetD, assumption+)
done

lemma (in Module) fsps_chain_boundTr1_1:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; C ⊆ fsps R M N f H; 
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; 
       ∃x. (∃b. (x, b) ∈ C) ∧ x ≠ {}; 
       fa ∈ {j. j ≤ (n::nat)} → ⋃{a. ∃b. (a, b) ∈ C}⟧ ⟹ 
        ∃(c, d) ∈ C. fa ` {j. j ≤ n} ⊆ c" 
apply (subgoal_tac "∀a b. (a, b) ∈ C ⟶ (a, b) ∈ fsps R M N f H")
apply (simp add:fsps_chain_boundTr1)
apply ((rule allI)+, rule impI, simp add:subsetD)
done

lemma (in Module) fsps_chain_boundTr1_2:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; C ⊆ fsps R M N f H; 
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; 
       ∃x. (∃b. (x, b) ∈ C) ∧ x ≠ {}; 
       fa ∈ {j. j ≤ (n::nat)} → ⋃{a. ∃b. (a, b) ∈ C}⟧ ⟹ 
       ∃P ∈ C. fa ` {j. j ≤ n} ⊆ fst P"  
apply (frule_tac N = N and f = f and C = C and fa = fa and n = n in 
         fsps_chain_boundTr1_1, assumption+) 
apply (erule bexE)
apply (cut_tac p = x in PairE_lemma, (erule exE)+)
apply (subgoal_tac "fa ` {j. j ≤ n} ⊆ fst x")
apply blast
apply simp
done

lemma (in Module) eSum_in_SubmoduleTr:"⟦H ⊆ carrier M; K ⊆ H⟧ ⟹
      f ∈ {j. j ≤ (n::nat)} → K ∧ s ∈ {j. j ≤ n} → carrier R  ⟶
      l_comb R (mdl M (fgs R M K)) n s f = l_comb R M n s f"
apply (induct_tac n)    
 apply (rule impI, (erule conjE)+)
 apply (simp add:l_comb_def del: Pi_split_insert_domain, simp add:mdl_def del: Pi_split_insert_domain, rule impI) 
 apply (simp add:fgs_def del: Pi_split_insert_domain, frule subset_trans[of K H "carrier M"], assumption+) 
 apply (frule funcset_mem[of f "{0}" K 0], simp del: Pi_split_insert_domain,
        frule l_span_cont_H[of K], simp add:subsetD)

apply (rule impI, erule conjE)
 apply (frule func_pre[of  _ _ K], frule func_pre[of  _ _ "carrier R"],
        simp)
 apply (simp add:l_comb_def, simp add:mdl_def)
 apply (rule impI, simp add:fgs_def,frule subset_trans[of K H "carrier M"], 
        assumption+)  
  apply (frule_tac x = "Suc n" and A = "{j. j ≤ Suc n}" in
         funcset_mem[of f _ K], simp,
        frule l_span_cont_H[of K], simp add:subsetD)
done

lemma (in Module) eSum_in_Submodule:"⟦H ⊆ carrier M; K ⊆ H; 
      f ∈ {j. j ≤ (n::nat)} → K; s ∈ {j. j ≤ n} → carrier R⟧ ⟹ 
      l_comb R (mdl M (fgs R M K)) n s f = l_comb R M n s f"  
apply (simp add:eSum_in_SubmoduleTr)
done

lemma (in Module) fgs_generator:"H ⊆ carrier M ⟹
       generator R (mdl M (fgs R M H)) H" 
apply (simp add:generator_def, simp add:mdl_def, fold mdl_def) 
apply (rule conjI)
 apply (simp add:fgs_def)
 apply (simp add:l_span_cont_H)
apply (rule equalityI)
 apply (rule subsetI, simp add:linear_span_def) 
 apply (case_tac "H = {}", simp add:mdl_def)
 apply (simp add:fgs_def linear_span_def)
 apply simp apply (erule exE, (erule bexE)+)
 apply (cut_tac f = f and n = n and s = s in eSum_in_Submodule[of H H],
        assumption+, simp, assumption+)
 apply simp
 apply (simp add:fgs_def)
 apply (cut_tac sc_Ring, frule Ring.whole_ideal)        
 apply (simp add:l_comb_mem_linear_span)
apply (rule subsetI)
 apply (case_tac "H = {}", simp)
 apply (simp add:fgs_def linear_span_def mdl_def)
 apply (frule_tac x = x in mem_fgs_l_comb[of H], assumption+)
 apply (erule exE, erule bexE, erule bexE)
 apply (simp add:eSum_in_Submodule[THEN sym, of H H])
 apply (frule fgs_submodule[of H],
        frule mdl_is_module[of "fgs R M H"])
 apply (rule Module.l_comb_mem_linear_span[of "mdl M (fgs R M H)" R "carrier R" H], assumption+)
 apply (cut_tac sc_Ring, rule Ring.whole_ideal, assumption)
 apply (simp add:mdl_carrier, simp add:fgs_def l_span_cont_H,
      assumption+)
done 

lemma (in Module) fgs_mono:"⟦free_generator R M H; J ⊆ K; K ⊆ H⟧
       ⟹ fgs R M J ⊆ fgs R M K"   (* H1 ⊆ H2 , J ⊆ K *)
apply (cut_tac sc_Ring)    
apply (case_tac "J = {}")
 apply (simp add:fgs_def linear_span_def)
 apply (case_tac "K = {}") apply simp apply simp
 apply (frule nonempty_ex [of K])
 apply (erule exE)
 apply (subgoal_tac "(λj. x) ∈ {j. j ≤ (0::nat)} → K",
        subgoal_tac "(λj. 𝟬⇘R⇙) ∈ {j. j ≤ (0::nat)} → carrier R",
        subgoal_tac "𝟬⇘M⇙ = l_comb R M 0 (λj. 𝟬⇘R⇙) (λj. x)")
 apply blast
 apply (simp add:l_comb_def)
 apply (frule free_generator_sub[of H],
        frule subset_trans[of K H "carrier M"], assumption+,
        frule_tac c = x in subsetD[of K "carrier M"], assumption+,
        simp add:sc_0_m)
 apply (rule Pi_I,
        frule Ring.ring_is_ag [of "R"],
        simp add:aGroup.ag_inc_zero[of R])
 apply (rule Pi_I, assumption)
apply (subgoal_tac "K ≠ {}") prefer 2 apply (rule contrapos_pp, simp+)
 apply (rule subsetI)
 apply (simp add:fgs_def, simp add:linear_span_def)
 apply (erule exE, (erule bexE)+)
 apply (frule_tac f = f and A = "{j. j ≤ n}" and B = J and ?B1.0 = K in 
        extend_fun, assumption+)
 apply blast
done

lemma (in Module) empty_fgs:"fgs R M {} = {𝟬}"
by(simp add:fgs_def linear_span_def)

lemma (in Module) mem_fsps_snd_mHom:"⟦R module N; free_generator R M H;
     f ∈ H → carrier N; (a, b) ∈ fsps R M N f H⟧  ⟹ 
                    b ∈ mHom R (mdl M (fgs R M a)) N"
by (simp add:fsps_def fsp_def)
(*
lemma (in Module) mem_fsps_snd_mHom1:"⟦R module N; free_generator R M H;
     f ∈ H → carrier N; (a, b) ∈ fsps R M N f H⟧  ⟹ 
                    b ∈ mHom R (mdl M (fgs R M a)) N"
by (simp add:fsps_def fsp_def) *)

lemma (in Module) mem_fsps_fst_sub:"⟦R module N; free_generator R M H;
     f ∈ H → carrier N; (a, b) ∈ fsps R M N f H⟧  ⟹  a ⊆ H"
by (simp add:fsps_def fsp_def)

lemma (in Module) mem_fsps_fst_sub1:"⟦R module N; free_generator R M H;
     f ∈ H → carrier N; (a, b) ∈ fsps R M N f H⟧  ⟹  a ⊆ carrier M"
apply (simp add:fsps_def fsp_def)
apply (frule free_generator_sub[of H],
       rule subset_trans[of a H "carrier M"], simp+)
done

lemma (in Module) Order_od_fm_fun:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N⟧ ⟹ Order (od_fm_fun R M N f H)"
apply (rule Order.intro)
 apply (simp add:od_fm_fun_carrier)
 apply (rule subsetI, simp add:od_fm_fun_def)
 apply (simp add:od_fm_fun_def)
 apply (simp add:od_fm_fun_def)
 apply (cut_tac p = a in PairE_lemma, (erule exE)+,
        cut_tac p = b in PairE_lemma, (erule exE)+, simp)
 apply (frule_tac a = x and b = y in mem_fsps_snd_mHom[of N H f], assumption+,
       frule_tac a = x and b = ya in mem_fsps_snd_mHom[of N H f], assumption+)
 apply (frule_tac a = x and b = y in mem_fsps_fst_sub[of N H f], assumption+,
        frule free_generator_sub,
        frule_tac A = x and B = H and C = "carrier M" in subset_trans,
        assumption+)  
apply (frule_tac a = x in fgs_submodule,
       frule_tac H = "fgs R M x" in mdl_is_module)
 apply (thin_tac "a = (x, y)", thin_tac "b = (x, ya)")
 apply (simp add:mdl_carrier)
 apply (frule_tac H = x in fgs_generator)
 apply (frule_tac R = R and M = "mdl M (fgs R M x)" and N = N and H = x 
       and f = y and g = ya in Module.gen_mHom_eq, assumption+,
       simp add:fsps_def fsp_def, assumption)
apply (simp add:od_fm_fun_def)
done

lemma (in Module) fsps_chain_boundTr2_1:"⟦R module N; 
      free_generator R M H; f ∈ H → carrier N; C ⊆ fsps R M N f H; 
      (a, b) ∈ C; (aa, ba) ∈ C; x ∈ fgs R M a; x ∈ fgs R M aa; a ⊆ aa⟧
      ⟹ b x = ba x"
apply (cut_tac sc_Ring, frule Ring.whole_ideal, frule free_generator_sub)
 apply (frule mem_fsps_snd_mHom[of N H f a b], assumption+, simp add:subsetD,
        frule mem_fsps_snd_mHom[of N H f aa ba], assumption+, simp add:subsetD)
 apply (case_tac "a = {}", simp add:empty_fgs)
 apply (cut_tac submodule_0, frule mdl_is_module[of "{𝟬}"],
        frule subsetD[of C "fsps R M N f H" "(aa, ba)"], assumption+) 
   apply (cut_tac fgs_submodule[of aa],
          frule mdl_is_module[of "fgs R M aa"])
   apply (frule Module.mHom_0[of "mdl M {𝟬}" R N b], assumption+,
        frule Module.mHom_0[of "mdl M (fgs R M aa)" R N ba], assumption+,
        simp add:mdl_def) 
   apply (frule mem_fsps_fst_sub[of N H f aa ba], assumption+,
          rule subset_trans[of aa H "carrier M"], assumption+)
 apply (frule nonempty_ex[of a], erule exE,
        frule_tac c = xa in subsetD[of a aa], assumption,
        frule_tac x = xa in nonempty[of _ aa],
        thin_tac "xa ∈ a", thin_tac "xa ∈ aa")
 apply (frule mem_fsps_fst_sub[of N H f aa ba], assumption+,
        simp add:subsetD)
 apply (frule mem_fgs_l_comb[of a x],
        frule subset_trans[of a aa H], assumption+,
        rule subset_trans[of a H "carrier M"], assumption+)
 apply (erule exE, (erule bexE)+)
 apply (frule_tac f = fa and A = "{j. j ≤ n}" and B = a and ?B1.0 = aa in 
                  extend_fun, assumption+)
 apply (frule subsetD[of C "fsps R M N f H" "(a, b)"], assumption+,
        frule subsetD[of C "fsps R M N f H" "(aa, ba)"], assumption+,
        thin_tac "C ⊆ fsps R M N f H")
 apply (cut_tac fgs_submodule[of a],
        frule mdl_is_module[of "fgs R M a"],
        cut_tac fgs_submodule[of  aa], 
        frule mdl_is_module[of "fgs R M aa"]) (* 
 apply (simp add:fsps_def fsp_def, (erule conjE)+) *)
 apply (frule subset_trans[of a aa H], assumption+)
 apply (frule_tac f1 = fa and n1 = n and s1 = s in eSum_in_Submodule[THEN sym,
        of H a], assumption+,
        frule_tac s = s and n = n and g = fa in Module.linmap_im_lincomb[of 
        "mdl M (fgs R M a)" R "carrier R" N _ a], assumption+,
        simp add:mdl_carrier,
        subst fgs_def, rule_tac l_span_cont_H,
        frule subset_trans[of a H "carrier M"], assumption+, simp,
        thin_tac "b (l_comb R (mdl M (fgs R M a)) n s fa) = 
                                                  l_comb R N n s (cmp b fa)",
        rotate_tac -1, frule sym, 
        thin_tac "l_comb R M n s fa = l_comb R (mdl M (fgs R M a)) n s fa",
        simp,
        thin_tac "l_comb R (mdl M (fgs R M a)) n s fa = l_comb R M n s fa")
 apply (frule_tac f1 = fa and n1 = n and s1 = s in eSum_in_Submodule[THEN sym,
        of H aa], assumption+,
        frule_tac s = s and n = n and g = fa in Module.linmap_im_lincomb[of 
        "mdl M (fgs R M aa)" R "carrier R" N _ aa], assumption+,
        simp add:mdl_carrier,
        subst fgs_def, rule_tac l_span_cont_H,
        frule subset_trans[of a H "carrier M"], assumption+, simp+,
        thin_tac "l_comb R M n s fa = l_comb R (mdl M (fgs R M aa)) n s fa",
        thin_tac "ba (l_comb R (mdl M (fgs R M aa)) n s fa) =
        l_comb R N n s (cmp ba fa)")
 apply (simp add:fsps_def fsp_def)
 apply (rule_tac s = s and n = n and f = "cmp b fa" and g = "cmp ba fa" in
        Module.linear_comb_eq[of N R "f ` H"], assumption+,
        simp add:image_sub0, assumption)
 apply (rule Pi_I, simp add:cmp_def,
       frule_tac x = xa and f = fa and A = "{j. j ≤ n}" and B = a in 
       funcset_mem, simp,
       frule_tac m = "fa xa" in Module.mHom_mem[of "mdl M (fgs R M a)" R N b],
         assumption+,
       simp add:mdl_carrier fgs_def, rule_tac c = "fa xa" in 
         subsetD[of a "linear_span R M (carrier R) a"],
        rule l_span_cont_H,
        frule subset_trans[of a aa H], assumption+,
        rule subset_trans[of a H "carrier M"], assumption+,
        drule_tac x = "fa xa" in bspec, assumption,
        frule_tac c = "fa xa" in subsetD[of a H], assumption+,
        rotate_tac -2, frule sym, thin_tac "f (fa xa) = b (fa xa)", simp)
  apply (rule Pi_I, simp add:cmp_def,
        frule_tac x = xa and f = fa and A = "{j. j ≤ n}" and B = aa in 
        funcset_mem, simp,
        frule_tac c = "fa xa" in subsetD[of aa H], assumption+,
        drule_tac x = "fa xa" in bspec, assumption,
        rotate_tac -1, frule sym, thin_tac "f (fa xa) = ba (fa xa)",
        simp)
  apply (rule ballI, simp add:cmp_def,
        frule_tac x = j and f = fa and A = "{j. j ≤ n}" and B = a in 
        funcset_mem, simp)
  apply (frule_tac x = "fa j" in bspec, assumption,
               thin_tac "∀z∈a. f z = b z",
               frule_tac c = "fa j" in subsetD[of a aa], assumption+,
               frule_tac x = "fa j" in bspec, assumption,
               thin_tac "∀z∈aa. f z = ba z")
  apply (rotate_tac -3, frule sym, 
               thin_tac "f (fa j) = b (fa j)", frule sym,
               thin_tac "f (fa j) = ba (fa j)", simp)
  apply (simp add:subset_trans[of aa H "carrier M"])
  apply (frule subset_trans[of a aa H], assumption+,
         simp add:subset_trans[of a H "carrier M"])
done

lemma (in Module) fsps_chain_boundTr2_2:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; C ⊆ fsps R M N f H; 
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; C ≠ {}; (a, b) ∈ C; 
       x ∈ fgs R M a; (a1, b1) ∈ C; x ∈ fgs R M a1⟧ ⟹ b x = b1 x"
 apply (frule_tac x = "(a, b)" in bspec, assumption,
        thin_tac "∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a",
        frule_tac x = "(a1, b1)" in bspec, assumption,
        thin_tac "∀ba∈C. fst (a, b) ⊆ fst ba ∨ fst ba ⊆ fst (a, b)", simp)
 apply (erule disjE)
 apply (rule fsps_chain_boundTr2_1[of N H f C a b a1 b1], assumption+)  
 apply (frule fsps_chain_boundTr2_1[of N H f C a1 b1 a b], assumption+)  
 apply (rule sym, assumption)
done

lemma (in Module) fsps_chain_boundTr2:"⋀x. ⟦R module N; free_generator R M H;
       f ∈ H → carrier N; C ⊆ fsps R M N f H;  
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; 
       x ∈ (fgs R M (⋃{a. ∃b. (a, b) ∈ C})); C ≠ {}⟧  ⟹ 
    (THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x)) ∈ 
    (carrier N) ∧ 
    (∃a1 b1. (a1, b1) ∈ C ∧ x ∈ fgs R M a1 ∧ 
    (THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x)) = 
              b1 x)"
apply (cut_tac sc_Ring, frule Ring.whole_ideal[of R])
apply (case_tac "⋃{a. ∃b. (a, b) ∈ C} = {}", simp add: empty_fgs,
       frule nonempty_ex[of C], erule exE,
       cut_tac p = xa in PairE_lemma, (erule exE)+,
       frule_tac c = xa in subsetD[of C "fsps R M N f H"], assumption+, simp)
apply (frule_tac a = xb and b = y in mem_fsps_snd_mHom[of N H f], 
       assumption+, simp add:subsetD)
apply (rename_tac a b a1 b1) 
 apply (subgoal_tac "∃!y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
                                          𝟬 ∈ (fgs R M a) ∧ y = b 𝟬)",
        subgoal_tac "(THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
         𝟬 ∈ fgs R M a ∧ y = b 𝟬)) ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
          𝟬 ∈ fgs R M a ∧ 
     (THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 𝟬 ∈ fgs R M a ∧ y = b 𝟬)) =
      b 𝟬)")  
 prefer 2
    apply (rule theI', simp, simp)
 apply (rule ex_ex1I)
   apply (cut_tac a = a1 in fgs_submodule)
   apply (frule_tac a = a1 and b = b1 in mem_fsps_fst_sub[of N H f],
          assumption+, simp add:subsetD, frule free_generator_sub[of H],
          rule subset_trans[of _ H "carrier M"], assumption+,
        frule_tac H = "fgs R M a1" in mdl_is_module,
        frule_tac M = "mdl M (fgs R M a1)" and f = b1 in 
                                   Module.mHom_0[of _ R N], assumption+,
        frule_tac H = "fgs R M a1" in submodule_inc_0,
        frule Module.module_inc_zero[of N],
        thin_tac "b1 ∈ mHom R (mdl M (fgs R M a1)) N",
        thin_tac "R module mdl M (fgs R M a1)",
        simp add:mdl_def) 
   apply (rotate_tac -3, frule sym, thin_tac "b1 𝟬 = 𝟬⇘N⇙", blast)
   apply ((erule conjE)+, (erule exE)+, (erule conjE)+)
   apply (cut_tac a = aa in fgs_submodule,
          frule_tac a = aa and b = ba in mem_fsps_fst_sub[of N H f],
          assumption+, simp add:subsetD,
          frule free_generator_sub, rule subset_trans, assumption+,
          simp add:subsetD,
          frule_tac H = "fgs R M aa" in mdl_is_module,
          frule_tac M = "mdl M (fgs R M aa)" and f = ba in 
                                   Module.mHom_0[of _ R N], assumption+,
          frule_tac H = "fgs R M aa" in submodule_inc_0,
          frule_tac c = "(aa, ba)" in subsetD[of C "fsps R M N f H"], 
          assumption+, simp,
          frule_tac a = aa and b = ba in mem_fsps_snd_mHom[of N H f],
          assumption+, simp add:mdl_def)  
   apply (cut_tac a = ab in fgs_submodule,
          frule_tac a = ab and b = bb in mem_fsps_fst_sub[of N H f],
          assumption+, simp add:subsetD,
          frule free_generator_sub, rule subset_trans[of _ H "carrier M"],
          assumption+,
          frule_tac H = "fgs R M ab" in mdl_is_module,
          frule_tac M = "mdl M (fgs R M ab)" and f = bb in 
                                   Module.mHom_0[of _ R N], assumption+) 
  apply (fold mdl_def,
         frule_tac c = "(ab, bb)" in subsetD[of C "fsps R M N f H"], 
         assumption+,
          frule_tac a = ab and b = bb in mem_fsps_snd_mHom[of N H f], 
          assumption+, simp add:mdl_def)
 (*********** case ⋃{a. ∃b. (a, b) ∈ C} = {} done **********)
 apply (subgoal_tac "∃!y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
                                          x ∈ (fgs R M a) ∧ y = b x)",
        subgoal_tac "(THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
         x ∈ fgs R M a ∧ y = b x)) ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ 
          x ∈ fgs R M a ∧ 
     (THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x)) =
      b x)")  
 prefer 2
   apply (rule theI', simp, simp)
   apply (rule ex_ex1I)
   apply (frule_tac K = "⋃{a. ∃b. (a, b) ∈ C}" and x = x in mem_fgs_l_comb)
   apply (rule subsetI, simp,
          thin_tac "∃x. (∃b. (x, b) ∈ C) ∧ x ≠ {}",
          erule exE, erule conjE, erule exE,
          frule_tac a = xb and b = b in mem_fsps_fst_sub[of N H f],
                assumption+, simp add:subsetD,
          frule free_generator_sub[of H], simp add:subsetD, assumption)
   apply (erule exE, (erule bexE)+)
   apply (frule_tac fa = fa and n = n in fsps_chain_boundTr1_1[of N H f C],
          assumption+)
   apply (frule_tac A = "⋃{a. ∃b. (a, b) ∈ C}" in nonempty_ex, 
          erule exE, simp, assumption+, erule bexE,
          cut_tac p = xa in PairE_lemma, (erule exE)+, simp)
   apply (frule_tac a = xb and b = y in mem_fsps_fst_sub[of N H f], 
               assumption+, simp add:subsetD,
          frule free_generator_sub[of H], 
          frule_tac A = xb in subset_trans[of _ H "carrier M"], assumption+)
   apply (frule_tac H = xb and s = s and n = n and f = fa in 
          l_comb_mem_linear_span[of "carrier R"], assumption+,
          rule Pi_I,
          frule_tac a = xc and A = "{j. j ≤ n}" and f = fa in 
          mem_in_image2, simp add:image_def, erule exE, blast,
          fold fgs_def) 
   apply (frule_tac a = xb and b = y in mem_fsps_snd_mHom[of N H f],
          assumption+, simp add:subsetD,
          frule_tac a = xb in fgs_submodule,
          frule_tac H = "fgs R M xb" in mdl_is_module,
          frule_tac R = R and M = "mdl M (fgs R M xb)" and N = N and
                f = y and m = x in Module.mHom_mem, assumption+,
          simp add:mdl_carrier, simp, blast)
 apply ((erule conjE)+, (erule exE)+, (erule conjE)+) 
  apply (frule_tac x = "(a, b)" in bspec, assumption,
         rotate_tac -1,
         frule_tac x = "(aa, ba)" in bspec, assumption,
         thin_tac "∀ba∈C. fst (a, b) ⊆ fst ba ∨ fst ba ⊆ fst (a, b)",
         simp)
 apply (rule_tac a = a and b = b and ?a1.0 = aa and ?b1.0 = ba and x = x in 
        fsps_chain_boundTr2_2[of N H f C], assumption+)
done

lemma (in Module) Un_C_submodule:"⟦R module N; free_generator R M H; 
     f ∈ H → carrier N; C ⊆ fsps R M N f H; C ≠ {};
     ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a⟧ ⟹ 
       submodule R M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))"
 apply (cut_tac sc_Ring, frule free_generator_sub[of H],
        frule Ring.whole_ideal)
 apply (subst fgs_def)
 apply (rule linear_span_subModule, assumption+) 
 apply (rule subsetI, simp) 
 apply (erule exE, erule conjE, erule exE,
        frule_tac c = "(xa, b)" in subsetD[of C "fsps R M N f H"], assumption+,
        frule_tac a = xa and b = b in mem_fsps_fst_sub[of N H f], assumption+,
        frule free_generator_sub, frule_tac A = xa in 
               subset_trans[of _ H "carrier M"], assumption+,
        simp add:subsetD)   
done

lemma (in Module) Un_C_fgs_sub:"⟦R module N; free_generator R M H; 
     f ∈ H → carrier N; C ⊆ fsps R M N f H; C ≠ {};
     ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a⟧ ⟹
     ⋃{a. ∃b. (a, b) ∈ C} ⊆ fgs R M (⋃{a. ∃b. (a, b) ∈ C})"
apply (simp add:fgs_def)
apply (rule l_span_cont_H)
apply (frule Un_C_submodule[of N H f C], assumption+)
apply (rule subsetI, simp, erule exE, erule conjE, erule exE)
apply (frule_tac a = xa and b = b in mem_fsps_fst_sub[of N H f], assumption+,
       simp add:subsetD,
       frule free_generator_sub[of H],
       frule_tac A = xa and B = H and C = "carrier M" in subset_trans, 
       assumption+, simp add:subsetD)
done

lemma (in Module) Chain_3_supset:"⟦R module N; free_generator R M H; 
    f ∈ H → carrier N; C ⊆ fsps R M N f H; C ≠ {};
   ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; (a1, b1) ∈ C; (a2, b2) ∈ C;
   (a3, b3) ∈ C⟧ ⟹ ∃(g, h)∈C. a1 ⊆ g ∧ a2 ⊆ g ∧ a3 ⊆ g"
proof -
  assume "(a1, b1) ∈ C"
    "(a2, b2) ∈ C"
    "(a3, b3) ∈ C"
  then have A: "a1 ∈ fst ` C"
    "a2 ∈ fst ` C"
    "a3 ∈ fst ` C"
    by (simp_all add: image_iff) force+
  assume "∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a"
  with A have "a1 ⊆ a2 ∨ a2 ⊆ a1"
    "a1 ⊆ a3 ∨ a3 ⊆ a1"
    "a2 ⊆ a3 ∨ a3 ⊆ a2"
    by auto
  with A have "∃a∈fst ` C. a1 ⊆ a ∧ a2 ⊆ a ∧ a3 ⊆ a"
    by auto
  then obtain a where "a ∈ fst ` C" and C: "a1 ⊆ a" "a2 ⊆ a" "a3 ⊆ a" by blast
  then obtain b where "(a, b) ∈ C" by auto
  with C show "∃(a, b)∈C. a1 ⊆ a ∧ a2 ⊆ a ∧ a3 ⊆ a"
    by auto
qed

lemma (in Module) fsps_chain_bound1:"⟦R module N; free_generator R M H;  
       f ∈ H → carrier N; C ⊆ fsps R M N f H;  
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a; C ≠ {}⟧  ⟹ 
      (λx∈(fgs R M (⋃{a. ∃b. (a, b) ∈ C})). (THE y. y ∈ carrier N ∧ 
                    (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x))) ∈ 
       mHom R (mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))) N"
apply (cut_tac sc_Ring, frule Ring.whole_ideal)
apply (frule Un_C_submodule[of N H f C], assumption+)
apply (frule mdl_is_module[of "fgs R M (⋃{a. ∃b. (a, b) ∈ C})"])
apply (rule Module.mHom_test[of "mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))" R N 
      "λx∈fgs R M (⋃{a. ∃b. (a, b) ∈ C}). THE y. y ∈ carrier N ∧ 
        (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x)"], assumption+)
apply (rule conjI)
 apply (rule Pi_I,
        frule submodule_subset[of "fgs R M (⋃{a. ∃b. (a, b) ∈ C})"],
        simp add:mdl_carrier, simp add:fsps_chain_boundTr2) 
apply (rule conjI)
 apply (simp add:mdl_carrier)
apply (rule conjI)
 apply (rule ballI)+
 apply (frule Module.module_is_ag[of "mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))"
         R])
 apply (frule_tac x = m and y = n in aGroup.ag_pOp_closed[of 
          "mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))"], assumption+)
 apply (frule_tac x = m in fsps_chain_boundTr2[of N H f C], assumption+,
        simp add:mdl_carrier, assumption, erule conjE, (erule exE)+, 
        (erule conjE)+,
        frule_tac x = n in fsps_chain_boundTr2[of N H f C], assumption+,
        simp add:mdl_carrier, assumption, erule conjE, (erule exE)+, 
        (erule conjE)+,
        frule_tac x = "m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n" in 
        fsps_chain_boundTr2[of N H f C], assumption+,
        simp add:mdl_carrier, assumption, erule conjE, (erule exE)+, 
        (erule conjE)+) apply (simp add:mdl_carrier)
 apply (thin_tac "(THE y.
            y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ m ∈ fgs R M a ∧ y = b m)) =
        b1 m") apply (
        thin_tac "(THE y.
            y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ n ∈ fgs R M a ∧ y = b n)) =
        b1a n") apply (
        thin_tac "(THE y.
            y ∈ carrier N ∧
            (∃a b. (a, b) ∈ C ∧
                   m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n ∈ fgs R M a ∧
                   y = b (m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n))) =
        b1b (m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n)")
 apply (thin_tac "m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n
        ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})",
        thin_tac "b1b (m ±⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ n) ∈ carrier N",
        simp add:mdl_def, fold mdl_def) 
 apply (cut_tac ?a1.0 = a1 and ?b1.0 = b1 and ?a2.0 = a1a and ?b2.0 = b1a and 
        ?a3.0 = a1b and ?b3.0 = b1b in Chain_3_supset[of N H f C], assumption+)
 apply (erule bexE)
 apply (cut_tac p = x in PairE_lemma, (erule exE)+, simp, (erule conjE)+)
 apply (frule_tac J = a1b and K = xa in fgs_mono[of H], assumption+,
        rule_tac a = xa and b = y in mem_fsps_fst_sub[of N H f], assumption+, 
        simp add:subsetD,
        frule_tac J = a1 and K = xa in fgs_mono[of H], assumption+,
        rule_tac a = xa and b = y in mem_fsps_fst_sub[of N H f], assumption+,
        simp add:subsetD, 
        frule_tac J = a1a and K = xa in fgs_mono[of H], assumption+,
        rule_tac a = xa and b = y in mem_fsps_fst_sub[of N H f], assumption+, 
        simp add:subsetD)
  apply (frule_tac c = m and A = "fgs R M a1" and B = "fgs R M xa" in subsetD,
          assumption+,
         frule_tac c = n and A = "fgs R M a1a" and B = "fgs R M xa" in subsetD,
          assumption+,
         frule_tac c = "m ± n" and A = "fgs R M a1b" and B = "fgs R M xa" in 
          subsetD, assumption+)
  apply (frule_tac a = a1 and b = b1 and aa = xa and ba = y in 
          fsps_chain_boundTr2_1[of N H f C], assumption+, simp,
         frule_tac a = a1a and b = b1a and aa = xa and ba = y in 
          fsps_chain_boundTr2_1[of N H f C], assumption+, simp,
         frule_tac a = a1b and b = b1b and aa = xa and ba = y in 
          fsps_chain_boundTr2_1[of N H f C], assumption+, simp)  
  apply (thin_tac "submodule R M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))",
         thin_tac "R module mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))",
         thin_tac "m ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})",
         thin_tac "n ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})",
         thin_tac "aGroup (mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C})))",
         thin_tac "y m ∈ carrier N",  thin_tac "(a1, b1) ∈ C",
         thin_tac "m ∈ fgs R M a1",   thin_tac "y n ∈ carrier N",
         thin_tac "(a1a, b1a) ∈ C",   thin_tac "n ∈ fgs R M a1a",
         thin_tac "(a1b, b1b) ∈ C",   thin_tac "m ± n ∈ fgs R M a1b",
         thin_tac "a1 ⊆ xa",          thin_tac "a1a ⊆ xa",
         thin_tac "a1b ⊆ xa",         thin_tac "fgs R M a1 ⊆ fgs R M xa",
         thin_tac "fgs R M a1a ⊆ fgs R M xa",
         thin_tac "b1b (m ± n) = y (m ± n)",
         thin_tac "b1 m = y m", thin_tac "b1a n = y n")
  apply (cut_tac a = xa in fgs_submodule, 
         frule_tac c = "(xa, y)" in subsetD[of C "fsps R M N f H"], 
         assumption+,
         simp add:mem_fsps_fst_sub1)
  apply (frule_tac H = "fgs R M xa" in mdl_is_module)
  apply (frule_tac a = xa and b = y in mem_fsps_snd_mHom[of N H f],
         assumption+, simp add:subsetD)
  apply (frule_tac R = R and M = "mdl M (fgs R M xa)" and N = N and f = y and 
         m = m and n = n in Module.mHom_add, assumption+,
         simp add:mdl_carrier, simp add:mdl_carrier, simp add:mdl_def)
(************** mHom_add ***********************)

apply (rule ballI)+
 apply (frule_tac a = a and m = m in Module.sc_mem[of 
          "mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))" R], assumption+)
 apply (frule_tac x = m in fsps_chain_boundTr2[of N H f C], assumption+,
        simp add:mdl_carrier, assumption, erule conjE, (erule exE)+, 
        (erule conjE)+,
        frule_tac x = "a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m" in 
        fsps_chain_boundTr2[of N H f C], assumption+,
        simp add:mdl_carrier, assumption, erule conjE, (erule exE)+, 
        (erule conjE)+) 
 apply (simp add:mdl_carrier)
 apply (thin_tac "(THE y.
            y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ m ∈ fgs R M a ∧ y = b m)) =
        b1 m",
        thin_tac "b1a (a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m) ∈ carrier N",
        thin_tac "(THE y.
            y ∈ carrier N ∧
            (∃aa b.
                (aa, b) ∈ C ∧
                a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m ∈ fgs R M aa ∧
                y = b (a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m))) =
        b1a (a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m)",
        thin_tac "a ⋅⇩s⇘mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))⇙ m
        ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})",
        thin_tac "submodule R M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))",
        thin_tac "R module mdl M (fgs R M (⋃{a. ∃b. (a, b) ∈ C}))")
  apply (simp add:mdl_def,
        thin_tac "m ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})",
        thin_tac "b1 m ∈ carrier N")
  apply (frule_tac x = "(a1, b1)" in bspec, assumption,
         rotate_tac -1,
         drule_tac x = "(a1a, b1a)" in bspec, assumption,
         simp)
  apply (erule disjE,
        frule_tac J = a1 and K = a1a in fgs_mono[of H], assumption+,
        rule_tac a = a1a and b = b1a in mem_fsps_fst_sub[of N H f], 
        assumption+, simp add:subsetD,
        frule_tac c = m and A = "fgs R M a1" and B = "fgs R M a1a" in subsetD,
        assumption+)
  apply (cut_tac a = a1a in fgs_submodule,
         frule_tac c = "(a1a, b1a)" in subsetD[of C "fsps R M N f H"],
                               assumption+, simp add:mem_fsps_fst_sub1,
         frule_tac H = "fgs R M a1a" in mdl_is_module,
         frule_tac a = a1a and b = b1a in mem_fsps_snd_mHom[of N H f],
          assumption+, simp add:subsetD)
  apply (frule_tac R = R and M = "mdl M (fgs R M a1a)" and N = N and m = m 
         and f = b1a and a = a in Module.mHom_lin, assumption+,
         simp add:mdl_carrier, assumption+, simp add:mdl_def,
                fold mdl_def)
  apply (frule_tac a = a1 and b = b1 and ?a1.0 = a1a and ?b1.0 = b1a and x = m
         in fsps_chain_boundTr2_2[of N H f C], assumption+, simp)

  apply (frule_tac J = a1a and K = a1 in fgs_mono[of H], assumption+,
        rule_tac a = a1 and b = b1 in mem_fsps_fst_sub[of N H f], 
        assumption+, simp add:subsetD,
        frule_tac c = "a ⋅⇩s m" and A = "fgs R M a1a" and B = "fgs R M a1" in 
        subsetD, assumption+)
  apply (frule_tac a = a1a and b = b1a and ?a1.0 = a1 and ?b1.0 = b1 and 
         x = "a ⋅⇩s m" in fsps_chain_boundTr2_2[of N H f C], assumption+, simp)
  apply (cut_tac a = a1 in fgs_submodule,
         frule_tac c = "(a1, b1)" in subsetD[of C "fsps R M N f H"],
           assumption+, simp add:mem_fsps_fst_sub1,
         frule_tac H = "fgs R M a1" in mdl_is_module,
         frule_tac a = a1 and b = b1 in mem_fsps_snd_mHom[of N H f],
          assumption+, simp add:subsetD)
  apply (frule_tac R = R and M = "mdl M (fgs R M a1)" and N = N and m = m 
         and f = b1 and a = a in Module.mHom_lin, assumption+,
         simp add:mdl_carrier, assumption+, simp add:mdl_def) 
done

lemma (in Module) fsps_chain_bound2:"⟦R module N; free_generator R M H;  
       f ∈ H → carrier N; C ⊆ fsps R M N f H; C ≠ {}; 
       ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a⟧  ⟹ 
   ∀y∈(⋃{a. ∃b. (a, b) ∈ C}). (λx∈(fgs R M (⋃{a. ∃b. (a, b) ∈ C})). 
   (THE y. y ∈ carrier N ∧ (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x))) y =
    f y"
apply (rule ballI)
 apply (subgoal_tac "y ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})")
 prefer 2 
 apply simp
 apply (erule exE, erule conjE, erule exE)
 apply (frule  Un_C_fgs_sub[of N H f C], assumption+)
 apply (rule_tac c = y in subsetD[of "⋃{a. ∃b. (a, b) ∈ C}"
                   "fgs R M (⋃{a. ∃b. (a, b) ∈ C})"], assumption+)
 apply (simp, blast)

 apply simp
 apply (frule_tac x = y in fsps_chain_boundTr2[of N H f C], assumption+)
 apply (erule conjE, (erule exE)+, erule conjE, erule exE, (erule conjE)+)
 apply (simp,
       thin_tac "(THE ya. ya ∈ carrier N ∧
            (∃a b. (a, b) ∈ C ∧ y ∈ fgs R M a ∧ ya = b y)) = b1 y")
 apply (frule_tac c = "(x, b)" in subsetD[of C "fsps R M N f H"],
        assumption+,
        simp add:fsps_def fsp_def, (erule conjE)+,
        thin_tac "∀z∈x. f z = b z")
 apply (frule_tac x = y and a = x and b = b and ?a1.0 = a1 and ?b1.0 = b1 in
        fsps_chain_boundTr2_2[of N H f C], assumption+,
        simp add:fsps_def fsp_def, assumption+, subst fgs_def,
        rule_tac c = y and A = x and B = "linear_span R M (carrier R) x"
        in subsetD,
        rule l_span_cont_H,
        frule free_generator_sub[of H], rule subset_trans[of _ H "carrier M"],
         assumption+, simp)
done

lemma (in Module) od_fm_fun_Chain:"⟦R module N; free_generator R M H; 
      f ∈ H → carrier N; Algebra2.Chain (od_fm_fun R M N f H) C; C ≠ {}⟧ ⟹ 
      ∀a∈C. ∀b∈C. fst a ⊆ fst b ∨ fst b ⊆ fst a"
apply (frule Order_od_fm_fun[of N H f], assumption+)
 apply (rule ballI)+
 apply (simp add:Algebra2.Chain_def, erule conjE, simp add:Torder_def, erule conjE,
        simp add:Torder_axioms_def)
 apply (simp add:Order.Iod_carrier)
  apply (auto simp add: Iod_def od_fm_fun_def ole_def)
  apply blast
done

lemma (in Module) od_fm_fun_inPr0:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; Algebra2.Chain (od_fm_fun R M N f H) C; C ≠ {};
       ∃b. (y, b) ∈ C; z ∈ y⟧  ⟹ z ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C})"
apply (frule Un_C_fgs_sub[of N H f C], assumption+)
 apply (simp add:Algebra2.Chain_def od_fm_fun_def, assumption) 
 apply (simp add:od_fm_fun_Chain)
 apply (rule_tac subsetD[of "⋃{a. ∃b. (a, b) ∈ C}" 
                     "fgs R M (⋃{a. ∃b. (a, b) ∈ C})" z], assumption+)
 apply (simp, blast)
done

lemma (in Module) od_fm_fun_indPr1:" ⟦R module N; free_generator R M H; 
      f ∈ H → carrier N; Algebra2.Chain (od_fm_fun R M N f H) C; C ≠ {}⟧ ⟹
      (⋃{a. ∃b. (a, b) ∈ C}, 
         λx ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C}). THE y. y ∈ carrier N ∧
         (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x)) ∈ fsps R M N f H"
apply (simp add:fsps_def fsp_def, rule conjI)
 apply (rule fsps_chain_bound1[of N H f C], assumption+)
 apply (simp add:od_fm_fun_def Algebra2.Chain_def)
 apply (simp add:od_fm_fun_Chain, assumption)
apply (rule conjI)
 apply (rule allI, rule impI)
 apply (rule ballI)
 apply (simp add:od_fm_fun_inPr0[of N H f C])
 apply (frule fsps_chain_bound2[of N H f C], assumption+,
        simp add:Algebra2.Chain_def od_fm_fun_def, assumption)
 apply (simp add:od_fm_fun_Chain)
 apply (drule_tac x = z in bspec)
  apply (simp, blast) 
 apply (simp add:od_fm_fun_inPr0)
apply (rule subsetI, simp, erule exE, erule conjE, erule exE)
 apply (frule Order_od_fm_fun[of N H f], assumption+,
        frule Order.Chain_sub[of "od_fm_fun R M N f H" C], assumption,
        thin_tac "Algebra2.Chain (od_fm_fun R M N f H) C",
        thin_tac "Order (od_fm_fun R M N f H)")
 apply (simp add:od_fm_fun_def)
 apply (frule_tac a = xa and b = b in mem_fsps_fst_sub[of N H f], assumption+,
        simp add:subsetD, simp add:subsetD)
done

lemma (in Module) od_fm_fun_indPr2:" ⟦R module N; free_generator R M H; 
      f ∈ H → carrier N; Algebra2.Chain (od_fm_fun R M N f H) C; C ≠ {}⟧ ⟹
     ub⇘od_fm_fun R M N f H⇙ C (⋃{a. ∃b. (a, b) ∈ C}, 
         λx ∈ fgs R M (⋃{a. ∃b. (a, b) ∈ C}). THE y. y ∈ carrier N ∧
                          (∃a b. (a, b) ∈ C ∧ x ∈ fgs R M a ∧ y = b x))"
apply (frule Order_od_fm_fun[of N H f], assumption+,
       simp add:upper_bound_def)

 apply (simp add:od_fm_fun_def, fold od_fm_fun_def,
        frule od_fm_fun_indPr1[of N H f C], assumption+, simp)

 apply (rule ballI,
        subst od_fm_fun_def, subst ole_def, simp)
 apply (rule conjI)
 apply (frule Order.Chain_sub[of "od_fm_fun R M N f H" C], assumption,
        simp add:od_fm_fun_carrier, simp add:subsetD)
 apply (unfold split_paired_all,
        rule subsetI, simp, blast)
done
  
lemma (in Module) od_fm_fun_inductive:"⟦R module N; free_generator R M H; 
      f ∈ H → carrier N⟧ ⟹ inductive_set (od_fm_fun R M N f H)"
apply (frule Order_od_fm_fun[of N H f], assumption+)
apply (simp add:inductive_set_def)
apply (rule allI, rule impI)
apply (case_tac "C ≠ {}")
 apply (frule_tac C = C in od_fm_fun_indPr2[of N H f], assumption+)
 apply blast
apply simp
 apply (simp add:upper_bound_def)
 apply (subst od_fm_fun_def, simp)
 apply (frule empty_fsp[of N H f], assumption+, blast)
done

lemma (in Module) sSum_eq:"⟦R module N; free_generator R M H; H1 ⊆ H; 
      h ∈ H - H1⟧ ⟹  (fgs R M H1) ∓ (fgs R M {h}) = fgs R M (H1 ∪ {h})"
apply (cut_tac sc_Ring, frule Ring.whole_ideal)
apply (frule free_generator_sub)
 apply (frule subset_trans[of H1 H "carrier M"], assumption+,
        frule fgs_sub_carrier[of H1])
 apply (cut_tac subset_trans[of "{h}" "H - H1" "carrier M"],
         frule fgs_sub_carrier[of "{h}"])
 apply (simp add:set_sum[of "fgs R M H1" "fgs R M {h}"])
 apply (rule equalityI)
  apply (rule subsetI, simp, (erule bexE)+)
  apply (case_tac "H1 = {}", simp add:empty_fgs) 
  apply (frule_tac c = k in subsetD[of "fgs R M {h}" "carrier M"], assumption+)
  apply (simp add:ag_l_zero)
  apply (cut_tac fgs_mono[of H H1 "insert h H1"],
         frule_tac c = ha in subsetD[of "fgs R M H1" "fgs R M (insert h H1)"],
          assumption+,
         cut_tac fgs_mono[of H "{h}" "insert h H1"],
         frule_tac c = k in subsetD[of "fgs R M {h}" "fgs R M (insert h H1)"],
          assumption+)
  apply (simp add:fgs_def,
         cut_tac sc_Ring, frule Ring.whole_ideal,
         rule linear_span_pOp_closed, assumption+,
         rule subsetI, simp, erule disjE, simp, simp add:subsetD, assumption+,
         rule subsetI, simp, rule subsetI, simp, erule disjE, simp, 
         simp add:subsetD, assumption+, rule subsetI, simp,
         rule subsetI, simp, erule disjE, simp, simp add:subsetD)
 apply (rule subsetI)

 apply (cut_tac x = x in mem_fgs_l_comb[of "insert h H1"],
        simp,
        rule subsetI, simp, erule disjE, simp, simp add:subsetD, assumption+)
 apply (erule exE, (erule bexE)+)
 apply (case_tac "f ` {j. j ≤ n} ⊆ H1")
 apply (frule_tac s = s and n = n and f = f in 
           l_comb_mem_linear_span[of "carrier R" H1], assumption+)
  apply (rule Pi_I)
  apply (frule_tac f = f and A = "{j. j ≤ n}" and B = "insert h H1" and 
         a = xa in mem_in_image, assumption+, simp add:subsetD)
  apply (fold fgs_def)
  apply (frule fgs_sub_carrier[of H1]) 
  apply (frule_tac c = "l_comb R M n s f" in subsetD[of "fgs R M H1" 
             "carrier M"], assumption+)
  apply (frule_tac t = "l_comb R M n s f" in ag_r_zero[THEN sym], simp)
  apply (cut_tac fgs_submodule[of "{h}"],
        frule submodule_inc_0[of "fgs R M {h}"], blast,
        rule subsetI, simp)
 
  apply (frule_tac f = f and A = "{j. j ≤ n}" and B = "insert h H1" in
          image_sub0)
  apply (frule_tac Y = "f ` {j. j ≤ n}" and a = h and X = H1 in sub_inserted1,
         assumption+, erule conjE,
         thin_tac "¬ f ` {j. j ≤ n} ⊆ H1", 
         thin_tac "f ` {j. j ≤ n} ⊆ insert h H1", erule conjE) 
  apply (cut_tac H = "insert h H1" and f = f and n = n and s = s in   
         unique_expression2)
         apply (rule subsetI, simp, erule disjE, simp, simp add:subsetD)
         apply assumption+
  apply ((erule exE)+, (erule conjE)+, simp)
  apply (simp add:bij_to_def, erule conjE,
         simp add:surj_to_def)
  apply (rotate_tac -2, frule sym, thin_tac "g ` {j. j ≤ m} = f ` {j. j ≤ n}",
         simp, thin_tac "f ` {j. j ≤ n} = g ` {j. j ≤ m}", simp add:image_def,
         erule exE,
         thin_tac "f ∈ {j. j ≤ n} → insert h H1",
         thin_tac "s ∈ {j. j ≤ n} → carrier R",
         thin_tac "l_comb R M n s f = l_comb R M m t g", erule conjE)

  apply (case_tac "m = 0", simp,
         frule_tac a = H1 in fgs_submodule,
         frule submodule_inc_0[of "fgs R M H1"],
         cut_tac a = "insert (g 0) H1" in fgs_submodule,
         rule subsetI, simp, erule disjE, simp, simp add:subsetD,
         frule_tac H = "fgs R M (insert (g 0) H1)" in submodule_subset,
         frule_tac c = "l_comb R M 0 t g" and A = "fgs R M (insert (g 0) H1)" 
                 and B = "carrier M" in subsetD, assumption+,
         frule_tac t = "l_comb R M 0 t g" in ag_l_zero[THEN sym],
         subgoal_tac "l_comb R M 0 t g ∈ fgs R M {g 0}", blast)
     apply (subst fgs_def,
         cut_tac s = t and n = m and f = g in 
                l_comb_mem_linear_span[of "carrier R" "{h}"], assumption+,
         rule subsetI, simp, simp, simp, 
         simp, simp)
   (** case n ≠ 0 **)
  apply (cut_tac f = g and n = "m - Suc 0" and s = t and l = xa in
          unique_expression3[of "insert h H1"],
         rule subsetI, simp, erule disjE, simp, simp add:subsetD)
         apply simp+ 
         apply (rule contrapos_pp, simp+, simp add:image_def)
         apply (erule bexE, simp add:inj_on_def)
         apply (drule_tac a = xa in forall_spec, simp)  
         apply (drule_tac a = xb in forall_spec,
                erule conjE, assumption, simp)
   apply ((erule exE)+, (erule conjE)+, simp)
         apply (thin_tac "g ∈ {j. j ≤ m} → insert (g xa) H1",
                thin_tac "t ∈ {j. j ≤ m} → carrier R",
                thin_tac "l_comb R M m t g = l_comb R M ma ta ga",
                thin_tac "inj_on g {j. j ≤ m}",
                thin_tac "g xa ∈ carrier M",
                thin_tac "fgs R M {g xa} ⊆ carrier M") 
         apply (rotate_tac 13, frule sym, thin_tac "h = g xa", simp) 
         apply (thin_tac "g xa = h", thin_tac "0 < m", thin_tac "xa ≤ m",
                thin_tac "ta ma = t xa", simp)
         apply (rename_tac x g m t)
   apply (case_tac "m = 0", simp,
         frule_tac a = H1 in fgs_submodule,
         frule submodule_inc_0[of "fgs R M H1"],
         cut_tac a = "insert h H1" in fgs_submodule,
         rule subsetI, simp, erule disjE, simp, simp add:subsetD,
         frule subset_trans[of H1 H "carrier M"], assumption+, 
         simp add:subsetD,
         frule_tac H = "fgs R M (insert h H1)" in submodule_subset,
         frule_tac c = "l_comb R M 0 t g" and A = "fgs R M (insert h H1)" 
                 and B = "carrier M" in subsetD, assumption+,
         frule_tac t = "l_comb R M 0 t g" in ag_l_zero[THEN sym],
         subgoal_tac "l_comb R M 0 t g ∈ fgs R M {h}", blast)
     apply (subst fgs_def,
         cut_tac s = t and n = 0 and f = g in 
                l_comb_mem_linear_span[of "carrier R" "{h}"],
         assumption, rule subsetI, simp, simp add:subsetD,
         simp, simp, assumption)
  apply (subgoal_tac "l_comb R M m t g = l_comb R M (Suc (m - Suc 0)) t g",
         simp del:Suc_pred,
         frule insert_sub[of H1 H h], assumption+,
         frule subset_trans[of "insert h H1" H "carrier M"], assumption+,
         subst l_comb_Suc[of "insert h H1" "carrier R"], assumption+,
         (subst Suc_pred, assumption,
          thin_tac "l_comb R M m t g = l_comb R M (Suc (m - Suc 0)) t g",
                simp)+)
  apply (subgoal_tac "l_comb R M (m - Suc 0) t g ∈ fgs R M H1",
         subgoal_tac "t m ⋅⇩s h ∈ fgs R M {h}", blast,
         subst fgs_def,
         rule_tac h = h and a = "t m" in 
                 sc_linear_span[of "carrier R" "{h}"], assumption+,
         rule subsetI, simp, simp add:Pi_def, simp,
         cut_tac a = "{h}" in fgs_submodule, rule subsetI, simp,
         cut_tac s = t and n = "m - Suc 0" and f = g in 
                   l_comb_mem_linear_span[of "carrier R" H1], assumption,
         simp add:subset_trans[of H1 H "carrier M"],
         rule func_pre, simp,
         rule Pi_I, simp,
         frule_tac f = g and A = "{k. k ≤ m}" and B = "insert h H1"
                and x = xa in funcset_mem, simp, simp, simp add:inj_on_def) 
  apply (erule disjE)
  apply (drule_tac a = m in forall_spec, simp,
         drule_tac a = xa in forall_spec, simp, simp, simp)
  apply (cut_tac n1 = xa and m1 = "xa - Suc 0" in Suc_le_mono[THEN sym],
              simp, simp add:fgs_def, simp)
  apply (rule subsetI, simp)
  apply (rule subsetI, simp add:subsetD)
done

definition
  monofun :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, 
            ('b, 'r, 'm2) Module_scheme, 'a ⇒ 'b, 'a set, 'a] ⇒ ('a ⇒ 'b)" where
  "monofun R M N f H h = (λx∈fgs R M {h}. 
          (THE y. (∃r∈carrier R. x = r ⋅⇩s⇘M⇙ h ∧  y = r ⋅⇩s⇘N⇙ (f h))))"  

lemma (in Module) fgs_single_span:"⟦h ∈ carrier M; x ∈ (fgs R M {h})⟧ ⟹ 
              ∃a∈carrier R. x = a ⋅⇩s h" 
apply (simp add:fgs_def linear_span_def)
apply (erule exE, (erule bexE)+)
 apply (cut_tac sc_Ring, frule Ring.whole_ideal)
 apply (frule_tac A = "carrier R" and z = h and h = f and n = n and t = s in 
        single_span, assumption+)
 apply (erule bexE, simp add:l_comb_def del: Pi_split_insert_domain)
apply (frule_tac f = sa and A = "{0}" and B = "carrier R" and 
                 x = 0 in funcset_mem,  simp, blast)
done

lemma (in Module) monofun_mHomTr:"⟦h ∈ H; free_generator R M H; 
      a ∈ carrier R; r ∈ carrier R; a ⋅⇩s h = r ⋅⇩s h⟧ ⟹ a = r"
apply (cut_tac sc_Ring, frule free_generator_sub,
       frule subsetD[of H "carrier M" h], assumption+)
apply (frule_tac a = a and m = h in sc_mem, assumption+,
       frule_tac a = r and m = h in sc_mem, assumption+)
apply (frule ag_eq_diffzero[of "a ⋅⇩s h" "r ⋅⇩s h"], assumption+,
       simp only:sc_minus_am1, thin_tac "(a ⋅⇩s h = r ⋅⇩s h) = (𝟬 = 𝟬)")
apply (frule Ring.ring_is_ag[of R],
       frule aGroup.ag_mOp_closed[of R r], assumption+)
       apply (simp add:sc_l_distr[THEN sym])
       apply (frule free_gen_coeff_zero[of H h "a ±⇘R⇙ -⇩a⇘R⇙ r"], assumption+)
       apply (rule aGroup.ag_pOp_closed, assumption+)
apply (simp add:aGroup.ag_eq_diffzero)
done

lemma (in Module) monofun_mhomTr1:"⟦R module N; h ∈ H; free_generator R M H;
        f ∈ H → carrier N; a ∈ carrier R⟧  ⟹ 
                monofun R M N f H h (a ⋅⇩s h) = a ⋅⇩s⇘N⇙ (f h)"
apply (frule free_generator_sub)
apply (simp add:monofun_def) 
 apply (cut_tac a = "{h}" and x = h in elem_fgs, rule subsetI, 
        simp add:subsetD, simp,
        cut_tac fgs_submodule[of "{h}"])
 apply (frule submodule_sc_closed[of "fgs R M {h}" a h], assumption+,
        simp)
 apply (subgoal_tac "∃!y. ∃r∈carrier R. a ⋅⇩s h = r ⋅⇩s h ∧ y = r ⋅⇩s⇘N⇙ f h",
        subgoal_tac "∃r∈carrier R. a ⋅⇩s h =  r ⋅⇩s h ∧
         (THE y. ∃s∈carrier R.  a ⋅⇩s h =  s ⋅⇩s h ∧ y =  s ⋅⇩s⇘N⇙ (f h)) = 
            r ⋅⇩s⇘N⇙ (f h)")
 prefer 2 apply (rule theI', simp) 
 apply (thin_tac "∃!y. ∃r∈carrier R. a ⋅⇩s h = r ⋅⇩s h ∧ y = r ⋅⇩s⇘N⇙ f h")
 apply (erule bexE, erule conjE, simp, 
        thin_tac "(THE y. ∃s∈carrier R. r ⋅⇩s h = s ⋅⇩s h ∧ y = s ⋅⇩s⇘N⇙ f h) = r ⋅⇩s⇘N⇙ f h")
 apply (frule_tac r = r in monofun_mHomTr[of h H a], assumption+, simp)
 
 apply (rule ex_ex1I)
 apply blast
 apply ((erule bexE)+, (erule conjE)+)
 apply (frule_tac r = r in monofun_mHomTr[of h H a], assumption+,
        frule_tac r = ra in monofun_mHomTr[of h H a], assumption+)
 apply (thin_tac "a ⋅⇩s h = r ⋅⇩s h", thin_tac "a ⋅⇩s h = ra ⋅⇩s h",
        rotate_tac -2, frule sym, thin_tac "a = r", frule sym, 
        thin_tac "a = ra", simp)

 apply (rule subsetI, simp add:subsetD)
done

lemma (in Module) monofun_mem:"⟦R module N; h ∈ H; free_generator R M H; 
       x ∈ fgs R M {h}; f ∈ H → carrier N⟧  ⟹  
       monofun R M N f H h x ∈ carrier N"
apply (frule free_generator_sub,
       frule subsetD[of H "carrier M" h], assumption+,
       frule fgs_single_span[of h x], assumption+)
apply (erule bexE, simp add:monofun_mhomTr1,
       frule funcset_mem[of f H "carrier N" h], assumption)
apply (simp add:Module.sc_mem[of N R _ "f h"])
done

lemma (in Module) monofun_eq_f:"⟦R module N; h ∈ H; free_generator R M H; 
       f ∈ H → carrier N⟧  ⟹  monofun R M N f H h h = f h"
apply (cut_tac sc_Ring)
apply (frule_tac N = N and h = h and f = f and a = "1⇩r⇘R⇙" in  monofun_mhomTr1,
        assumption+)
 apply (simp add:Ring.ring_one)
 apply (frule free_generator_sub, frule subsetD[of H "carrier M" h],
                           assumption+,
        frule funcset_mem[of f H "carrier N" h], assumption)
 apply (simp add:sprod_one, simp add:Module.sprod_one)
done

lemma (in Module) sSum_unique:"⟦R module N; free_generator R M H; H1 ⊆ H; 
       h ∈ H - H1; x1 ∈(fgs R M H1); x2 ∈ (fgs R M H1); 
       y1 ∈ (fgs R M {h}); y2 ∈ (fgs R M {h}); x1 ± y1 = x2 ± y2⟧ ⟹
       x1 = x2 ∧ y1 = y2"
apply (cut_tac sc_Ring, frule Ring.whole_ideal [of "R"],
       frule free_generator_sub)
 apply (frule_tac subset_trans[of H1 H "carrier M"], assumption+)
 apply (frule subsetD[of H "carrier M" h], simp)
 apply (frule_tac fgs_single_span[of h y1], assumption+,
        frule_tac fgs_single_span[of h y2], assumption+)
 apply (erule bexE, erule bexE)
 apply (frule_tac  a = a and m = h in sc_mem, assumption+,
        frule_tac  a = aa and m = h in sc_mem, assumption+)
 apply (frule subset_trans[of H1 H "carrier M"], assumption+)
 apply (frule_tac A = "carrier R" and H = H1 in lin_span_sub_carrier, 
                      assumption+) 
 apply (fold fgs_def)
 apply (frule subsetD[of "fgs R M H1" "carrier M" x1], assumption+,
        frule subsetD[of "fgs R M H1" "carrier M" x2], assumption+)
 apply simp
 apply (frule ag_mOp_closed[of x2])
 apply (frule_tac z = "a ⋅⇩s h" in ag_pOp_assoc[of "-⇩a x2" "x1"], assumption+,
        simp only:ag_pOp_assoc[THEN sym], simp add:ag_l_inv1,
        simp add:ag_l_zero,
        frule ag_pOp_closed[of "-⇩a x2" x1], assumption+,
        frule_tac x = "a ⋅⇩s h" in ag_mOp_closed)
 apply (frule_tac y = "a ⋅⇩s h" and z = "-⇩a (a ⋅⇩s h)" in 
                    ag_pOp_assoc[of "-⇩a x2 ± x1"], assumption+,
        simp add:ag_r_inv1 ag_r_zero, thin_tac "-⇩a x2 ± x1 ± a ⋅⇩s h = aa ⋅⇩s h")
 apply (frule fgs_submodule[of H1])
 apply (frule submodule_mOp_closed[of "fgs R M H1" x2], assumption,
        frule submodule_pOp_closed[of "fgs R M H1" "-⇩a x2" "x1"], assumption+)
 apply (case_tac "H1 = {}", simp add:empty_fgs)
 apply (simp add:ag_eq_diffzero[THEN sym])
 apply (frule mem_fgs_l_comb[of H1 "-⇩a x2 ± x1"], assumption+,
        erule exE, (erule bexE)+)
 apply (case_tac "-⇩a⇘M⇙ x2 ±⇘M⇙ x1 = 𝟬⇘M⇙", simp, rotate_tac -2, frule sym,
        thin_tac "𝟬 = l_comb R M n s f", simp,
        simp add:ag_pOp_commute[of "-⇩a x2" " x1"])
 apply (simp add:ag_eq_diffzero[of x1 x2])
 apply (simp add:ag_eq_diffzero[THEN sym])
 apply simp
 apply (frule_tac f = f and n = n and s = s in unique_expression2[of H1],
        assumption+, (erule exE)+, (erule conjE)+, simp,
        simp add:bij_to_def, erule conjE,
        thin_tac "f ∈ {j. j ≤ n} → H1",
        thin_tac "s ∈ {j. j ≤ n} → carrier R",
        thin_tac "surj_to g {j. j ≤ m} (f ` {j. j ≤ n})",
        thin_tac "l_comb R M n s f = l_comb R M m t g", simp)
 apply (frule_tac f = g and A = "{j. j ≤ m}" and B = H1 and ?B1.0 = H in
                  extend_fun, assumption+)
 apply (frule_tac f = g and n = m and s = t in unique_expression4[of H],
        simp, (erule exE)+, (erule conjE)+, erule exE, (erule conjE)+)
 apply (frule_tac f = g and A = "{j. j ≤ m}" and B = H1 in image_sub0,
        frule_tac A = "ga ` {k. k ≤ ma}" and B = "g ` {j. j ≤ m}" and 
        C = H1 in subset_trans, assumption+, simp,
        thin_tac "g ∈ {j. j ≤ m} → H1",
        thin_tac "t ∈ {j. j ≤ m} → carrier R",
        thin_tac "ga ` {k. k ≤ ma} ⊆ g ` {k. k ≤ m}",
        thin_tac "l_comb R M m t g = l_comb R M ma ta ga",
        thin_tac "g ` {j. j ≤ m} ⊆ H1",
        thin_tac "inj_on g {j. j ≤ m}",
        thin_tac "g ∈ {j. j ≤ m} → H", simp) 
  apply (rename_tac a aa m g t)
  apply (simp add:sc_minus_am1,
         cut_tac sc_Ring, frule Ring.ring_is_ag,
         frule_tac x = a in aGroup.ag_mOp_closed[of R], assumption)
  apply (simp add:sc_l_distr[THEN sym]) 
  apply (case_tac "aa ±⇘R⇙ -⇩a⇘R⇙ a = 𝟬⇘R⇙", simp add:sc_0_m,
         frule_tac x = aa and y = "-⇩a⇘R⇙ a" in aGroup.ag_pOp_closed, assumption+)
  apply (subgoal_tac "(λx∈{0::nat}. (aa ±⇘R⇙ -⇩a⇘R⇙ a)) ∈
                               {j. j ≤ (0::nat)} → carrier R",
         subgoal_tac "(λx∈{0::nat}. h) ∈
                               {j. j ≤ (0::nat)} → H")
  apply (frule_tac f = "λx∈{0::nat}. h" and n = 0 and 
         s = "λx∈{0::nat}. (aa ±⇘R⇙ -⇩a⇘R⇙ a)" and g = g and m = m and t = t in 
         unique_expression5[of H])
  apply (simp)
  apply (simp add:inj_on_def)
  apply (simp, assumption+)
  apply (simp add:l_comb_def[of _ _ 0], rule ballI, simp)
  apply simp
  apply (frule_tac A = "(λx∈{0}. h) ` {j. j ≤ 0}" and B = "g ` {j. j ≤ m}" 
         and C = H1 in subset_trans, assumption+,
         thin_tac "(λx∈{0}. h) ∈ {j. j ≤ 0} → H",
         thin_tac "(λx∈{0}. aa ±⇘R⇙ -⇩a⇘R⇙ a) ∈ {j. j ≤ 0} → carrier R",
         thin_tac "(λx∈{0}. h) ` {j. j ≤ 0} ⊆ g ` {j. j ≤ m}",
         thin_tac "g ` {k. k ≤ m} ⊆ H1")
  apply (simp, simp, simp)
done

lemma (in Module) ex_extensionTr:"⟦R module N; free_generator R M H;  
       f ∈ H → carrier N; H1 ⊆ H; h ∈ H; h ∉ H1; 
       g ∈ mHom R (mdl M (fgs R M H1)) N; 
       x ∈ fgs R M H1 ∓ (fgs R M {h})⟧ ⟹ 
     ∃k1∈ fgs R M H1. ∃k2∈fgs R M {h}. x = k1 ± k2 ∧ 
 (THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}. x = h1 ± h2 ∧ y = g h1 ±⇘N⇙ 
         (monofun R M N f H h h2)) = g k1  ±⇘N⇙ (monofun R M N f H h k2)"
apply (frule free_generator_sub)
apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp,
       simp)
apply (subgoal_tac "∃!y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}. x = h1 ± h2 ∧ 
                          y = g h1 ±⇘N⇙ (monofun R M N f H h h2)",
       subgoal_tac "∃h1∈fgs R M H1. ∃h2∈fgs R M {h}. x = h1 ± h2 ∧ 
  (THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}. x =  h1 ± h2 ∧ 
    y = g h1 ±⇘N⇙ (monofun R M N f H h h2)) = g h1 ±⇘N⇙ (monofun R M N f H h h2)")
prefer 2 apply (rule theI') apply simp
 apply (thin_tac " ∃!y. ∃h1∈fgs R M H1.
        ∃h2∈fgs R M {h}. x = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2")
 apply blast
apply (rule ex_ex1I)
 apply (thin_tac "fgs R M (insert h H1) = fgs R M H1 ∓ (fgs R M {h})")
 apply (cut_tac fgs_sub_carrier[of H1], cut_tac fgs_sub_carrier[of "{h}"])
 apply (simp add:set_sum)
 apply (erule bexE)+
 apply (frule subsetD[of H "carrier M" h], assumption+) 
 apply (frule_tac x = k in monofun_mem[of N h H _ f], assumption+)
apply blast
 apply (rule subsetI, simp, simp add:subsetD,
        rule subset_trans[of H1 H "carrier M"], assumption+)
 apply ((erule bexE)+, (erule conjE)+, simp)
 apply (frule_tac ?x1.0 = h1a and ?x2.0 = h1 and ?y1.0 = h2a and ?y2.0 = h2 
        in sSum_unique[of N H H1 h], assumption+, simp, assumption+)
 apply ((erule conjE)+, simp)
done

lemma (in Module) monofun_add:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; h ∈ H; x ∈ fgs R M {h}; y ∈ fgs R M {h}⟧ ⟹ 
       monofun R M N f H h (x ± y) = 
                   monofun R M N f H h x ±⇘N⇙ (monofun R M N f H h y)"
apply (frule free_generator_sub,
       cut_tac sc_Ring, frule Ring.ring_is_ag,
       frule subsetD[of H "carrier M" h], assumption+,
       frule fgs_single_span[of h x], assumption+,
       frule fgs_single_span[of h y], assumption+, (erule bexE)+, simp,
       simp add:sc_l_distr[THEN sym])
apply (frule_tac x = a and y = aa in aGroup.ag_pOp_closed[of R], assumption+)
apply (simp add:monofun_mhomTr1,
       frule funcset_mem[of f H "carrier N" h], assumption+)
apply (simp add:Module.sc_l_distr)
done

lemma (in Module) monofun_sprod:"⟦R module N; free_generator R M H; 
      f ∈ H → carrier N; h ∈ H; x ∈ fgs R M {h}; a ∈ carrier R⟧ ⟹ 
      monofun R M N f H h ( a ⋅⇩s x) = a ⋅⇩s⇘N⇙ (monofun R M N f H h x)"
apply (frule free_generator_sub,
       cut_tac sc_Ring,
       frule subsetD[of H "carrier M" h], assumption+,
       frule fgs_single_span[of h x], assumption+,
       erule bexE, simp add:sc_assoc[THEN sym])
apply (frule_tac x = a and y = aa in Ring.ring_tOp_closed, assumption+)
apply (simp add:monofun_mhomTr1,
       frule funcset_mem[of f H "carrier N" h], assumption+)
apply (simp add:Module.sc_assoc)
done

lemma (in Module) monofun_0:"⟦R module N; free_generator R M H; 
      f ∈ H → carrier N; h ∈ H⟧ ⟹  monofun R M N f H h  𝟬  = 𝟬⇘N⇙"
apply (cut_tac fgs_submodule[of "{h}"],
       frule submodule_inc_0[of "fgs R M {h}"])
apply (cut_tac sc_Ring, frule Ring.ring_zero,
       frule monofun_sprod[of N H f h 𝟬 "𝟬⇘R⇙"], assumption+,
       cut_tac ag_inc_zero)
apply (simp add:sc_0_m,
       frule monofun_mem[of N h H 𝟬 f], assumption+,
       simp add:Module.sc_0_m)
apply (frule free_generator_sub, rule subsetI, simp add:subsetD)
done

lemma (in Module) ex_extension:"⟦R module N; free_generator R M H; 
       f ∈ H → carrier N; H1 ⊆ H; h ∈ H - H1; (H1, g) ∈ fsps R M N f H⟧ ⟹
       ∃k. ((H1 ∪ {h}), k) ∈ fsps R M N f H"
apply (frule free_generator_sub,
       cut_tac sc_Ring,
       frule subset_trans[of H1 H "carrier M"], assumption+,
       frule subsetD[of H "carrier M" h], simp+,
       frule singleton_sub[of h "carrier M"])
apply (frule fgs_submodule[of "{h}"],
       frule fgs_submodule[of H1],
       frule submodule_subset[of "fgs R M {h}"],
       frule submodule_subset[of "fgs R M H1"],
       frule insert_sub[of H1 "carrier M" h], assumption,
       frule fgs_submodule[of "insert h H1"])
apply (simp add:fsps_def fsp_def)
 apply (erule conjE)+
 apply (subgoal_tac "(λx ∈ (fgs R M (H1 ∪ {h})). 
        (THE y. (∃h1∈(fgs R M H1). ∃h2∈(fgs R M {h}). x = h1 ± h2 ∧ 
                 y = g h1 ±⇘N⇙ (monofun R M N f H h h2)))) ∈ 
        mHom R (mdl M (fgs R M (insert h H1))) N ∧ 
  f h = (λx ∈ (fgs R M (H1 ∪ {h})). 
        (THE y. (∃h1∈(fgs R M H1). ∃h2∈(fgs R M {h}). x = h1 ± h2 ∧ 
            y = g h1 ±⇘N⇙ (monofun R M N f H h h2)))) h ∧ 
        (∀z∈H1. g z = (λx ∈ (fgs R M (H1 ∪ {h})). 
        (THE y. (∃h1∈(fgs R M H1). ∃h2∈(fgs R M {h}). x = h1 ± h2 ∧ 
                  y = g h1 ±⇘N⇙ (monofun R M N f H h h2)))) z)")
 apply blast
apply (rule conjI)
 apply (rule Module.mHom_test)
 apply (rule mdl_is_module, assumption+)
 apply (rule conjI,
        rule Pi_I, simp add:mdl_carrier)
 apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp, simp)
 apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and x = x and N = N
        in ex_extensionTr, assumption+,
        (erule bexE)+, erule conjE, rotate_tac -1,
         frule sym,
        thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  x = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
                  g k1 ±⇘N⇙ monofun R M N f H h k2")
 apply (frule mdl_is_module[of "fgs R M H1"],
        frule_tac f = g and m = k1 in Module.mHom_mem[of "mdl M (fgs R M H1)" 
                   R N], assumption+, simp add:mdl_carrier)
 apply (frule_tac x = k2 in monofun_mem[of N h H _ f], assumption+)
 apply (frule Module.module_is_ag[of N],
        frule_tac x = "g k1" and y = "monofun R M N f H h k2 " in 
        aGroup.ag_pOp_closed[of N], assumption+, simp)
 apply (simp add:mdl_carrier)
 apply (rule conjI, (rule ballI)+) 
 apply (frule mdl_is_module[of "fgs R M (insert h H1)"],
        frule Module.module_is_ag[of "mdl M (fgs R M (insert h H1))"],
        frule_tac x = m and y = n in aGroup.ag_pOp_closed[of
         "mdl M (fgs R M (insert h H1))"],
        (simp add:mdl_carrier)+)
 apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp, simp)
 apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
       x = "m ±⇘mdl M (fgs R M H1 ∓ fgs R M {h})⇙ n" in ex_extensionTr, assumption+,
       (erule bexE)+, (erule conjE)+, simp,
       thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  k1 ± k2 = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
        g k1 ±⇘N⇙ monofun R M N f H h k2")
  apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
       x = m in ex_extensionTr, assumption+, (erule bexE)+, (erule conjE)+, 
       simp,
       thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  k1a ± k2a = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
        g k1a ±⇘N⇙ monofun R M N f H h k2a")
  apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
       x = n in ex_extensionTr, assumption+, (erule bexE)+, (erule conjE)+, 
       simp,
       thin_tac "(THE y. ∃h1∈fgs R M H1.  ∃h2∈fgs R M {h}.
                  k1b ± k2b = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
        g k1b ±⇘N⇙ monofun R M N f H h k2b")
  apply (simp add:mdl_def[of M "fgs R M H1 ∓ fgs R M {h}"],
         fold mdl_def)
  apply (frule_tac c = k1a in subsetD[of "fgs R M H1" "carrier M"], 
         assumption+,
         frule_tac c = k1b in subsetD[of "fgs R M H1" "carrier M"], 
         assumption+) apply (
         frule_tac c = k2a in subsetD[of "fgs R M {h}" "carrier M"], 
         assumption+,
         frule_tac c = k2b in subsetD[of "fgs R M {h}" "carrier M"], 
         assumption+)  
  apply (simp add:pOp_assocTr41[THEN sym], simp add:pOp_assocTr42,
        frule_tac x = k2a and y = k1b in ag_pOp_commute, assumption+, simp,
        thin_tac "k2a ± k1b = k1b ± k2a", simp add:pOp_assocTr42[THEN sym],
        simp add:pOp_assocTr41)
  apply(frule_tac h = k1a and k = k1b in submodule_pOp_closed[of "fgs R M H1"],
        assumption+)
  apply(frule_tac h = k2a and k = k2b in 
          submodule_pOp_closed[of "fgs R M {h}"], assumption+)      
  apply (frule_tac ?x1.0 = "k1a ± k1b" and ?x2.0 = k1 and ?y1.0 = "k2a ± k2b" 
         and ?y2.0 = k2 in sSum_unique[of N H H1 h], assumption+, simp,
         assumption+, erule conjE, rotate_tac -2, frule sym,
         thin_tac "k1a ± k1b = k1", frule sym, thin_tac "k2a ± k2b = k2",
         thin_tac "k1a ± k1b ± (k2a ± k2b) = k1 ± k2", simp,
         frule mdl_is_module[of "fgs R M H1"])
  apply (frule_tac m = k1a and n = k1b in Module.mHom_add[of 
                           "mdl M (fgs R M H1)" R N g], assumption+,
         simp add:mdl_carrier, simp add:mdl_carrier, 
         simp add:mdl_def, fold mdl_def)
  apply (simp add: monofun_add)
  apply (frule_tac m = k1a in Module.mHom_mem[of "mdl M (fgs R M H1)" R N g],
         assumption+, simp add:mdl_carrier,
         frule_tac m = k1b in Module.mHom_mem[of "mdl M (fgs R M H1)" R N g],
         assumption+, simp add:mdl_carrier,
         frule_tac x = k2a in monofun_mem[of N h H _ f], assumption+,
         frule_tac x = k2b in monofun_mem[of N h H _ f], assumption+)
  apply (frule Module.module_is_ag[of N],
         simp add:aGroup.pOp_assocTr41[of N, THEN sym], 
         simp add:aGroup.pOp_assocTr42[of N],
         simp add:aGroup.ag_pOp_commute[of N])
apply (rule ballI)+
apply (frule mdl_is_module[of "fgs R M (insert h H1)"])
 apply (frule_tac a = a and m = m in Module.sc_mem[of 
             "mdl M (fgs R M (insert h H1))" R], assumption+,
        simp add:mdl_carrier, simp add:mdl_carrier)
 apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp) 
 apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
       x = "a ⋅⇩s⇘mdl M (fgs R M (insert h H1))⇙ m" in ex_extensionTr, assumption+,
       simp)
 apply ((erule bexE)+, erule conjE, simp,
       thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  k1 ± k2 = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
                  g k1 ±⇘N⇙ monofun R M N f H h k2")
       apply (simp add:mdl_def, fold mdl_def)
 apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
       x = m in ex_extensionTr, assumption+,
       (erule bexE)+, erule conjE, simp,
       thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  k1a ± k2a = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
                  g k1a ±⇘N⇙ monofun R M N f H h k2a",
       frule_tac c = k1a in subsetD[of "fgs R M H1" "carrier M"], assumption+,
       frule_tac c = k1 in subsetD[of "fgs R M H1" "carrier M"], assumption+,
       frule_tac c = k2a in subsetD[of "fgs R M {h}" "carrier M"], assumption+,
       frule_tac c = k2 in subsetD[of "fgs R M {h}" "carrier M"], assumption+)        apply (simp add:sc_r_distr,
              frule_tac a = a and h = k1a in 
                    submodule_sc_closed[of "fgs R M H1"], assumption+,
              frule_tac a = a and h = k2a in 
                    submodule_sc_closed[of "fgs R M {h}"], assumption+)
  apply (frule_tac ?x1.0 = k1 and ?x2.0 = "a ⋅⇩s k1a" and ?y1.0 = k2 and
          ?y2.0 = "a ⋅⇩s k2a" in sSum_unique[of N H H1 h], assumption+,
          simp, assumption+, rule sym, assumption,
          thin_tac "a ⋅⇩s k1a ± a ⋅⇩s k2a = k1 ± k2", simp)
  apply (frule subset_trans[of H1 H "carrier M"], assumption+,
          frule mdl_is_module[of "fgs R M H1"])
  apply (frule_tac a = a and m = k1a in Module.mHom_lin[of "mdl M (fgs R M H1)"
          R N _ g], assumption+, simp add:mdl_carrier, assumption+)
  apply (simp add:mdl_def, fold mdl_def)
  apply (simp add:monofun_sprod)
  apply (frule_tac m = k1a in Module.mHom_mem[of "mdl M (fgs R M H1)" R N g],
          assumption+, simp add:mdl_carrier,
         frule_tac x = k2a in monofun_mem[of N h H _ f], assumption+,
         simp add:Module.sc_r_distr[of N])
apply (rule conjI) apply simp
  apply (cut_tac insert_sub[of H1 "carrier M" h], 
         frule elem_fgs[of "insert h H1" h], simp, simp)
  apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
         x = h in ex_extensionTr, assumption+)
   apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp, simp) 
   apply ((erule bexE)+, (erule conjE), simp,
         thin_tac "(THE y.
            ∃h1∈fgs R M H1.
               ∃h2∈fgs R M {k1 ± k2}.
                  k1 ± k2 = h1 ± h2 ∧
                  y = g h1 ±⇘N⇙ monofun R M N f H (k1 ± k2) h2) =
        g k1 ±⇘N⇙ monofun R M N f H (k1 ± k2) k2")
   apply (rotate_tac -1, frule sym, thin_tac "h = k1 ± k2", simp)
   apply (cut_tac elem_fgs[of "{h}" h], 
          frule ag_l_zero[THEN sym, of h])
   apply (frule submodule_inc_0[of "fgs R M H1"])
   apply (frule_tac ?x1.0 = k1 and ?x2.0 = 𝟬 and ?y1.0 = k2 and ?y2.0 = h in 
          sSum_unique[of N H H1 h], assumption+, simp, assumption+,
          simp, simp, simp add: monofun_eq_f)
   apply (cut_tac Module.mHom_0[of "mdl M (fgs R M H1)" R N g],
          simp add:mdl_def, fold mdl_def)
   apply (frule funcset_mem[of f H "carrier N" h], assumption+,
          frule Module.module_is_ag[of N], simp add:aGroup.l_zero,
          rule mdl_is_module, assumption+,
          rule subsetI, simp, simp, assumption+)
apply (rule ballI, simp,
       cut_tac x = z in elem_fgs[of "insert h H1"],
       rule subsetI, simp, erule disjE, simp, simp add:subsetD, 
       rule_tac c = z in subsetD[of "H1" "insert h H1"],
       rule subsetI, simp, assumption, simp) 

apply (frule_tac h = h and H = H and ?H1.0 = H1 and g = g and N = N and
         x = z in ex_extensionTr, assumption+) 
   apply (frule sSum_eq[THEN sym, of N H H1 h], assumption+, simp, simp) 
   apply ((erule bexE)+, (erule conjE), simp)
   apply (thin_tac "(THE y. ∃h1∈fgs R M H1. ∃h2∈fgs R M {h}.
                  k1 ± k2 = h1 ± h2 ∧ y = g h1 ±⇘N⇙ monofun R M N f H h h2) =
        g k1 ±⇘N⇙ monofun R M N f H h k2")
   apply (rotate_tac -1, frule sym, thin_tac "z = k1 ± k2", simp)
 apply (frule_tac x = z in elem_fgs[of H1], assumption,
       frule_tac c = z in subsetD[of H1 "carrier M"], assumption+,
       frule_tac t = z in ag_r_zero[THEN sym]) 
 apply (frule_tac ?x1.0 = k1 and ?x2.0 = z and ?y1.0 = k2 and ?y2.0 = 𝟬  in 
        sSum_unique[of N H H1 h], assumption+, simp, assumption+,
        simp add:submodule_inc_0, simp, simp)
 apply (simp add: monofun_0)
 apply (frule mdl_is_module[of "fgs R M H1"],
        frule_tac m = z in Module.mHom_mem[of "mdl M (fgs R M H1)" R N g],
        assumption+, simp add:mdl_carrier)
 apply (frule Module.module_is_ag[of N],
        simp add:aGroup.ag_r_zero)
done

lemma (in Module) mHom_mHom:"⟦R module N; g ∈ mHom R (mdl M (carrier M)) N⟧
       ⟹ g ∈ mHom R M N"
apply (rule mHom_test, assumption)
apply (rule conjI)
 apply (simp add:mHom_def aHom_def mdl_def)
 apply (simp add:mHom_def aHom_def mdl_def)
done


lemma (in Module) exist_extension_mhom:"⟦R module N; free_generator R M H; 
      f ∈ H → carrier N⟧ ⟹ ∃g∈mHom R M N. ∀x∈H. g x = f x"
supply [[simproc del: defined_all]]
apply (frule Order_od_fm_fun[of N H f], assumption+) 
apply (frule_tac  N = N and H = H and f = f in od_fm_fun_inductive, 
             assumption+)
apply (frule_tac D = "od_fm_fun R M N f H" in Order.g_Zorn_lemma3,
        assumption+)
apply (erule bexE)
apply (rule contrapos_pp, simp+)
 apply (simp add:maximal_element_def)
 apply (simp add:od_fm_fun_carrier)
 apply (cut_tac p = m in PairE_lemma, (erule exE)+, simp)
 apply (frule_tac a = x and b = y in mem_fsps_fst_sub[of N H f], assumption+)
 apply (case_tac "x ≠ H", frule not_sym)
 apply (frule_tac A = H and B = x in diff_nonempty, assumption,
        frule_tac A = "H - x" in nonempty_ex, erule exE,
        rename_tac m H1 g h)
 apply (frule_tac ?H1.0 = H1 and h = h and g = g in ex_extension[of N H f],
        assumption+, erule exE)
 apply (drule_tac x = "(H1 ∪ {h}, k)" in bspec, assumption)
 apply (simp add:od_fm_fun_def ole_def, fold od_fm_fun_def,
        simp add:insert_inc1, (erule conjE)+,
        cut_tac a = h and A = H1 in insert_inc2,
        rotate_tac -3, frule sym, thin_tac "H1 = insert h H1", simp)
 apply simp 
 apply (frule_tac a = H and b = y in mem_fsps_snd_mHom[of N H f], assumption+)
 apply (simp add:fgs_def free_generator_def generator_def)
 apply (frule_tac g = y in mHom_mHom[of N], assumption+,
        (erule conjE)+, thin_tac "∀n s. s ∈ {j. j ≤ n} → carrier R ∧
               (∃f. f ∈ {j. j ≤ n} → H ∧
                    inj_on f {j. j ≤ n} ∧ l_comb R M n s f = 𝟬) ⟶
               s ∈ {j. j ≤ n} → {𝟬⇘R⇙}")
 apply (drule_tac x = y in bspec, assumption+,
        simp add:fsps_def fsp_def)
done

section "Nakayama lemma" 

definition
  Lcg :: "[('r, 'm) Ring_scheme, ('a, 'r, 'm1) Module_scheme, nat] ⇒ bool" where
  "Lcg R M j ⟷ (∃H. finite_generator R M H ∧ j = card H)" 
 (* Least cardinality of generator *)

lemma (in Module) NAKTr1:"M fgover R ⟹ 
      ∃H. finite_generator R M H ∧ (LEAST j. 
        ∃L. finite_generator R M L ∧ j = card L) = card H"
apply (simp add:fGOver_def)
 apply (erule exE)
 apply (rule LeastI)
apply (rule_tac x = H in exI) apply simp
done

lemma (in Module) NAKTr2:"⟦Lcg R M j; k < (LEAST j. Lcg R M j)⟧ ⟹
                            ¬ Lcg R M k"
apply (rule not_less_Least, assumption+) 
done

lemma (in Module) NAKTr3:"⟦M fgover R; H ⊆ carrier M; finite H;
       card H < (LEAST j. ∃L. finite_generator R M L ∧ j = card L)⟧ ⟹
              ¬ finite_generator R M H"
apply (frule NAKTr1, erule exE, erule conjE) 
 apply (cut_tac j = "card Ha" and k = "card H" in NAKTr2)
 apply (simp add:Lcg_def, blast)
 apply (simp add:Lcg_def)
 apply (simp add:Lcg_def)
apply (rule contrapos_pp, simp+)
 apply (drule_tac a = H in forall_spec, assumption)
 apply simp
done

lemma (in Module) finite_gen_over_ideal:"⟦ideal R A; h ∈ {j. j ≤ (n::nat)} →
 carrier M; generator R M (h ` {j. j ≤ n}); A ⊙⇘R⇙ M = carrier M; 
 m ∈ carrier M ⟧  ⟹  ∃s∈{j. j ≤ n} → A. m = l_comb R M n s h"
apply (frule l_span_closed3[of "A" "h ` {j. j ≤ n}"], assumption+)
apply (rotate_tac -1, frule sym, 
        thin_tac "linear_span R M A (h ` {j. j ≤ n}) = carrier M")
 apply (frule eq_set_inc[of m "carrier M" 
                  "linear_span R M A (h ` {j. j ≤ n})"], assumption+)
 apply (thin_tac "carrier M = linear_span R M A (h ` {j. j ≤ n})")
 apply (simp add:linear_span_def) 
 apply (cut_tac Nset_nonempty[of n], simp)
 apply (case_tac "∀x. ¬ x ≤ n", simp, simp) (** simp no good **)
 apply (erule exE, (erule bexE)+)
apply (simp add:finite_lin_span)
done

lemma (in Module) NAKTr4:"⟦ideal R A; h ∈ {j. j ≤ (k::nat)} → carrier M; 
 0 < k;  h ` {j. j ≤ k} ⊆ carrier M; s ∈ {j. j ≤ k} → A; 
 h k = Σ⇩e M (λj. s j ⋅⇩s (h j)) (k - Suc 0) ± (s k ⋅⇩s (h k))⟧ ⟹ 
  (1⇩r⇘R⇙ ±⇘R⇙ (-⇩a⇘R⇙ (s k))) ⋅⇩s (h k) = Σ⇩e M (λj. s j ⋅⇩s (h j)) (k - Suc 0)"
apply (cut_tac sc_Ring)
apply (frule funcset_mem[of h "{j. j ≤ k}" "carrier M" k], simp)
apply (frule_tac funcset_mem[of s "{j. j ≤ k}" A k], simp,
       frule_tac h = "s k" in Ring.ideal_subset[of R A], assumption+)
apply (cut_tac n = "k - Suc 0" and f = "λj. s j ⋅⇩s h j" in nsum_mem)
apply (rule allI, rule impI, rule sc_mem,
       frule_tac x = j in funcset_mem[of s "{j. j ≤ k}" A ],
       simp)
 apply (simp add:Ring.ideal_subset)
 apply (cut_tac i = j and j = "k - Suc 0" and k = k in 
        le_trans, assumption+, simp,
        rule_tac x = j in funcset_mem[of h "{j. j ≤ k}" "carrier M"],
        assumption, simp)

 apply (frule sc_mem[of "s k" "h k"], assumption+,
        frule ag_mOp_closed[of "s k ⋅⇩s h k"])
 apply (frule_tac ag_pOp_add_r[of "h k"
        "Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0) ± s k ⋅⇩s h k" "-⇩a (s k ⋅⇩s h k)"],
         rule ag_pOp_closed, assumption+,
        thin_tac "h k = Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0) ± s k ⋅⇩s h k",
        simp add:ag_pOp_assoc ag_r_inv1 ag_r_zero,
        simp add:sc_minus_am1)
 apply (frule Ring.ring_is_ag, 
        frule aGroup.ag_mOp_closed[of R "s k"], assumption+)
       (** I don't know how to change s k to 1⇩r⇘R⇙ ⋅⇩s s k **) 
 apply (subgoal_tac "(1⇩r⇘R⇙ ±⇘R⇙ (-⇩a⇘R⇙ (s k))) ⋅⇩s h k = h k ± (-⇩a⇘R⇙ (s k)) ⋅⇩s h k",
        simp,
        thin_tac "h k ± (-⇩a⇘R⇙ (s k)) ⋅⇩s h k = Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0)")
 apply (cut_tac Ring.ring_one[of R],
        simp add:sc_l_distr sprod_one, assumption)
done
 
lemma (in Module) NAKTr5:"⟦¬ zeroring R; ideal R A; A ⊆ J_rad R; 
       A ⊙⇘R⇙ M = carrier M; finite_generator R M H; card H = Suc k; 0 < k⟧ ⟹
     ∃h ∈ {j. j ≤ k} → carrier M. H = h ` {j. j ≤ k} ∧  
             h k ∈ linear_span R M A (h ` {j. j ≤ (k - Suc 0)})"
apply (cut_tac sc_Ring)
 apply (insert Nset2_finiteTr [of "k"]) 
 apply (subgoal_tac "∃h. h ∈ {j. j ≤ k} → H ∧ surj_to h {j. j ≤ k} H")
 prefer 2 
 apply (subgoal_tac "finite H")
 apply blast apply (simp add:finite_generator_def) 
 apply (thin_tac " ∀A. finite A ∧ card A = Suc k ⟶
           (∃f. f ∈ {j. j ≤ k} → A ∧ surj_to f {j. j ≤ k} A)")
 apply (erule exE)
 apply (simp add:surj_to_def, erule conjE) apply (rotate_tac -1) 
 apply (drule sym)
apply (frule_tac f = h and A = "{j. j ≤ k}" and B = "H" and x = k in 
       funcset_mem)
 apply simp
 apply (simp add:finite_generator_def,
        simp add:generator_def, erule conjE)
 apply (cut_tac A = "h ` {j. j ≤ k}" and B = "carrier M" and c = "h k" in
   subsetD, assumption, simp)
 apply (frule_tac h = h and n = k and m = "h k" in finite_gen_over_ideal [of 
       "A"])
 apply (fastforce simp add:Pi_def image_def)
 apply (simp add:generator_def)
 apply assumption+
 apply (erule bexE)
 apply (frule_tac f = s and A = "{j. j ≤ k}" and B = A and x = k in 
           funcset_mem, simp, simp add:subsetD)
 apply (subgoal_tac "l_comb R M k s h = l_comb R M (Suc (k - Suc 0)) s h",
        simp del:Suc_pred,
        thin_tac "l_comb R M k s h = l_comb R M (Suc (k - Suc 0)) s h")
apply (cut_tac s = s and n = "k - Suc 0" and f = h and H = "h ` {j. j ≤ k}" 
       in l_comb_Suc[of _ A], assumption+,
       frule Ring.ideal_subset1[of R A], assumption,
       simp add:extend_fun, simp)
apply (rotate_tac -3, frule sym, 
       thin_tac "h k = l_comb R M (Suc (k - Suc 0)) s h", simp)
apply (frule_tac h = h and k = k and s = s in NAKTr4[of A])
 apply (fastforce simp add:Pi_def image_def)
 apply(assumption+, rule sym, simp add:l_comb_def)
apply (cut_tac H = "h ` {j. j ≤ (k - Suc 0)}" and s = s and n = "k - Suc 0" 
       and f = h in l_comb_mem_linear_span[of A], assumption+)
   apply (rule_tac A = "h ` {j. j ≤ k - Suc 0}" and 
           B = "h ` {j. j ≤ k}" and C = "carrier M" in  subset_trans)
   apply (rule subsetI, simp add:image_def, erule exE, erule conjE,
          cut_tac i = xa and j = "k - Suc 0" and k = k in le_trans,
           assumption, subst Suc_le_mono[THEN sym], simp, blast, assumption)
   apply (rule Pi_I, simp)
   apply (frule_tac x = x in le_pre_le[of _ k], simp add:Pi_def)
   apply (rule Pi_I, simp) 
   apply (unfold l_comb_def)
   apply (rotate_tac -2, frule sym,
    thin_tac "(1⇩r⇘R⇙ ±⇘R⇙ -⇩a⇘R⇙ (s k)) ⋅⇩s h k = Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0)",
    thin_tac "Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0) ± s k ⋅⇩s h k = h k",
    simp,
    thin_tac "Σ⇩e M (λj. s j ⋅⇩s h j) (k - Suc 0) = (1⇩r⇘R⇙ ±⇘R⇙ -⇩a⇘R⇙ (s k)) ⋅⇩s h k")
    apply (frule_tac x = "s k" in Ring.J_rad_unit [of R], assumption,
           frule_tac f = s and A = "{j. j ≤ k}" and B = A and x = k in 
           funcset_mem, simp, simp add:subsetD)
    apply (frule Ring.ring_one[of R],
           frule_tac a = "1⇩r⇘R⇙" in forall_spec, assumption)
    apply (frule_tac h = "s k" in Ring.ideal_subset[of R A], assumption+,
           frule Ring.ring_is_ag[of R],
           frule_tac x = "s k" in aGroup.ag_mOp_closed[of R], assumption,
           thin_tac "∀y. y ∈ carrier R ⟶ Unit R (1⇩r⇘R⇙ ±⇘R⇙ (-⇩a⇘R⇙ (s k)) ⋅⇩r⇘R⇙ y)",
           simp add:Ring.ring_r_one)
    apply (simp add:Unit_def, erule conjE, erule bexE)
    apply (simp add:Ring.ring_tOp_commute)
    apply (frule_tac H = "h ` {j. j ≤ k - Suc 0}" and r = b and 
          x = "(1⇩r⇘R⇙ ±⇘R⇙ (-⇩a⇘R⇙ (s k))) ⋅⇩s h k" in linear_span_sc_closed[of A])
    apply (rule_tac A = "h ` {j. j ≤ k - Suc 0}" and B = "h ` {j. j ≤ k}"
           and C = "carrier M" in subset_trans,
           rule subsetI, simp add:image_def, erule exE, erule conjE)
    apply (frule_tac x = xa and n = k in le_pre_le, blast, assumption+)
    apply (simp add:sc_assoc[THEN sym] sprod_one)
    apply(simp add:Pi_def)
    apply blast
 apply simp
done

lemma (in Module) NAK:"⟦¬ zeroring R; M fgover R; ideal R A; A ⊆ J_rad R;  
       A ⊙⇘R⇙ M = carrier M ⟧ ⟹ carrier M = {𝟬}"
apply (cut_tac sc_Ring)
apply (frule NAKTr1, erule exE, erule conjE)
apply (simp add:finite_generator_def, frule conjunct1, frule conjunct2,
       fold finite_generator_def)
apply (case_tac "H = {}", simp add:generator_def linear_span_def,
       frule_tac A = H in nonempty_card_pos1, assumption+)
apply (case_tac "card H = Suc 0", simp,
       frule_tac A = H in nonempty_ex, erule exE, rename_tac H h,
       frule_tac t = H and a1 = h in card1_tr0[THEN sym], assumption+, simp) 
apply (frule_tac H = "{h}" in generator_sub_carrier,
       frule sym, thin_tac "A ⊙⇘R⇙ M = carrier M", simp,
       thin_tac "carrier M = A ⊙⇘R⇙ M", simp add:smodule_ideal_coeff_def,
       simp add:generator_def) 
 apply (erule conjE, rotate_tac -1, frule sym, 
        thin_tac "linear_span R M (carrier R) {h} = carrier M", simp)
 apply (rotate_tac -1, frule sym,
        frule_tac a = h and A = "linear_span R M (carrier R) {h}" and
                  B = "carrier M" in eq_set_inc, assumption+,
        frule_tac a = h and A = "carrier M" in singleton_sub)
 apply (frule_tac H = "{h}" in l_spanA_l_span[of A], assumption+,
        thin_tac "carrier M = linear_span R M (carrier R) {h}",
        thin_tac "linear_span R M (carrier R) {h} = carrier M", simp,
        thin_tac "h ∈ linear_span R M (carrier R) {h}",
        thin_tac "linear_span R M A (linear_span R M (carrier R) {h}) =
           linear_span R M A {h}",
        thin_tac "(LEAST j. ∃L. finite L ∧
                   L ⊆ linear_span R M (carrier R) {h} ∧
                   linear_span R M (carrier R) L =
                   linear_span R M (carrier R) {h} ∧
                   j = card L) = Suc 0")
apply (frule_tac h = h and x = h in mem_single_l_span1[of A],
        assumption+, erule bexE,
       frule_tac h = a in Ring.ideal_subset[of R A], assumption+,
       frule_tac a = a and m = h in sc_mem, assumption+,
       frule_tac x = "a ⋅⇩s h" in ag_mOp_closed)
apply (frule_tac a = h and b = "a ⋅⇩s h" and c = "-⇩a (a ⋅⇩s h)" in
       ag_pOp_add_r, assumption+,
       thin_tac "h = a ⋅⇩s h", simp add:ag_r_inv1,
       simp add:sc_minus_am1,
       frule Ring.ring_is_ag[of R],
       frule_tac x = a in aGroup.ag_mOp_closed, assumption)
apply (subgoal_tac "h ± (-⇩a⇘R⇙ a) ⋅⇩s h = 1⇩r⇘R⇙ ⋅⇩s h ±  (-⇩a⇘R⇙ a) ⋅⇩s h", simp)
apply (frule Ring.ring_one[of R],
       simp add:sc_l_distr[THEN sym],
       frule_tac x = a in Ring.J_rad_unit [of R], assumption, 
       simp add:subsetD,
       drule_tac a = "1⇩r⇘R⇙" in forall_spec, assumption,
       simp add:Ring.ring_r_one,
       simp add:Unit_def, erule conjE, erule bexE,
       simp add:Ring.ring_tOp_commute,
       frule_tac a = b and b = "1⇩r⇘R⇙ ±⇘R⇙ -⇩a⇘R⇙ a" and m = h in sc_assoc,
       rule aGroup.ag_pOp_closed, assumption+, simp add:sprod_one sc_a_0,
       simp add:l_span_zero, simp add:sprod_one)
 
 apply (rotate_tac -1, frule not_sym,
        frule_tac m = "Suc 0" and n = "card H" in noteq_le_less, assumption,
        thin_tac "Suc 0 ≤ card H", thin_tac "card H ≠ Suc 0")
 apply (frule_tac a = "Suc 0" and b = "card H" and c = "Suc 0" in
                  diff_less_mono, simp,
        thin_tac "Suc 0 < card H")
 apply (frule_tac H = H and k = "card H - Suc 0" in NAKTr5[of A],
         assumption+, simp, simp)
 apply (erule bexE)
 apply (frule_tac H = H and ?H1.0 = "h ` {j. j ≤ card H - Suc 0 - Suc 0}" in
        generator_generator,
       frule_tac f = h and A = "{j. j ≤ card H - Suc 0}" and B = "carrier M"
       and ?A1.0 = "{j. j ≤ card H - Suc 0 - Suc 0}" in image_sub,
       rule subsetI, simp+)
 apply (erule conjE)
   apply (cut_tac f = h and n = "card H - Suc (Suc 0)" in image_Nset_Suc)
   apply (frule_tac m = "Suc 0" and n = "card H" in Suc_leI)
   apply (simp add:Suc_Suc_Tr)
   apply (frule_tac f = h and A = "{j. j ≤ card H - Suc 0}" and 
          B = "carrier M" and ?A1.0 = "{j. j ≤ card H - Suc 0 - Suc 0}" in 
         image_sub,
         rule subsetI, simp)
   apply (frule_tac H = "h ` {j. j ≤ card H - Suc 0 - Suc 0}" in 
          lin_span_coeff_mono[of A], simp, simp)
   apply (frule_tac c = "h (card H - Suc 0)" and A = 
          "linear_span R M A (h ` {j. j ≤ card H - Suc (Suc 0)})" and 
           B = "linear_span R M (carrier R)
              (h ` {j. j ≤ card H - Suc (Suc 0)})" in subsetD, assumption)
  apply (rule_tac A = H and B = "insert (h (card H - Suc 0)) 
                        (h ` {j. j ≤ card H - Suc (Suc 0)})" and 
          C = "linear_span R M (carrier R)
                  (h ` {j. j ≤ card H - Suc (Suc 0)})" in subset_trans) 
  apply simp
  apply (rule_tac A = "h ` {j. j ≤ card H - Suc (Suc 0)}" and 
         B = "linear_span R M (carrier R)
           (h ` {j. j ≤ card H - Suc (Suc 0)})" and a = "h (card H - Suc 0)" 
        in insert_sub)
  apply (rule subsetI)
  apply (rule_tac H = "h ` {j. j ≤ card H - Suc (Suc 0)}" and h = x in
         h_in_linear_span, assumption+)
  apply (frule_tac H = "h ` {j. j ≤ card H - Suc 0 - Suc 0}" in NAKTr3)
  apply (simp add:generator_sub_carrier)
  apply (rule finite_imageI, simp) 
  apply (thin_tac "H = h ` {j. j ≤ card H - Suc 0} ∧
           h (card H - Suc 0)
           ∈ linear_span R M A (h ` {j. j ≤ card H - Suc 0 - Suc 0})")
  apply (cut_tac k = "card H - Suc 0 - Suc 0" in finite_Collect_le_nat,
         frule_tac A = "{j. j ≤ card H - Suc 0 - Suc 0}" and f = h in 
                   card_image_le,
         simp)
  apply (frule_tac m = "Suc 0" and n = "card H" in  Suc_leI,
         simp add:Suc_Suc_Tr, simp add:finite_generator_def) (*
  apply (rule_tac i = "card (h ` {j. j ≤ card H - Suc (Suc 0)})" and 
         j = "card H - Suc 0" and k = "card H" in Nat.le_less_trans, assumption+)  
  apply simp*)
  apply (cut_tac k = "card H - Suc 0 - Suc 0" in finite_Collect_le_nat,
         frule_tac F = "{j. j ≤ card H - Suc 0 - Suc 0}" and h = h in 
         finite_imageI, simp add:finite_generator_def)
done
 
lemma (in Module) fg_qmodule:"⟦ M fgover R; submodule R M N⟧ ⟹
                          (M /⇩m N) fgover R" 
apply (frule mpj_mHom[of N])
apply (frule mpj_surjec [of N])
apply (rule surjec_finitely_gen [of "M /⇩m N" "mpj M N"])
apply (simp add:qmodule_module)
apply assumption+
done   

lemma (in Module) NAK1:"⟦¬ zeroring R; M fgover R; submodule R M N; 
      ideal R A; A ⊆ J_rad R;  carrier M = A ⊙⇘R⇙ M ∓ N ⟧ ⟹ carrier M = N"
apply (subgoal_tac "A ⊙⇘R⇙ (M /⇩m N) = carrier (M /⇩m N)")
apply (frule fg_qmodule [of N], assumption+)
apply (frule qmodule_module [of N])
apply (frule Module.NAK [of "M /⇩m N" R "A"], assumption+,
       thin_tac "R module M /⇩m N", thin_tac "M /⇩m N fgover R",
       thin_tac "A ⊙⇘R⇙ M /⇩m N = carrier (M /⇩m N)",
       thin_tac "carrier M = A ⊙⇘R⇙ M ∓ N")
 apply (simp add:qmodule_def)
apply (rule equalityI) 
 apply (rule subsetI)
 apply (frule_tac m = x in set_mr_cos_mem[of N], assumption)
 apply simp
 apply (frule_tac m = x in m_in_mr_coset[of N], assumption, simp)
 apply (simp add:submodule_subset)
apply (subst smodule_ideal_coeff_def)
apply (frule qmodule_module [of N]) 
 apply (frule Module.lin_span_sub_carrier[of "M /⇩m N" R A "carrier (M /⇩m N)"],
        assumption, simp)
 apply (rule equalityI, assumption+)
 apply (thin_tac "linear_span R (M /⇩m N) A (carrier (M /⇩m N)) ⊆ 
                                                      carrier (M /⇩m N)")
 apply (rule subsetI) 
 apply (simp add:qmodule_carr)
 apply (frule_tac x = x in mem_set_mr_cos[of N], assumption, erule bexE)
 apply (frule smodule_ideal_coeff_is_Submodule[of A],
        frule submodule_subset,
        frule submodule_subset[of "A ⊙⇘R⇙ M"])
 apply (frule_tac x = m in mem_set_sum[of "A ⊙⇘R⇙ M" "N"], assumption+,
        simp, (erule bexE)+)
 apply simp
  apply (frule submodule_asubg[of N])
  apply (frule sym, thin_tac "carrier M = A ⊙⇘R⇙ M ∓ N", simp)
  apply (frule_tac c = h in subsetD[of "A ⊙⇘R⇙ M" "carrier M"], assumption+,
         frule_tac c = k in subsetD[of N "carrier M"], assumption+,
         frule_tac x = h and y = k in ag_pOp_commute, assumption+, simp)
  apply (simp add:arcos_fixed[THEN sym, of N], thin_tac "h ± k = k ± h",
         thin_tac "m = k ± h",
         thin_tac "submodule R M (A ⊙⇘R⇙ M)",
         thin_tac "A ⊙⇘R⇙ M ⊆ carrier M",
         thin_tac "A ⊙⇘R⇙ M ∓ N = carrier M")
  apply (simp add:smodule_ideal_coeff_def)
  apply (frule_tac h = h in linmap_im_linspan1 [of A "M /⇩m N" "mpj M N" 
         "carrier M"], assumption+,
         rule mpj_mHom[of N], assumption, simp, assumption)
  apply (frule_tac m = h in elem_mpj[of _ N], assumption,
         frule_tac mpj_surjec[of N], 
         simp add:surjec_def surj_to_def qmodule_carr)
done

section "Direct sum and direct products of modules"

definition
  prodM_sprod :: "[('r, 'm) Ring_scheme, 'i set, 
      'i ⇒ ('a, 'r, 'm1) Module_scheme] ⇒  'r ⇒ ('i ⇒ 'a) ⇒  ('i ⇒ 'a)" where
  "prodM_sprod R I A = (λa∈carrier R. λg∈carr_prodag I A. 
                                         (λj∈I. a ⋅⇩s⇘(A j)⇙ (g j)))"

definition
  prodM :: "[('r, 'm) Ring_scheme, 'i set, 'i ⇒ ('a, 'r, 'm1) Module_scheme] ⇒
     ⦇ carrier:: ('i ⇒ 'a) set, 
       pop::['i ⇒ 'a, 'i ⇒ 'a] ⇒ ('i ⇒ 'a),
       mop:: ('i ⇒ 'a) ⇒ ('i ⇒ 'a), zero::('i ⇒ 'a), 
       sprod :: ['r, 'i ⇒ 'a] ⇒ ('i ⇒ 'a) ⦈" where
  "prodM R I A = ⦇carrier = carr_prodag I A, 
    pop = prod_pOp I A, mop = prod_mOp I A,
    zero = prod_zero I A, sprod = prodM_sprod R I A ⦈"  

definition
  mProject :: "[('r, 'm) Ring_scheme, 'i set,
             'i ⇒ ('a, 'r, 'more) Module_scheme, 'i] ⇒ ('i ⇒ 'a) ⇒ 'a" where
  "mProject R I A j = (λf∈carr_prodag I A. f j)"

abbreviation
  PRODMODULES  ("(3mΠ⇘_ _⇙ _)" [72,72,73]72) where
  "mΠ⇘R I⇙ A == prodM R I A"

lemma (in Ring) prodM_carr:"⟦∀i∈I. (R module (M i))⟧ ⟹ 
                                carrier (prodM R I M) = carr_prodag I M"
apply (simp add:prodM_def)
done

lemma (in Ring) prodM_mem_eq:"⟦∀i∈I. (R module (M i)); 
      m1 ∈ carrier (prodM R I M); m2 ∈ carrier (prodM R I M); 
      ∀i∈I. m1 i = m2 i ⟧ ⟹ m1 = m2" 
apply (simp add:prodM_carr [of I M])
apply (rule carr_prodag_mem_eq [of I M])
apply (rule ballI, drule_tac x = k in bspec, assumption,
       simp add:Module.module_is_ag)
apply assumption+
done

lemma (in Ring) prodM_sprod_mem:"⟦∀i∈I. (R module (M i)); a ∈ carrier R;
       m ∈ carr_prodag I M⟧ ⟹ prodM_sprod R I M a m ∈ carr_prodag I M" 
apply (simp add:prodM_sprod_def carr_prodag_def)
apply (erule conjE)+
apply (rule conjI)
 apply (rule Pi_I)
 apply (simp add:Un_carrier_def)
 apply (drule_tac x = x in bspec, assumption,
        drule_tac x = x in bspec, assumption+)

 apply (frule_tac R = R and M = "M x" and a = a and m = "m x" in
        Module.sc_mem, assumption+, blast)
 apply (rule ballI, 
        drule_tac x = i in bspec, assumption,
        drule_tac x = i in bspec, assumption+)
       
 apply (frule_tac M = "M i" and a = a and m = "m i" in 
            Module.sc_mem [of _ "R"], assumption+)
done

lemma (in Ring) prodM_sprod_val:"⟦∀i∈I. (R module (M i)); a ∈ carrier R;
 m ∈ carr_prodag I M; j ∈ I⟧ ⟹ (prodM_sprod R I M a m) j = a ⋅⇩s⇘(M j)⇙ (m j)" 
apply (simp add:prodM_sprod_def)
done

lemma (in Ring) prodM_Module:"∀i∈I. (R module (M i)) ⟹ 
                                      R module (prodM R I M)"
apply (rule Module.intro)
 apply (cut_tac prodag_aGroup[of I M])
apply (simp add:prodM_def prodag_def aGroup_def)
apply (erule conjE)+
 apply (rule allI, rule impI)
 apply (rotate_tac -2,
        frule_tac a = a in forall_spec, assumption)
 apply (thin_tac "∀a. a ∈ carr_prodag I M ⟶ 
                                      prod_pOp I M (prod_zero I M) a = a",
        thin_tac "∀i∈I. R module M i",
        thin_tac "∀a. a ∈ carr_prodag I M ⟶ (∀b. b ∈ carr_prodag I M ⟶
             (∀c. c ∈ carr_prodag I M ⟶ prod_pOp I M (prod_pOp I M a b) c =
                       prod_pOp I M a (prod_pOp I M b c)))",
        thin_tac "∀a. a ∈ carr_prodag I M ⟶
             prod_pOp I M (prod_mOp I M a) a = prod_zero I M",
        frule_tac a = "prod_zero I M" in forall_spec, assumption,
        thin_tac "∀a. a ∈ carr_prodag I M ⟶ (∀b. b ∈ carr_prodag I M ⟶
                  prod_pOp I M a b = prod_pOp I M b a)",
        frule_tac a = a in forall_spec, assumption,
        thin_tac "∀b. b ∈ carr_prodag I M ⟶ prod_pOp I M (prod_zero I M) b =
             prod_pOp I M b (prod_zero I M)", simp)
 apply (rule ballI, drule_tac x = k in bspec, assumption,
        simp add:Module.module_is_ag)
 apply (rule Module_axioms.intro)
 apply (cut_tac Ring, assumption)
 apply (simp add:prodM_carr, simp add:prodM_def prodM_sprod_mem)
 apply (simp add:prodM_carr, simp add:prodM_def)
 apply (frule_tac a = a and m = m in prodM_sprod_mem[of I M], assumption+,
        frule_tac a = b and m = m in prodM_sprod_mem[of I M], assumption+,
       (cut_tac ring_is_ag,
        frule_tac x = a and y = b in aGroup.ag_pOp_closed[of R], assumption+),
        frule_tac a = "a ± b" and m = m in prodM_sprod_mem[of I M], 
        assumption+)
 apply (rule prodM_mem_eq[of I M], assumption, simp add:prodM_carr)
 apply (simp add:prodM_carr,
        rule_tac X = "prodM_sprod R I M a m" and Y = "prodM_sprod R I M b m" 
        in prod_pOp_mem[of I M],
        (rule ballI, drule_tac x = k in bspec, assumption,
        simp add:Module.module_is_ag),
        assumption+)      
 apply (rule ballI,
        simp add:prodM_sprod_def prod_pOp_def,
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. R module M i",
        thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
        thin_tac "(λj∈I. b ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
        thin_tac "(λj∈I. (a ± b) ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
        simp add:carr_prodag_def, (erule conjE)+,
        drule_tac x = i in bspec, assumption+)

apply (cut_tac Ring, simp add:Module.sc_l_distr)
  apply (simp add:prodM_carr)
  apply (simp add:prodM_def)
  apply (cut_tac X = m and Y = n in prod_pOp_mem[of I M],
         (rule ballI, frule_tac x = k in bspec, assumption,
          thin_tac "∀i∈I. R module M i", simp add:Module.module_is_ag),
          assumption+)
  apply (frule_tac a = a and m = "prod_pOp I M m n" in prodM_sprod_mem[of I M],
         assumption+)
 
  apply (rule prodM_mem_eq[of I M], assumption, simp add:prodM_carr)      
  apply (simp add:prodM_carr,
         frule_tac a = a and m = m in prodM_sprod_mem[of I M], assumption+,
         frule_tac a = a and m = n in prodM_sprod_mem[of I M], assumption+,
         rule_tac X = "prodM_sprod R I M a m" and Y = "prodM_sprod R I M a n" 
        in prod_pOp_mem[of I M],
        (rule ballI, drule_tac x = k in bspec, assumption,
        simp add:Module.module_is_ag),
        assumption+)
  apply (rule ballI)
  apply (frule_tac a = a and m = m in prodM_sprod_mem[of I M], assumption+,
         frule_tac a = a and m = n in prodM_sprod_mem[of I M], assumption+,
         simp add:prod_pOp_def prodM_sprod_def,
         drule_tac x = i in bspec, assumption,
         thin_tac "(λx∈I. m x ±⇘M x⇙ n x) ∈ carr_prodag I M",
         thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ (if j ∈ I then m j ±⇘M j⇙ n j else undefined))
        ∈ carr_prodag I M",
         thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
         thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ n j) ∈ carr_prodag I M")
   apply (simp add:carr_prodag_def, (erule conjE)+,
          drule_tac x = i in bspec, assumption,
          drule_tac x = i in bspec, assumption)
    
   apply (simp add:Module.sc_r_distr)

  apply (simp add:prodM_carr,
         frule_tac a = b and m = m in prodM_sprod_mem[of I M], assumption+,
         frule_tac a = a and m = "prodM_sprod R I M b m" in prodM_sprod_mem[of
          I M], assumption+)
  apply (frule_tac x = a and y = b in ring_tOp_closed, assumption+,
         frule_tac a = "a ⋅⇩r b" and m = m in prodM_sprod_mem[of I M], 
         assumption+)
  apply (simp add:prodM_def,
         rule prodM_mem_eq, assumption+, simp add:prodM_carr,
         simp add:prodM_carr)
  apply (rule ballI, simp add:prodM_sprod_def,
         drule_tac x = i in bspec, assumption,
         thin_tac "(λj∈I. b ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
         thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ (if j ∈ I then b ⋅⇩s⇘M j⇙ m j else undefined))
        ∈ carr_prodag I M",
         thin_tac "(λj∈I. (a ⋅⇩r b) ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
         simp add:carr_prodag_def, (erule conjE)+,
         drule_tac x = i in bspec, assumption)
     
   apply (simp add:Module.sc_assoc)

  apply (simp add:prodM_carr, cut_tac ring_one,
         frule_tac a = "1⇩r"  and m = m in prodM_sprod_mem[of I M], assumption+,
         rule prodM_mem_eq, assumption+, simp add:prodM_carr,
         simp add:prodM_def, simp add:prodM_def)
  apply (rule ballI, simp add:prodM_def,
         thin_tac "prodM_sprod R I M 1⇩r m ∈ carr_prodag I M",
         simp add:prodM_sprod_def,
         drule_tac x = i in bspec, assumption,
         simp add:carr_prodag_def, (erule conjE)+,
         drule_tac x = i in bspec, assumption,
         simp add:Module.sprod_one)
done
         
definition
  dsumM :: "[('r, 'm) Ring_scheme, 'i set, 'i ⇒ ('a, 'r, 'more) Module_scheme]
  ⇒  ⦇ carrier:: ('i ⇒ 'a) set, 
        pop::['i ⇒ 'a, 'i ⇒ 'a] ⇒ ('i ⇒ 'a),
        mop:: ('i ⇒ 'a) ⇒ ('i ⇒ 'a), 
        zero::('i ⇒ 'a), 
        sprod :: ['r, 'i ⇒ 'a] ⇒ ('i ⇒ 'a) ⦈" where
 
  "dsumM R I A = ⦇ carrier = carr_dsumag I A, 
     pop = prod_pOp I A, mop = prod_mOp I A,
     zero = prod_zero I A, sprod = prodM_sprod R I A⦈"  

abbreviation
  DSUMMOD  ("(3⇘_⇙Σ⇩d⇘_⇙ _)" [72,72,73]72) where
  "⇘R⇙Σ⇩d⇘I⇙ A == dsumM R I A"

lemma (in Ring) dsumM_carr:"carrier (dsumM R I M) = carr_dsumag I M"
by (simp add:dsumM_def)

lemma (in Ring) dsum_sprod_mem:"⟦∀i∈I. R module M i; a ∈ carrier R;
       b ∈ carr_dsumag I M⟧  ⟹ prodM_sprod R I M a b ∈ carr_dsumag I M"
apply (simp add:carr_dsumag_def)
 apply (simp add:finiteHom_def, erule conjE, erule exE, (erule conjE)+,
        frule_tac a = a and m = b in prodM_sprod_mem[of I M], assumption+)
 apply (subgoal_tac "∀j∈I - H. prodM_sprod R I M a b j = 𝟬⇘M j⇙", blast)
 apply (rule ballI, 
        drule_tac x = j in bspec, assumption,
        drule_tac x = j in bspec, simp)
      
 apply (subst prodM_sprod_def, simp)
 apply (simp add:Module.sc_a_0)
done

lemma (in Ring) carr_dsum_prod:"carr_dsumag I M ⊆ carr_prodag I M"
apply (rule subsetI) apply (simp add:carr_dsumag_def finiteHom_def) 
done

lemma (in Ring) carr_dsum_prod1:"
                 ∀x. x ∈ carr_dsumag I M ⟶ x ∈ carr_prodag I M"
apply (rule allI) apply (rule impI)
apply (cut_tac carr_dsum_prod [of I M])
apply (simp add:subsetD)
done

lemma (in Ring) carr_dsumM_mem_eq:"⟦∀i∈I. R module M i; x ∈ carr_dsumag I M;
      y ∈ carr_dsumag I M; ∀j∈I. x j = y j⟧ ⟹ x = y" 
apply (cut_tac carr_dsum_prod [of I M])
apply (frule subsetD [of "carr_dsumag I M" "carr_prodag I M" "x"], assumption+,
       frule subsetD [of "carr_dsumag I M" "carr_prodag I M" "y"], assumption+)
apply (subgoal_tac "∀i∈I. aGroup (M i)")
apply (rule carr_prodag_mem_eq [of "I" "M"], assumption+)
apply (rule ballI) 
apply (drule_tac x = i in bspec, assumption,
       simp add:Module.module_is_ag)
done

lemma (in Ring) dsumM_Module:"∀i∈I. R module (M i) ⟹ R module (⇘R⇙Σ⇩d⇘I⇙ M)"
apply (rule Module.intro)
 apply (cut_tac prodag_aGroup[of I M])
 apply (cut_tac carr_dsum_prod1[of I M])
apply (simp add:dsumM_def prodag_def aGroup_def,
       cut_tac dsum_pOp_func[of I M], simp,
       cut_tac dsum_iOp_func[of I M], simp,
       cut_tac dsum_zero_func[of I M], simp)
 apply (erule conjE)+
 apply (rule allI, rule impI,
        thin_tac "∀a. a ∈ carr_prodag I M ⟶
             (∀b. b ∈ carr_prodag I M ⟶
                  (∀c. c ∈ carr_prodag I M ⟶
                       prod_pOp I M (prod_pOp I M a b) c =
                       prod_pOp I M a (prod_pOp I M b c)))",
        thin_tac "∀i∈I. R module M i")
  apply (frule_tac a = a in forall_spec, assumption,
         drule_tac a = "prod_zero I M" in forall_spec, assumption)
  apply (drule_tac a = a in forall_spec, assumption,
         rotate_tac -1,
         drule_tac a = "prod_zero I M" in forall_spec, assumption, simp)

  apply (rule ballI, drule_tac x = k in bspec, assumption,
         simp add:Module.module_is_ag) 
  apply (rule ballI, drule_tac x = k in bspec, assumption,
         (simp add:Module.module_is_ag)+)
  apply (rule ballI, drule_tac x = k in bspec, assumption+,
         simp add:Module.module_is_ag)+

apply (rule Module_axioms.intro)
 apply (cut_tac Ring, simp del: Pi_split_insert_domain,
        simp add:dsumM_carr dsumM_def del: Pi_split_insert_domain,
        simp add:dsum_sprod_mem del: Pi_split_insert_domain)

(* sc_l_distr *)
 apply (cut_tac ring_is_ag,
        frule_tac x = a and y = b in aGroup.ag_pOp_closed, assumption+,
        simp add:dsumM_carr del: Pi_split_insert_domain,
        frule_tac a = a and b = m in dsum_sprod_mem[of I M], assumption+,
        frule_tac a = b and b = m in dsum_sprod_mem[of I M], assumption+,
        frule_tac a = "a ± b" and b = m in dsum_sprod_mem[of I M], assumption+,
        simp add:dsumM_def del: Pi_split_insert_domain,
        cut_tac X = "prodM_sprod R I M a m" and Y = "prodM_sprod R I M b m" in
        prod_pOp_mem[of I M],
        (rule ballI, frule_tac x = k in bspec, assumption,
        thin_tac "∀i∈I. R module M i", simp add:Module.module_is_ag del: Pi_split_insert_domain),
        (cut_tac carr_dsum_prod[of I M], simp add:subsetD del: Pi_split_insert_domain)+)
   apply(cut_tac carr_dsum_prod1[of I M])
apply(rule prodM_mem_eq)
apply(assumption+)
apply((simp add:prodM_carr del: Pi_split_insert_domain)+)
apply(rule ballI)
apply(simp add:prodM_sprod_def prod_pOp_def del: Pi_split_insert_domain PiE_restrict)
apply(thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
        thin_tac "(λj∈I. b ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
        thin_tac "(λj∈I. (a ± b) ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
        thin_tac "(λx∈I. (if x ∈ I then a ⋅⇩s⇘M x⇙ m x else undefined) ±⇘M x⇙
               (if x ∈ I then b ⋅⇩s⇘M x⇙ m x else undefined))
        ∈ carr_prodag I M")
   apply (frule_tac a = m in forall_spec, assumption,
               thin_tac "∀x. x ∈ carr_dsumag I M ⟶ x ∈ carr_prodag I M",
               frule_tac x = i in bspec, assumption,
               thin_tac "∀i∈I. R module M i",
               thin_tac "m ∈ carr_dsumag I M",
               simp add:carr_prodag_def, (erule conjE)+,
               frule_tac x = i in bspec, assumption,
               thin_tac "∀i∈I. m i ∈ carrier (M i)")
    apply (simp add:Module.sc_l_distr)

 (** sc_r_distr **)
 apply (simp add:dsumM_carr,
        frule_tac a = a and b = m in dsum_sprod_mem[of I M], assumption+,
        frule_tac a = a and b = n in dsum_sprod_mem[of I M], assumption+)
 apply (simp add:dsumM_def, cut_tac carr_dsum_prod1[of I M],
        cut_tac X = m and Y = n in prod_pOp_mem[of I M],
        (rule ballI, frule_tac x = k in bspec, assumption,
        thin_tac "∀i∈I. R module M i", simp add:Module.module_is_ag), simp+,
        frule_tac a = a and m = "prod_pOp I M m n" in prodM_sprod_mem[of I M],
        assumption, simp)
 apply (cut_tac X = "prodM_sprod R I M a m" and Y = "prodM_sprod R I M a n" in
        prod_pOp_mem[of I M],
        (rule ballI, frule_tac x = k in bspec, assumption,
        thin_tac "∀i∈I. R module M i", simp add:Module.module_is_ag), simp+,
        rule_tac ?m1.0 = "prodM_sprod R I M a (prod_pOp I M m n)" and 
        ?m2.0 = "prod_pOp I M (prodM_sprod R I M a m) (prodM_sprod R I M a n)"
        in prodM_mem_eq[of I M], assumption, (simp add:prodM_carr)+)
 apply (rule ballI,
        frule_tac x = i in bspec, assumption,
        thin_tac "prodM_sprod R I M a m ∈ carr_dsumag I M",
        thin_tac "prodM_sprod R I M a n ∈ carr_dsumag I M")
 apply (rotate_tac 1,
        frule_tac a = m in forall_spec, assumption,
        frule_tac a = n in forall_spec, assumption,
        thin_tac "∀x. x ∈ carr_dsumag I M ⟶ x ∈ carr_prodag I M",
        thin_tac "m ∈ carr_dsumag I M",
        thin_tac "n ∈ carr_dsumag I M")
 apply (frule_tac a = a and m = m in prodM_sprod_mem[of I M], assumption+, 
        frule_tac a = a and m = n in prodM_sprod_mem[of I M], assumption+)
 apply (simp add:prodM_sprod_def prod_pOp_def del: PiE_restrict,
        thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ (if j ∈ I then m j ±⇘M j⇙ n j else undefined))
        ∈ carr_prodag I M",
        thin_tac "(λx∈I. (if x ∈ I then a ⋅⇩s⇘M x⇙ m x else undefined) ±⇘M x⇙
               (if x ∈ I then a ⋅⇩s⇘M x⇙ n x else undefined))
        ∈ carr_prodag I M",
        thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M",
        thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ n j) ∈ carr_prodag I M",
        thin_tac "(λx∈I. m x ±⇘M x⇙ n x) ∈ carr_prodag I M")
  apply (simp add:carr_prodag_def, (erule conjE)+,
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. R module M i",
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. m i ∈ carrier (M i)",
        frule_tac x = i in bspec, assumption,
        simp add:Module.sc_r_distr)

  apply (frule_tac x = a and y = b in ring_tOp_closed, assumption+,
        simp add:dsumM_carr,
     frule_tac a = b and b = m in dsum_sprod_mem[of I M], assumption+,
     frule_tac a = a and b = "prodM_sprod R I M b m" in dsum_sprod_mem[of I M],
     assumption+,
     frule_tac a = "a ⋅⇩r b" and b = m in dsum_sprod_mem[of I M], assumption+)
 apply (cut_tac carr_dsum_prod1[of I M])
 apply (simp add:dsumM_def,
        rule_tac ?m1.0 = "prodM_sprod R I M (a ⋅⇩r b) m" and 
        ?m2.0 = "prodM_sprod R I M a (prodM_sprod R I M b m)"
        in prodM_mem_eq[of I M], assumption, (simp add:prodM_carr)+)
 apply (rule ballI, simp add:prodM_sprod_def,
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. R module M i",
        thin_tac "(λj∈I. b ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
        thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ (if j ∈ I then b ⋅⇩s⇘M j⇙ m j else undefined))
        ∈ carr_dsumag I M",
        thin_tac "(λj∈I. (a ⋅⇩r b) ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
        frule_tac a = m in forall_spec, assumption,
        thin_tac "∀x. x ∈ carr_dsumag I M ⟶ x ∈ carr_prodag I M",
        thin_tac "m ∈ carr_dsumag I M",
        simp add:carr_prodag_def, (erule conjE)+,
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. m i ∈ carrier (M i)",
        simp add:Module.sc_assoc)

  apply (simp add:dsumM_carr)      
  apply (simp add:dsumM_def)
  apply (cut_tac ring_one,
         cut_tac carr_dsum_prod1[of I M],
         frule_tac a = "1⇩r" and b = m in dsum_sprod_mem[of I M], assumption+,
         rule_tac ?m1.0 = "prodM_sprod R I M 1⇩r m" and
         ?m2.0 = m in prodM_mem_eq[of I M], assumption, (simp add:prodM_carr)+,
         frule_tac a = m in forall_spec, assumption,
         frule_tac a = "prodM_sprod R I M 1⇩r m" in forall_spec, assumption,
         thin_tac "∀x. x ∈ carr_dsumag I M ⟶ x ∈ carr_prodag I M")
  apply (rule ballI,
        frule_tac x = i in bspec, assumption,
        thin_tac "∀i∈I. R module M i")
 apply (simp add:prodM_sprod_def)
  apply (thin_tac "(λj∈I. 1⇩r ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
         thin_tac "(λj∈I. 1⇩r ⋅⇩s⇘M j⇙ m j) ∈ carr_prodag I M")
  apply (simp add:carr_prodag_def, (erule conjE)+,
         frule_tac x = i in bspec, assumption,
         simp add:Module.sprod_one)
done
  
definition
  ringModule :: "('r, 'b) Ring_scheme ⇒ ('r, 'r) Module"
                ("(M⇘_⇙)" [998]999) where
  "M⇘R⇙ = ⦇carrier = carrier R, pop = pop R, mop = mop R,
        zero = zero R, sprod = tp R⦈" 

lemma (in Ring) ringModule_Module:"R module M⇘R⇙"
apply (rule Module.intro)
 apply (simp add:aGroup_def,  simp add:ringModule_def,
        simp add:pop_closed,  simp add:pop_aassoc,
        simp add:pop_commute, simp add:mop_closed,
        simp add:l_m,         simp add:ex_zero,
        simp add:l_zero)

apply (rule Module_axioms.intro)
 apply (cut_tac Ring, assumption,
        simp add:ringModule_def, simp add:ring_tOp_closed,
        simp add:ringModule_def, simp add:ring_distrib2,
        simp add:ringModule_def, simp add:ring_distrib1,
        simp add:ringModule_def, simp add:ring_tOp_assoc,
        simp add:ringModule_def, simp add:rg_l_unit)
done

definition
  dsumMhom :: "['i set, 'i ⇒ ('a, 'r, 'm) Module_scheme, 
    'i ⇒ ('b, 'r, 'm1) Module_scheme, 'i ⇒ ('a ⇒ 'b)] ⇒ ('i ⇒ 'a) ⇒ 
    ('i ⇒ 'b)" where

  "dsumMhom I A B S = (λf∈carr_dsumag I A. (λk∈I. (S k) (f k)))" 

(**     I ⟶ A
          \   |
           \  | S
              B        **)
 

lemma (in Ring) dsumMhom_mem:"⟦∀i∈I. R module M i; ∀i∈I. R module N i;
                ∀i∈I. S i ∈ mHom R (M i) (N i); x ∈ carr_dsumag I M⟧
                 ⟹ dsumMhom I M N S x ∈ carr_dsumag I N"
apply (subst carr_dsumag_def, simp, simp add:finiteHom_def)
apply (rule conjI)
 apply (simp add:dsumMhom_def)
 apply (cut_tac carr_dsum_prod1[of I M],
        drule_tac a = x in forall_spec, assumption) apply (
         subst carr_prodag_def, simp)
   apply (rule conjI,
          rule Pi_I,
          thin_tac "x ∈ carr_dsumag I M", simp,
          simp add:Un_carrier_def,
          drule_tac x = xa in bspec, assumption,
          drule_tac x = xa in bspec, assumption,
          drule_tac x = xa in bspec, assumption,
          simp add:carr_prodag_def, (erule conjE)+,
          drule_tac x = xa in bspec, assumption)

   apply (frule_tac R = R and M = "M xa" and N = "N xa" and f = "S xa" and 
          m = "x xa" in Module.mHom_mem, assumption+, blast)

  apply (rule ballI,
         drule_tac x = i in bspec, assumption,
         drule_tac x = i in bspec, assumption,
         drule_tac x = i in bspec, assumption,
         simp add:carr_prodag_def, (erule conjE)+,
         drule_tac x = i in bspec, assumption)
  apply (simp add:Module.mHom_mem)
   apply (cut_tac carr_dsum_prod1[of I M],
         drule_tac a = x in forall_spec, assumption)

  apply (simp add:dsumMhom_def)
  apply (simp add:carr_prodag_def, (erule conjE)+)
  apply (simp add:carr_dsumag_def, simp add:finiteHom_def)
  apply (erule conjE, erule exE)
  apply (subgoal_tac "∀j∈I - H. S j (x j) = 𝟬⇘N j⇙", blast)
  apply (rule ballI,
         drule_tac x = j in bspec, simp,
         drule_tac x = j in bspec, simp,
         drule_tac x = j in bspec, simp,
         simp add:carr_prodag_def, (erule conjE)+,
         drule_tac x = j in bspec, simp)
  apply (simp add:Module.mHom_0)
done

lemma (in Ring) dsumMhom_mHom:"⟦∀i∈I. (R module (M i)); 
      ∀i∈I. (R module (N i)); ∀i∈I. ((S i) ∈ mHom R (M i) (N i))⟧ ⟹ 
                dsumMhom I M N S ∈ mHom R (dsumM R I M) (dsumM R I N)"
apply (subst mHom_def, simp) 
apply (rule conjI)
 apply (simp add:aHom_def,
        rule conjI,
        simp add:dsumM_def dsumMhom_mem)
apply (rule conjI,
        simp add:dsumMhom_def extensional_def dsumM_def)
apply (rule ballI)+
 apply (simp add:dsumM_def)
 apply (subgoal_tac "∀i∈I. aGroup (M i)",
        frule_tac X = a and Y = b in dsum_pOp_mem [of I M], assumption+,
        frule_tac x = "prod_pOp I M a b" in dsumMhom_mem [of I M N S], 
        assumption+,
        frule_tac x = a in dsumMhom_mem [of I M N S], assumption+,
        frule_tac x = b in dsumMhom_mem [of I M N S], assumption+)
 apply (subgoal_tac "∀i∈I. aGroup (N i)")
 apply (frule_tac X = "dsumMhom I M N S a" and Y = "dsumMhom I M N S b" in 
                                      dsum_pOp_mem [of I N], assumption+)
 apply (rule carr_dsumM_mem_eq [of I N], assumption+, rule ballI) 
 apply (cut_tac carr_dsum_prod1 [of  I M], cut_tac carr_dsum_prod1 [of I N])
 apply (simp add:prod_pOp_def)
 apply (simp add:dsumMhom_def)
 apply (rule_tac R = R and M = "M j" and N = "N j" and m = "a j" and n = "b j"
        in  Module.mHom_add)
  apply simp+
  apply (simp add:carr_dsumag_def carr_prodag_def finiteHom_def,
         simp add:carr_dsumag_def carr_prodag_def finiteHom_def,
         rule ballI, rotate_tac 1,
         drule_tac x = i in bspec, assumption,
         simp add:Module.module_is_ag,
         rule ballI, drule_tac x = i in bspec, assumption, 
         simp add:Module.module_is_ag)
apply (rule ballI)+
 apply (simp add:dsumM_def)
 apply (frule_tac a = a and b = m in dsum_sprod_mem [of I M], assumption+)
 apply (frule_tac x = "prodM_sprod R I M a m" in 
                  dsumMhom_mem [of I M N S], assumption+)
 apply (frule_tac x = m in dsumMhom_mem [of I M N S], assumption+)
 apply (frule_tac a = a and b = "dsumMhom I M N S m" in 
                    dsum_sprod_mem [of I N], assumption+)
 apply (rule carr_dsumM_mem_eq [of I N], assumption+)
 apply (rule ballI)
 apply (cut_tac carr_dsum_prod1 [of I])
 apply (drule_tac a = m in forall_spec, assumption)
        
  apply (cut_tac carr_dsum_prod1 [of I N],
         frule_tac a = "dsumMhom I M N S m" in forall_spec,
         assumption)
 apply (simp add:dsumMhom_def prodM_sprod_def)
  apply (thin_tac "(λj∈I. a ⋅⇩s⇘M j⇙ m j) ∈ carr_dsumag I M",
         thin_tac "(λk∈I. S k (if k ∈ I then a ⋅⇩s⇘M k⇙ m k else undefined))
        ∈ carr_dsumag I N",
         thin_tac "(λk∈I. S k (m k)) ∈ carr_dsumag I N",
         thin_tac "(λj∈I. a ⋅⇩s⇘N j⇙ (if j ∈ I then S j (m j) else undefined))
        ∈ carr_dsumag I N",
         thin_tac "∀x. x ∈ carr_dsumag I N ⟶ x ∈ carr_prodag I N")
  apply (drule_tac x = j in bspec, assumption,
         drule_tac x = j in bspec, assumption,
         drule_tac x = j in bspec, assumption,
         simp add:carr_prodag_def, (erule conjE)+,
         drule_tac x = j in bspec, assumption)
  apply (simp add:Module.mHom_lin)
done

end