diff --git a/IsarMathLib/ROOT b/IsarMathLib/ROOT index e1c60a5..608d257 100644 --- a/IsarMathLib/ROOT +++ b/IsarMathLib/ROOT @@ -51,6 +51,8 @@ session "IsarMathLib" = "ZF" + Ring_ZF_4 Field_ZF Module_ZF + Module_ZF_1 + Module_ZF_2 VectorSpace_ZF OrderedField_ZF Int_ZF_IML diff --git a/docs/IsarMathLib/Module_ZF_1.html b/docs/IsarMathLib/Module_ZF_1.html new file mode 100644 index 0000000..0d73346 --- /dev/null +++ b/docs/IsarMathLib/Module_ZF_1.html @@ -0,0 +1,1578 @@ + + + + + +Theory Module_ZF_1 + + + + +
+

Theory Module_ZF_1

+
+ +
(*
+    This file is a part of IsarMathLib -
+    a library of formalized mathematics written for Isabelle/Isar.
+
+    Copyright (C) 2024  Daniel de la Concepcion Saez
+
+    This program is free software; Redistribution and use in source and binary forms,
+    with or without modification, are permitted provided that the following conditions are met:
+
+   1. Redistributions of source code must retain the above copyright notice,
+   this list of conditions and the following disclaimer.
+   2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation and/or
+   other materials provided with the distribution.
+   3. The name of the author may not be used to endorse or promote products
+   derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
+USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*)
+
+subsection ‹ Linear Combinations on Modules›
+
+theory Module_ZF_1 imports Module_ZF CommutativeSemigroup_ZF
+
+begin
+
+text‹Since modules are abelian groups, we can make use of its commutativity to create new elements
+by adding acted on elements finitely. Consider two ordered collections of ring elements and of
+group elements (indexed by a finite set); then we can add their actions to obtain a new group
+element. This is a linear combination.›
+
+definition(in module0)
+  LinearComb ("∑[_;{_,_}]" 88)
+  where "fR:C→R ⟹ fG:C→ℳ ⟹ D∈FinPow(C) ⟹ LinearComb(D,fR,fG) ≡ if D≠0 then CommSetFold(AM,{⟨m,(fR`m)⋅S (fG`m)⟩. m∈domain(fR)},D)
+    else Θ"
+
+text‹The function that for each index element gives us the acted element of the 
+abelian group is a function from the index to the group.›
+
+lemma(in module0) coordinate_function:
+  assumes "AA:C→R" "B:C→ℳ"
+  shows "{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}:C→ℳ"
+proof-
+  {
+    fix m assume "m∈C"
+    then have p:"AA`m∈R""B`m∈ℳ" using assms(1,2) apply_type by auto
+    from p(1) have "H`(AA`m):ℳ→ℳ" using H_val_type(2) by auto
+    then have "(AA`m)⋅S(B`m)∈ℳ" using p(2) apply_type by auto
+  }
+  then have "{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}⊆C×ℳ" by auto moreover
+  {
+    fix x y assume "⟨x,y⟩∈{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}"
+    then have xx:"x∈C" "y=(AA`x)⋅S (B`x)" by auto
+    {
+      fix y' assume "⟨x,y'⟩∈{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}"
+      then have "y'=(AA`x)⋅S (B`x)" by auto
+      with xx(2) have "y=y'" by auto
+    }
+    then have "∀y'. ⟨x,y'⟩∈{⟨m,(AA`m)⋅S (B`m)⟩. m∈C} ⟶ y=y'" by auto
+  }
+  then have "∀x y. ⟨x,y⟩∈{⟨m,(AA`m)⋅S (B`m)⟩. m∈C} ⟶ (∀y'. ⟨x,y'⟩∈{⟨m,(AA`m)⋅S (B`m)⟩. m∈C} ⟶ y=y')"
+    by auto 
+  moreover have "domain({⟨m,(AA`m)⋅S (B`m)⟩. m∈C})⊆C" unfolding domain_def by auto ultimately
+  show "{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}:C→ℳ" unfolding Pi_def function_def by auto
+qed
+
+text‹A linear combination results in a group element where
+the functions and the sets are well defined.›
+
+theorem(in module0) linComb_is_in_module:
+  assumes "AA:C→R" "B:C→ℳ" "D∈FinPow(C)"
+  shows "(∑[D;{AA,B}])∈ℳ"
+proof-
+  {
+    assume noE:"D≠0"
+    have ffun:"{⟨m,(AA`m)⋅S (B`m)⟩. m∈C}:C→ℳ" using coordinate_function assms by auto
+    note commsemigr.sum_over_set_add_point(1)[OF
+      commsemigr.intro[OF _ _ ffun] assms(3) noE]
+      mod_ab_gr.abelian_group_axioms abelian_group_def
+      group0_def IsAgroup_def IsAmonoid_def abelian_group_axioms_def moreover
+    from assms(1) have "domain(AA)=C" unfolding Pi_def by auto
+    ultimately have ?thesis unfolding LinearComb_def[OF assms(1-3)] using noE by auto
+  }
+  then show ?thesis unfolding LinearComb_def[OF assms(1-3)] 
+    using mod_ab_gr.group0_2_L2 by auto
+qed
+
+text‹A linear combination of one element functions is just the action
+of one element onto another.›
+
+lemma(in module0) linComb_one_element:
+  assumes "x∈X" "AA:X→R" "B:X→ℳ"
+  shows "∑[{x};{AA,B}]=(AA`x)⋅S(B`x)"
+proof-
+  have dom:"domain(AA)=X" using assms(2) func1_1_L1 by auto
+  have fin:"{x}∈FinPow(X)" unfolding FinPow_def using assms(1) by auto
+  have A:"∑[{x};{AA,B}]=CommSetFold(AM,{⟨t,(AA`t)⋅S (B`t)⟩. t∈X},{x})"
+    unfolding LinearComb_def[OF assms(2,3) fin] dom by auto
+  have assoc:"AM{is associative on}ℳ" using mod_ab_gr.abelian_group_axioms
+    unfolding abelian_group_def group0_def IsAgroup_def IsAmonoid_def by auto
+  have comm:"commsemigr(ℳ, AM, X, {⟨t,(AA`t)⋅S (B`t)⟩. t∈X})"
+    unfolding commsemigr_def
+    using mod_ab_gr.abelian_group_axioms 
+    unfolding abelian_group_def abelian_group_axioms_def
+    group0_def IsAgroup_def IsAmonoid_def using coordinate_function[OF assms(2,3)] by auto
+  have sing:"1≈{x}" "|{x}|=1" using singleton_eqpoll_1 eqpoll_sym by auto
+  then obtain b where b:"b∈bij(|{x}|,{x})" "b∈bij(1,{x})" unfolding eqpoll_def by auto then
+  have "∑[{x};{AA,B}]=Fold1(AM,{⟨t,(AA`t)⋅S (B`t)⟩. t∈X} O b)" 
+    using commsemigr.sum_over_set_bij[OF comm fin, of b] trans[OF A] by blast
+  also have "…=({⟨t,(AA`t)⋅S (B`t)⟩. t∈X} O b)`0" using semigr0.prod_of_1elem unfolding semigr0_def using
+    comp_fun[OF _ coordinate_function[OF assms(2,3)], of b 1] b(2) assms(1) func1_1_L1B[of b 1 "{x}" X] assoc unfolding bij_def inj_def by blast
+  also have "…=({⟨t,(AA`t)⋅S (B`t)⟩. t∈X})`(b`0)" using comp_fun_apply b unfolding bij_def inj_def by auto
+  also have "…= {⟨t,(AA`t)⋅S (B`t)⟩. t∈X}`x" using apply_type[of b 1 "λt. {x}" 0] b unfolding bij_def inj_def
+    by auto
+  ultimately show ?thesis using apply_equality[OF _ coordinate_function[OF assms(2,3)]] assms(1) by auto
+qed
+
+text ‹Since a linear combination is a group element, it makes sense to apply the action onto it.
+With this result we simplify it to a linear combination.›
+
+lemma(in module0) linComb_action:
+  assumes "AA:X→R" "B:X→ℳ" "r∈R" "D∈FinPow(X)"
+  shows "r⋅S(∑[D;{AA,B}])=∑[D;{{⟨k,r⋅(AA`k)⟩. k∈X},B}]" 
+    and "{⟨m,r ⋅(AA`m)⟩. m∈X}:X→R"
+proof-
+  show f:"{⟨m,r ⋅(AA`m)⟩. m∈X}:X→R" unfolding Pi_def function_def domain_def
+    using apply_type[OF assms(1)] assms(3) Ring_ZF_1_L4(3) by auto
+  {
+    fix AAt Bt assume as:"AAt:X → R" "Bt:X → ℳ"
+    have "∑[0;{AAt,Bt}]=Θ" using LinearComb_def[OF as] unfolding FinPow_def by auto
+    then have "r ⋅S (∑[0;{AAt,Bt}])=Θ" using assms(3) zero_fixed by auto moreover
+    have mr:"{⟨m,r⋅(AAt`m)⟩. m∈X}:X→R" unfolding Pi_def function_def domain_def
+      using apply_type[OF as(1)] assms(3) Ring_ZF_1_L4(3) by auto
+    then have "∑[0;{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}]=Θ" using LinearComb_def[OF mr as(2)]
+      unfolding FinPow_def by auto
+    ultimately have "r ⋅S (∑[0;{AAt,Bt}]) = ∑[0;{{⟨x, r ⋅(AAt ` x)⟩ . x ∈ X},Bt}]" by auto
+  }
+  then have case0:"(∀AAt∈X → R.
+    ∀Bt∈X → ℳ. r ⋅S (∑[0;{AAt,Bt}]) = ∑[0;{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}])" by auto
+  {
+    fix Tk assume A:"Tk∈FinPow(X)" "Tk≠0"
+    then obtain t where tt:"t∈Tk" by auto
+    {
+      assume "(∀AAk∈X→R. ∀Bk∈X→ℳ. (r⋅S(∑[Tk-{t};{AAk,Bk}])=∑[Tk-{t};{{⟨k,r⋅(AAk`k)⟩. k∈X},Bk}]))"
+      with tt obtain t where t:"t∈Tk" "(∀AAk∈X→R. ∀Bk∈X→ℳ. (r⋅S(∑[Tk-{t};{AAk,Bk}])=∑[Tk-{t};{{⟨k,r⋅(AAk`k)⟩. k∈X},Bk}]))" by auto
+      let ?Tk="Tk-{t}"
+      have CC:"Tk=?Tk∪{t}" using t by auto
+      have DD:"?Tk∈FinPow(X)" using A(1) unfolding FinPow_def using subset_Finite[of ?Tk Tk]
+        by auto
+      have tX:"t∈X" using t(1) A(1) unfolding FinPow_def by auto
+      then have EE:"X-(?Tk)=(X-Tk)∪{t}" using t(1) by auto
+      {
+        assume as:"Tk-{t}≠0"
+        with t have BB:"t∈Tk" "Tk-{t}≠0" "∀AAk∈X→R. ∀Bk∈X→ℳ. (r⋅S(∑[Tk-{t};{AAk,Bk}])=∑[Tk-{t};{{⟨k,r⋅(AAk`k)⟩. k∈X},Bk}])" by auto
+        from BB(3) have A3:"∀AAk∈X→R. ∀Bk∈X→ℳ. (r⋅S(∑[?Tk;{AAk,Bk}])=∑[?Tk;{{⟨k,r⋅(AAk`k)⟩. k∈X},Bk}])" by auto
+        {
+          fix AAt Bt assume B:"AAt:X→R" "Bt:X→ℳ"
+          then have af:"{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X}:X→ℳ" using coordinate_function by auto
+          have comm:"commsemigr(ℳ, AM, X, {⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X})"
+            unfolding commsemigr_def
+            using mod_ab_gr.abelian_group_axioms 
+            unfolding abelian_group_def abelian_group_axioms_def
+            group0_def IsAgroup_def IsAmonoid_def using af by auto
+          then have "CommSetFold(AM,{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X},Tk)=CommSetFold(AM,{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X},?Tk)
+            +V({⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X}`t)" using commsemigr.sum_over_set_add_point(2)[of ℳ AM X "{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X}" "Tk-{t}"] DD BB(2) 
+            A(1-2) EE CC by auto
+          also have "…=CommSetFold(AM,{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X},?Tk)
+            +V((AAt`t)⋅S(Bt`t))" using apply_equality[OF _ af, of t "(AAt`t)⋅S(Bt`t)"] tX by auto
+          ultimately have "CommSetFold(AM,{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X},Tk)=CommSetFold(AM,{⟨k,(AAt`k)⋅S(Bt`k)⟩. k∈X},?Tk)
+            +V((AAt`t)⋅S(Bt`t))" by auto moreover
+          have "domain(AAt)=X" using B(1) Pi_def by auto ultimately
+          have "(∑[Tk;{AAt,Bt}])=(∑[?Tk;{AAt,Bt}])+V((AAt`t)⋅S(Bt`t))" unfolding LinearComb_def[OF B(1,2) A(1)]
+            LinearComb_def[OF B(1,2) DD] using as A(2) by auto
+          then have eq:"r⋅S(∑[Tk;{AAt,Bt}])=r⋅S((∑[?Tk;{AAt,Bt}])+V((AAt`t)⋅S(Bt`t)))" by auto
+          moreover have "∀g∈ℳ. ∀h∈ℳ. (H`r)`(g+Vh)=((H`r)`g)+V((H`r)`h)" 
+            using module_ax1 assms(3) by auto
+          moreover have AR:"AAt`t∈R" using B(1) tX apply_type by auto
+          then have "H`(AAt`t):ℳ→ℳ" using H_val_type(2) by auto
+          from apply_type[OF this] have "(AAt`t)⋅S(Bt`t)∈ℳ" using apply_type[OF B(2)] tX by auto moreover
+          have mr:"{⟨m,r⋅(AAt`m)⟩. m∈X}:X→R" unfolding Pi_def function_def domain_def
+            using apply_type[OF B(1)] assms(3) Ring_ZF_1_L4(3) by auto
+          then have fff:"{⟨m,({⟨m,r⋅(AAt`m)⟩. m∈X}`m)⋅S(Bt`m)⟩. m∈X}:X→ℳ" using coordinate_function[OF mr B(2)] apply_equality[OF _ mr] by auto
+          with tX have pff:"⟨t,({⟨m,r⋅(AAt`m)⟩. m∈X}`t)⋅S(Bt`t)⟩∈{⟨m,({⟨m,r⋅(AAt`m)⟩. m∈X}`m)⋅S(Bt`m)⟩. m∈X}"
+            by auto
+          have dom:"domain({⟨m,(r⋅(AAt`m))⟩. m∈X})=X" by auto
+          have comm2:"commsemigr(ℳ, AM, X, {⟨m, ({⟨x,r ⋅(AAt`x)⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X})"
+            unfolding commsemigr_def
+            using mod_ab_gr.abelian_group_axioms 
+            unfolding abelian_group_def abelian_group_axioms_def
+            group0_def IsAgroup_def IsAmonoid_def using fff by auto
+          have "∑[?Tk;{AAt,Bt}]∈ℳ" using linComb_is_in_module[OF B(1,2) DD].
+          ultimately have "r ⋅S ((∑[?Tk;{AAt,Bt}]) +V ((AAt ` t) ⋅S (Bt ` t)))=(r⋅S(∑[?Tk;{AAt,Bt}]))+V(r⋅S((AAt`t)⋅S(Bt`t)))"
+            by auto
+          also have "…=(r⋅S(∑[?Tk;{AAt,Bt}]))+V((r⋅(AAt`t))⋅S(Bt`t))" using module_ax3
+            assms(3) AR apply_type[OF B(2)] tX by auto
+          also have "…=(∑[?Tk;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}])+V((r⋅(AAt`t))⋅S(Bt`t))"
+            using A3 B(1,2) by auto
+          also have "…=(∑[?Tk;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}])+V(({⟨m, r ⋅ (AAt ` m)⟩ . m ∈ X} `t)⋅S(Bt`t))"
+            using apply_equality[OF _ mr] tX by auto
+          also have "…=(∑[?Tk;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}])+V({⟨m, ({⟨x,(r ⋅(AAt`x))⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X}`t)"
+            using apply_equality[OF pff fff] by auto
+          also have "…=CommSetFold(AM,{⟨m, ({⟨x,r ⋅(AAt`x)⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X},?Tk)+V({⟨m, ({⟨x,(r ⋅(AAt`x))⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X}`t)"
+            unfolding LinearComb_def[OF mr B(2) DD] using dom as by auto
+          also have "…=CommSetFold(AM,{⟨m, ({⟨x,r ⋅(AAt`x)⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X},Tk)" using 
+            commsemigr.sum_over_set_add_point(2)[OF comm2, of "Tk-{t}"] fff DD tX CC BB(2) by auto
+          ultimately have "r ⋅S ((∑[?Tk;{AAt,Bt}]) +V ((AAt ` t) ⋅S (Bt ` t))) =CommSetFold(AM,{⟨m, ({⟨x,r ⋅(AAt`x)⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X},Tk)"
+            by auto
+          with eq have "r ⋅S (∑[Tk;{AAt,Bt}]) =CommSetFold(AM,{⟨m, ({⟨x,r ⋅(AAt`x)⟩. x∈X}`m)⋅S(Bt`m)⟩. m∈X},Tk)" by auto
+          also have "…=∑[Tk;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}]" using A(2) unfolding LinearComb_def[OF mr B(2) A(1)] dom by auto
+          ultimately have "r ⋅S (∑[Tk;{AAt,Bt}]) =∑[Tk;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}]" by auto
+        }
+        then have "∀AA∈X→R. ∀B∈X→ℳ. r ⋅S (∑[Tk;{AA,B}]) =∑[Tk;{{⟨x,r⋅(AA`x)⟩. x∈X},B}]" using BB by auto
+      }
+      moreover
+      {
+        assume "Tk-{t}=0"
+        then have sing:"Tk={t}" using A(2) by auto
+        {
+          fix AAt Bt assume B:"AAt:X→R" "Bt:X→ℳ"
+          have mr:"{⟨m,r⋅(AAt`m)⟩. m∈X}:X→R" unfolding Pi_def function_def domain_def
+            using apply_type[OF B(1)] assms(3) Ring_ZF_1_L4(3) by auto
+          from sing have "∑[Tk;{AAt,Bt}]=(AAt`t)⋅S(Bt`t)" using linComb_one_element[OF tX B]
+            by auto
+          then have "r ⋅S (∑[Tk;{AAt,Bt}])=r ⋅S ((AAt`t)⋅S(Bt`t))" by auto
+          also have "…=(r ⋅ (AAt`t))⋅S(Bt`t)" using module_ax3 assms(3) apply_type[OF B(1) tX]
+            apply_type[OF B(2) tX] by auto
+          also have "…=({⟨m,(r ⋅ (AAt`m))⟩. m∈X}`t)⋅S(Bt`t)" using apply_equality[OF _ mr] tX by auto
+          also have "…=∑[Tk;{{⟨m,(r ⋅ (AAt`m))⟩. m∈X},Bt}]" using sing linComb_one_element[OF tX mr B(2)]
+            by auto
+          ultimately have "r ⋅S (∑[Tk;{AAt,Bt}])=∑[Tk;{{⟨m,(r ⋅ (AAt`m))⟩. m∈X},Bt}]" by auto
+        }
+      }
+      ultimately have " ∀AA∈X → R. ∀B∈X → ℳ. r ⋅S (∑[Tk;{AA,B}]) = ∑[Tk;{{⟨x, r ⋅ (AA ` x)⟩ . x ∈ X},B}]"
+        by auto
+    }
+    with tt have "∃t∈Tk. (∀AAt∈X → R.  ∀Bt∈X → ℳ.
+                      r ⋅S (∑[Tk - {t};{AAt,Bt}]) =
+                      ∑[Tk - {t};{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}]) ⟶
+               (∀AAt∈X → R. ∀Bt∈X → ℳ.
+                      r ⋅S (∑[Tk;{AAt,Bt}]) = ∑[Tk;{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}])" by auto
+  }
+  then have caseStep:"∀A∈FinPow(X). A≠0 ⟶ (∃t∈A. (∀AAt∈X → R.
+                   ∀Bt∈X → ℳ.
+                      r ⋅S (∑[A - {t};{AAt,Bt}]) =
+                      ∑[A - {t};{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}]) ⟶
+               (∀AAt∈X → R.
+                   ∀Bt∈X → ℳ.
+                      r ⋅S (∑[A;{AAt,Bt}]) = ∑[A;{{⟨x, r ⋅ (AAt ` x)⟩ . x ∈ X},Bt}]))" by auto
+  have "∀AAt∈X→R. ∀Bt∈X→ℳ. r ⋅S(∑[D;{AAt,Bt}]) =∑[D;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}]" using
+    FinPow_ind_rem_one[where P="λD. (∀AAt∈X→R. ∀Bt∈X→ℳ. r ⋅S(∑[D;{AAt,Bt}]) =∑[D;{{⟨x,r⋅(AAt`x)⟩. x∈X},Bt}])",
+    OF case0 caseStep] assms(4) by auto
+  with assms(1,2) show "r ⋅S(∑[D;{AA,B}]) =∑[D;{{⟨x,r⋅(AA`x)⟩. x∈X},B}]" by auto
+qed
+
+text‹A linear combination can always be defined on a cardinal.›
+
+lemma(in module0) linComb_reorder_terms1:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "g∈bij(|D|,D)"
+  shows "(∑[D;{AA,B}])=∑[|D|;{AA O g,B O g}]"
+proof-
+  from assms(3,4) have funf:"g:|D|→X" unfolding bij_def inj_def FinPow_def using func1_1_L1B by auto
+  have ABfun:"AA O g:|D|→R" "B O g:|D|→ℳ" using comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)] by auto
+  then have domAg:"domain(AA O g)=|D|" unfolding Pi_def by auto
+  from assms(1) have domA:"domain(AA)=X" unfolding Pi_def by auto
+  have comm:"commsemigr(ℳ, AM, domain(AA), {⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)})"
+    unfolding commsemigr_def using mod_ab_gr.abelian_group_axioms unfolding IsAgroup_def
+    IsAmonoid_def abelian_group_def group0_def abelian_group_axioms_def
+    using coordinate_function[OF assms(1,2)] domA by auto
+  {
+    assume A:"D=0"
+    then have D:"∑[D;{AA,B}]=Θ" using LinearComb_def assms(1-3) by auto moreover
+    from A assms(4) have "|D|=0" unfolding bij_def inj_def Pi_def by auto
+    moreover then have "|D|∈FinPow(|D|)" unfolding FinPow_def by auto moreover
+    note ABfun
+    ultimately have ?thesis using LinearComb_def[of "AA O g" "|D|" "B O g", of "|D|"] by auto
+  }
+  moreover
+  {
+    assume A:"D≠0"
+    then have eqD:"∑[D;{AA,B}]=CommSetFold(AM,{⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)},D)" using LinearComb_def[OF assms(1-3)] by auto
+    have eqD1:"CommSetFold(AM,{⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)},D)=Fold1(AM,{⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)} O g)" 
+      using commsemigr.sum_over_set_bij[OF comm] assms(3) A
+      domA assms(4) by blast
+    {
+      fix n assume n:"n∈|D|"
+      then have T:"({⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)} O g)`n={⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)}`( g`n)"
+        using comp_fun_apply funf unfolding bij_def inj_def by auto
+      have "g`n∈D" using assms(4) unfolding bij_def inj_def using apply_type n by auto
+      then have "g`n∈domain(AA)" using domA assms(3) unfolding FinPow_def by auto
+      then have "{⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)}`( g`n)=(AA`(g`n))⋅S (B`( g`n))" using apply_equality[OF _ coordinate_function[OF assms(1,2)]]
+        domA by auto
+      also have "…=((AA O g)`n)⋅S ((B O g)`n)" using comp_fun_apply funf n by auto
+      also have "…={⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|}`n" using apply_equality[OF _ coordinate_function[OF comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)]]]
+        n by auto
+      ultimately have "({⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)} O g)`n={⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|}`n" using T by auto
+    }
+    then have "∀x∈|D|. ({⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)} O g)`x={⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|}`x" by auto
+    then have eq:"{⟨m,(AA`m)⋅S (B`m)⟩. m∈domain(AA)} O g={⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|}" using func_eq[OF comp_fun[OF funf coordinate_function[OF assms(1) assms(2)]]
+      coordinate_function[OF comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)]]] domA by auto
+    have R1:"∑[D;{AA,B}]=Fold1(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|})"
+      using trans[OF eqD eqD1] subst[OF eq, of "λt. ∑[D;{AA,B}] = Fold1(AM,t)"] by blast
+    from A have Dno:"|D|≠0" using assms(4) unfolding bij_def surj_def by auto
+    have "||D||=|D|" using cardinal_cong assms(4) unfolding eqpoll_def by auto
+    then have idf:"id(|D|)∈bij(||D||,|D|)" using id_bij by auto
+    have comm:"commsemigr(ℳ, AM, |D|, {⟨m, ((AA O g) ` m) ⋅S ((B O g) ` m)⟩ . m ∈ |D|})"
+      unfolding commsemigr_def using mod_ab_gr.abelian_group_axioms
+      unfolding abelian_group_def group0_def IsAgroup_def IsAmonoid_def
+      abelian_group_axioms_def using coordinate_function[OF comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)]]
+      by auto
+    have sub:"{⟨m, ((AA O g) ` m) ⋅S ((B O g) ` m)⟩ . m ∈ |D|} ⊆ |D|×ℳ" using
+      coordinate_function[OF comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)]]
+      unfolding Pi_def by auto
+    have finE:"Finite(|D|)" using assms(4,3) eqpoll_imp_Finite_iff unfolding eqpoll_def FinPow_def by auto
+    then have EFP:"|D|∈FinPow(|D|)" unfolding FinPow_def by auto
+    then have eqE:"∑[|D|;{AA O g,B O g}]=CommSetFold(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈domain(AA O g)},|D|)" using LinearComb_def[OF comp_fun[OF funf assms(1)]
+      comp_fun[OF funf assms(2)]] Dno by auto
+    also have "…=CommSetFold(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|},|D|)" using domAg by auto
+    also have "…=Fold1(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|})" using commsemigr.sum_over_set_bij[OF comm
+      EFP Dno idf]
+      subst[OF right_comp_id[of "{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|}" "|D|" ℳ, OF sub], 
+        of "λt. CommSetFold(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|},|D|) = Fold1(AM,t)"]
+      by blast
+    ultimately have "∑[|D|;{AA O g,B O g}]=Fold1(AM,{⟨m,((AA O g)`m)⋅S ((B O g)`m)⟩. m∈|D|})"
+      by (simp only:trans)
+    with R1 have ?thesis by (simp only:trans sym)
+  }
+  ultimately show ?thesis by blast
+qed
+
+text‹Actually a linear combination can be defined over any
+bijective set with the original set.›
+
+lemma(in module0) linComb_reorder_terms2:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "g∈bij(E,D)"
+  shows "(∑[D;{AA,B}])=∑[E;{AA O g,B O g}]"
+proof-
+  from assms(3,4) have funf:"g:E→X" unfolding bij_def inj_def FinPow_def using func1_1_L1B by auto
+  have ABfun:"AA O g:E→R" "B O g:E→ℳ" using comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)] by auto
+  then have domAg:"domain(AA O g)=E" unfolding Pi_def by auto
+  from assms(1) have domA:"domain(AA)=X" unfolding Pi_def by auto
+  from assms(3-4) have finE:"Finite(E)" unfolding FinPow_def using eqpoll_imp_Finite_iff unfolding eqpoll_def by auto
+  then have "|E|≈E" using well_ord_cardinal_eqpoll Finite_imp_well_ord by blast
+  then obtain h where h:"h∈bij(|E|,E)" unfolding eqpoll_def by auto
+  then have "(g O h)∈bij(|E|,D)" using comp_bij assms(4) by auto moreover
+  have ED:"|E|=|D|" using cardinal_cong assms(4) unfolding eqpoll_def by auto
+  ultimately have "(g O h)∈bij(|D|,D)" by auto
+  then have "(∑[D;{AA,B}])=(∑[|D|;{AA O (g O h),B O (g O h)}])" using linComb_reorder_terms1 assms(1-3) by auto moreover
+  from h have "(∑[E;{AA O g,B O g}])=(∑[|E|;{(AA O g) O h,(B O g) O h}])" using linComb_reorder_terms1 comp_fun[OF funf assms(1)] comp_fun[OF funf assms(2)] 
+    finE unfolding FinPow_def by auto
+  moreover note ED ultimately
+  show ?thesis using comp_assoc by auto
+qed
+
+text‹Restricting the defining functions to the domain set does nothing to
+the linear combination›
+
+corollary(in module0) linComb_restrict_coord:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)"
+  shows "(∑[D;{AA,B}])=∑[D;{restrict(AA,D),restrict(B,D)}]"
+  using linComb_reorder_terms2[OF assms id_bij] right_comp_id_any by auto
+
+text‹A linear combination can by defined with a natural number
+and functions with that number as domain.›
+
+corollary(in module0) linComb_nat:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)"
+  shows "∃n∈nat. ∃A1∈n→R. ∃B1∈n→ℳ. ∑[D;{AA,B}]=∑[n;{A1,B1}] ∧ A1``n=AA``D ∧ B1``n=B``D"
+proof
+  from assms(3) have fin:"Finite(D)" unfolding FinPow_def by auto
+  then obtain n where n:"n∈nat" "D≈n" unfolding Finite_def by auto moreover
+  from fin have "|D|≈D" using well_ord_cardinal_eqpoll Finite_imp_well_ord by blast
+  ultimately have "|D|≈n" "n∈nat" using eqpoll_trans[of "|D|"] by auto
+  then have "n∈nat" "||D||=|n|" using cardinal_cong by auto
+  then have D:"|D|=n" "n∈nat" using Card_cardinal_eq[OF Card_cardinal] Card_cardinal_eq[OF nat_into_Card] by auto
+  then show "|D|∈nat" by auto
+  from n(2) D(1) obtain g where g:"g∈bij(|D|,D)" using eqpoll_sym unfolding eqpoll_def by auto
+  show "∃A1∈|D|→R. ∃B1∈|D|→ℳ. ∑[D;{AA,B}]=∑[|D|;{A1,B1}] ∧ A1``|D|=AA``D ∧ B1``|D|=B``D"
+  proof
+    from g have gX:"g:|D|→X" unfolding bij_def inj_def using assms(3) unfolding FinPow_def using func1_1_L1B by auto
+    then show "(AA O g):|D|→R" using comp_fun assms(1) by auto
+    show "∃B1∈|D|→ℳ. ∑[D;{AA,B}]=∑[|D|;{AA O g,B1}] ∧ (AA O g)``|D|=AA``D ∧ B1``|D|=B``D"
+    proof
+      show "(B O g):|D|→ℳ" using comp_fun assms(2) gX by auto
+      have "∑[D;{AA,B}]=∑[|D|;{AA O g,B O g}]" using g linComb_reorder_terms1 assms func1_1_L1B by auto
+      moreover have "(AA O g)``|D|=AA``(g``|D|)" using image_comp by auto
+      then have "(AA O g)``|D|=AA``D" using g unfolding bij_def using surj_range_image_domain by auto
+      moreover have "(B O g)``|D|=B``(g``|D|)" using image_comp by auto
+      then have "(B O g)``|D|=B``D" using g unfolding bij_def using surj_range_image_domain by auto
+      ultimately show "∑[D;{AA,B}]=∑[|D|;{AA O g,B O g}] ∧ (AA O g)``|D|=AA``D ∧ (B O g)``|D|=B``D" by auto
+    qed
+  qed
+qed
+
+subsubsection‹Adding linear combinations›
+
+text ‹Adding a linear combination defined over $\emptyset$ leaves it as is›
+
+lemma(in module0) linComb_sum_base_induct1:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "AA1:Y→R" "B1:Y→ℳ"
+  shows "(∑[D;{AA,B}])+V(∑[0;{AA1,B1}])=∑[D;{AA,B}]"
+proof-
+  from assms(1-3) have "∑[D;{AA,B}]∈ℳ" using linComb_is_in_module by auto
+  then have eq:"(∑[D;{AA,B}])+VΘ=∑[D;{AA,B}]" using zero_neutral(1)
+    by auto moreover
+  have ff:"0∈FinPow(Y)" unfolding FinPow_def by auto
+  from eq show ?thesis using LinearComb_def[OF assms(4-5) ff] by auto
+qed
+
+text‹Applying a product of $1\times$ to the defining set computes the same linear combination; since they are bijective sets›
+
+lemma(in module0) linComb_sum_base_induct2:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)"
+  shows "(∑[D;{AA,B}])=∑[{0}×D;{{⟨⟨0,x⟩,AA`x⟩. x∈X},{⟨⟨0,x⟩,B`x⟩. x∈X}}]" and
+  "(∑[D;{AA,B}])=∑[{0}×D;{restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D),restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)}]"
+proof-
+  let ?g="{⟨⟨0,d⟩,d⟩. d∈D}"
+  from assms(3) have sub:"D⊆X" unfolding FinPow_def by auto
+  have gfun:"?g:{0}×D→D" unfolding Pi_def function_def by blast
+  then have gfunX:"?g:{0}×D→X" using sub func1_1_L1B by auto
+  from gfun have "?g∈surj({0}×D,D)" unfolding surj_def using apply_equality[OF _ gfun] by blast moreover
+  {
+    fix w y assume "?g`w=?g`y" "w∈{0}×D" "y∈{0}×D"
+    then obtain dw dy where "w=⟨0,dw⟩" "y=⟨0,dy⟩" "?g`w=?g`y" "dw∈D" "dy∈D" by auto
+    then have "dw=dy" "w=⟨0,dw⟩" "y=⟨0,dy⟩" using apply_equality[OF _ gfun, of w dw] apply_equality[OF _ gfun, of y dy] by auto
+    then have "w=y" by auto
+  }
+  then have "?g∈inj({0}×D,D)" unfolding inj_def using gfun by auto ultimately
+  have gbij:"?g∈bij({0}×D,D)" unfolding bij_def by auto
+  with assms have A1:"(∑[D;{AA,B}])=∑[{0}×D;{AA O ?g,B O ?g}]" using linComb_reorder_terms2 by auto
+  from gbij have "Finite({0}×D)" using assms(3) eqpoll_imp_Finite_iff unfolding FinPow_def eqpoll_def by auto
+  then have fin:"{0}×D∈FinPow({0}×X)" unfolding FinPow_def using sub by auto
+  have A0:"{⟨⟨0,x⟩,AA`x⟩. x∈X}:{0}×X→R" unfolding Pi_def function_def using apply_type[OF assms(1)] by auto
+  have B0:"{⟨⟨0,x⟩,B`x⟩. x∈X}:{0}×X→ℳ" unfolding Pi_def function_def using apply_type[OF assms(2)] by auto
+  {
+    fix r assume "r∈{0}×D"
+    then obtain rd where rd:"r=⟨0,rd⟩" "rd∈D" by auto
+    then have "(AA O ?g)`r=AA`rd" using comp_fun_apply gfun apply_equality by auto
+    also have "…={⟨⟨0,x⟩,AA`x⟩. x∈X}`⟨0,rd⟩" using apply_equality[OF _ A0] sub rd(2) by auto
+    also have "…=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`⟨0,rd⟩" using restrict rd(2) by auto
+    ultimately have "(AA O ?g)`r=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`r" using rd(1) by auto
+  }
+  then have "∀r∈{0}×D. (AA O ?g)`r=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`r" by auto moreover
+  have "AA O ?g:{0}×D→R" using gfunX assms(1) comp_fun by auto moreover
+  have "{0}×D⊆{0}×X" using sub by auto
+  then have "restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D):{0}×D→R" using A0 restrict_fun by auto ultimately
+  have f1:"(AA O ?g)=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)" using func_eq[of "AA O ?g" "{0}×D" R "restrict({⟨⟨0, x⟩, AA ` x⟩ . x ∈ X}, {0} × D)"]
+    by auto
+  {
+    fix r assume "r∈{0}×D"
+    then obtain rd where rd:"r=⟨0,rd⟩" "rd∈D" by auto
+    then have "(B O ?g)`r=B`rd" using comp_fun_apply gfun apply_equality by auto
+    also have "…={⟨⟨0,x⟩,B`x⟩. x∈X}`⟨0,rd⟩" using apply_equality[OF _ B0] sub rd(2) by auto
+    also have "…=restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`⟨0,rd⟩" using restrict rd(2) by auto
+    ultimately have "(B O ?g)`r=restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`r" using rd(1) by auto
+  }
+  then have "∀r∈{0}×D. (B O ?g)`r=restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`r" by auto moreover
+  have "B O ?g:{0}×D→ℳ" using gfunX assms(2) comp_fun by auto moreover
+  have "{0}×D⊆{0}×X" using sub by auto
+  then have "restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D):{0}×D→ℳ" using B0 restrict_fun by auto ultimately
+  have "(B O ?g)=restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)" using func_eq[of "B O ?g" "{0}×D" ℳ "restrict({⟨⟨0, x⟩, B ` x⟩ . x ∈ X}, {0} × D)"]
+    by auto
+  with A1 f1 show "(∑[D;{AA,B}])=∑[{0}×D;{restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D),restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)}]" by auto
+  also have "…=∑[{0}×D;{{⟨⟨0,x⟩,AA`x⟩. x∈X},{⟨⟨0,x⟩,B`x⟩. x∈X}}]" using linComb_restrict_coord[OF A0 B0 fin] by auto
+  ultimately show "(∑[D;{AA,B}])=∑[{0}×D;{{⟨⟨0,x⟩,AA`x⟩. x∈X},{⟨⟨0,x⟩,B`x⟩. x∈X}}]" by auto
+qed
+
+text‹Then, we can model adding a liner combination on the empty set
+as a linear combination of the disjoint union of sets›
+
+lemma(in module0) linComb_sum_base_induct:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "AA1:Y→R" "B1:Y→ℳ"
+  shows "(∑[D;{AA,B}])+V(∑[0;{AA1,B1}])=∑[D+0;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]"
+proof-
+  from assms(3) have sub:"D⊆X" unfolding FinPow_def by auto
+  then have sub2:"{0}×D⊆{0}×X" by auto
+  then have sub3:"{0}×D∈Pow(X+Y)" unfolding sum_def by auto
+  let ?g="{⟨⟨0,x⟩,x⟩. x∈D}"
+  have gfun:"?g:{0}×D→D" unfolding Pi_def function_def by blast
+  then have "?g∈surj({0}×D,D)" unfolding surj_def using apply_equality by auto moreover
+  {
+    fix w y assume "?g`w=?g`y" "w∈{0}×D" "y∈{0}×D"
+    then obtain dw dy where "w=⟨0,dw⟩" "y=⟨0,dy⟩" "?g`w=?g`y" "dw∈D" "dy∈D" by auto
+    then have "dw=dy" "w=⟨0,dw⟩" "y=⟨0,dy⟩" using apply_equality[OF _ gfun, of w dw] apply_equality[OF _ gfun, of y dy] by auto
+    then have "w=y" by auto
+  }
+  then have "?g∈inj({0}×D,D)" unfolding inj_def using gfun by auto ultimately
+  have gbij:"?g∈bij({0}×D,D)" unfolding bij_def by auto
+  then have "Finite({0}×D)" using assms(3) eqpoll_imp_Finite_iff unfolding FinPow_def eqpoll_def by auto
+  with sub3 have finpow0D:"{0}×D∈FinPow(X+Y)" unfolding FinPow_def by auto
+  have A0:"{⟨⟨0,x⟩,AA`x⟩. x∈X}:{0}×X→R" unfolding Pi_def function_def using apply_type[OF assms(1)] by auto
+  have A1:"{⟨⟨1,x⟩,AA1`x⟩. x∈Y}:{1}×Y→R" unfolding Pi_def function_def using apply_type[OF assms(4)] by auto
+  have domA0:"domain({⟨⟨0,x⟩,AA`x⟩. x∈X})={0}×X" by auto
+  have domA1:"domain({⟨⟨1,x⟩,AA1`x⟩. x∈Y})={1}×Y" by auto
+  have A:"{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y}:X+Y→R" using fun_disjoint_Un[OF A0 A1] unfolding sum_def by auto
+  have B0:"{⟨⟨0,x⟩,B`x⟩. x∈X}:{0}×X→ℳ" unfolding Pi_def function_def using apply_type[OF assms(2)] by auto
+  have B1:"{⟨⟨1,x⟩,B1`x⟩. x∈Y}:{1}×Y→ℳ" unfolding Pi_def function_def using apply_type[OF assms(5)] by auto
+  then have domB0:"domain({⟨⟨0,x⟩,B`x⟩. x∈X})={0}×X" unfolding Pi_def by auto
+  then have domB1:"domain({⟨⟨1,x⟩,B1`x⟩. x∈Y})={1}×Y" unfolding Pi_def by auto
+  have B:"{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}:X+Y→ℳ" using fun_disjoint_Un[OF B0 B1] unfolding sum_def by auto
+  have "(∑[D;{AA,B}])+V(∑[0;{AA1,B1}])=∑[D;{AA,B}]" using linComb_sum_base_induct1 assms by auto
+  also have "…=∑[{0}×D;{restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D),restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)}]" using linComb_sum_base_induct2(2) assms(1-3) by auto
+  ultimately have eq1:"(∑[D;{AA,B}])+V(∑[0;{AA1,B1}])=∑[{0}×D;{restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D),restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)}]" by auto
+  {
+    fix s assume "s∈{0}×D"
+    then obtain ds where ds:"ds∈D" "s=⟨0,ds⟩" by auto
+    then have "restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`s={⟨⟨0,x⟩,AA`x⟩. x∈X}`s" using restrict by auto
+    also have "…=({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s" using fun_disjoint_apply1 domA1 ds(2) by auto
+    also have "…=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D)`s" using restrict ds by auto
+    ultimately have "restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`s=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D)`s" by auto
+  }
+  then have tot:"∀s∈{0}×D. restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)`s=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D)`s" by auto moreover
+  have f1:"restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D):{0}×D→R" using restrict_fun A0 sub2 by auto moreover
+  have f2:"restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D):{0}×D→R" using restrict_fun[OF fun_disjoint_Un[OF A0 A1]] sub2 by auto
+  ultimately have fA:"restrict({⟨⟨0,x⟩,AA`x⟩. x∈X},{0}×D)=restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D)" using func_eq[OF f1 f2] by auto
+  {
+    fix s assume "s∈{0}×D"
+    then obtain ds where ds:"ds∈D" "s=⟨0,ds⟩" by auto
+    then have "restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`s={⟨⟨0,x⟩,B`x⟩. x∈X}`s" using restrict by auto
+    also have "…=({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s" using fun_disjoint_apply1 domB1 ds(2) by auto
+    also have "…=restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D)`s" using restrict ds by auto
+    ultimately have "restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`s=restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D)`s" by auto
+  }
+  then have tot:"∀s∈{0}×D. restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)`s=restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D)`s" by auto moreover
+  have f1:"restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D):{0}×D→ℳ" using restrict_fun B0 sub2 by auto moreover
+  have f2:"restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D):{0}×D→ℳ" using restrict_fun[OF fun_disjoint_Un[OF B0 B1]] sub2 by auto
+  ultimately have fB:"restrict({⟨⟨0,x⟩,B`x⟩. x∈X},{0}×D)=restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D)" using func_eq[OF f1 f2] by auto
+  with fA eq1 have "(∑[D;{AA,B}])+V(∑[0;{AA1,B1}])=∑[{0}×D;{restrict({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{0}×D),restrict({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y},{0}×D)}]"
+    by auto
+  also have "…=∑[{0}×D;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]" using linComb_restrict_coord[OF A B finpow0D]
+    by auto
+  also have "…=∑[D+0;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]" unfolding sum_def by auto
+  ultimately show ?thesis by auto
+qed
+
+text‹An element of the set for the linear combination
+can be removed and add it using group addition.›
+
+lemma(in module0) sum_one_element:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "t∈D"
+  shows "(∑[D;{AA,B}])=(∑[D-{t};{AA,B}])+V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)"
+proof-
+  from assms(1,2) have af:"{⟨k,(AA`k)⋅S(B`k)⟩. k∈X}:X→ℳ" using coordinate_function by auto  
+  from assms(3) have sub:"D⊆X" unfolding FinPow_def by auto
+  then have tX:"t∈X" using assms(4) by auto
+  have dom:"domain(AA)=X" using assms(1) Pi_def by auto
+  {
+    assume A:"D-{t}=0"
+    with assms(4) have "D={t}" by auto
+    then have "(∑[D;{AA,B}])=∑[{t};{AA,B}]" by auto
+    also have "…=(AA`t)⋅S(B`t)" using linComb_one_element sub assms(1,2,4) by auto
+    also have "…={⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t" using af assms(4) sub apply_equality by auto
+    also have "…=Θ +V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)" using zero_neutral(2)
+      apply_type[OF af] assms(4) sub by auto
+    also have "…=(∑[D-{t};{AA,B}])+V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)" using A LinearComb_def[OF assms(1,2), of "D-{t}"]
+      unfolding FinPow_def by auto
+    ultimately have ?thesis by auto
+  }
+  moreover
+  {
+    assume A:"D-{t}≠0"
+    then have D:"D≠0" by auto
+    have comm:"commsemigr(ℳ, AM, X, {⟨k,(AA`k)⋅S(B`k)⟩. k∈X})"
+      unfolding commsemigr_def using mod_ab_gr.abelian_group_axioms
+      unfolding abelian_group_def abelian_group_axioms_def group0_def
+      IsAgroup_def IsAmonoid_def using af by auto
+    have fin:"D-{t}∈FinPow(X)" using assms(3) unfolding FinPow_def using subset_Finite[of "D-{t}" D] by auto
+    have "(D-{t})∪{t}=D" "X-(D-{t})=(X-D)∪{t}" using assms(4) sub by auto
+    then have "CommSetFold(AM,{⟨k,(AA`k)⋅S(B`k)⟩. k∈X},D)=CommSetFold(AM,{⟨k,(AA`k)⋅S(B`k)⟩. k∈X},D-{t})
+      +V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)" using commsemigr.sum_over_set_add_point(2)[OF comm
+      fin A] by auto
+    also have "…=(∑[D-{t};{AA,B}])+V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)" using LinearComb_def[OF assms(1,2) fin] A
+      dom by auto
+    ultimately have "CommSetFold(AM,{⟨k,(AA`k)⋅S(B`k)⟩. k∈X},D)=(∑[D-{t};{AA,B}])+V({⟨k,(AA`k)⋅S(B`k)⟩. k∈X}`t)" by auto moreover
+    then have ?thesis unfolding LinearComb_def[OF assms(1-3)] using D dom by auto
+  }
+  ultimately show ?thesis by blast
+qed
+
+text ‹A small technical lemma to proof by induction on finite sets that the addition of linear combinations
+is a linear combination›
+
+lemma(in module0) linComb_sum_ind_step:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)" "E∈FinPow(Y)" "AA1:Y→R" "B1:Y→ℳ" "t∈E" "D≠0"
+    "(∑[D;{AA,B}])+V(∑[E-{t};{AA1,B1}])=∑[D+(E-{t});{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]"
+  shows "(∑[D;{AA,B}])+V(∑[E;{AA1,B1}])=∑[D+E;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]"
+proof-
+  have a1f:"{⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}:Y→ℳ" using coordinate_function assms(5,6) by auto
+  with assms(4,7) have p1:"({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t)∈ℳ" unfolding FinPow_def using apply_type by auto
+  have p2:"∑[D;{AA,B}]∈ℳ" using linComb_is_in_module assms(1-3) by auto
+  have "E-{t}∈FinPow(Y)" using assms(4,7) unfolding FinPow_def using subset_Finite[of "E-{t}" E] by auto
+  then have p3:"∑[E-{t};{AA1,B1}]∈ℳ" using linComb_is_in_module assms(5,6) by auto
+  have "∑[E;{AA1,B1}]=(∑[E-{t};{AA1,B1}])+V({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t)" using sum_one_element[OF assms(5,6,4,7)].
+  then have "(∑[D;{AA,B}])+V(∑[E;{AA1,B1}])=(∑[D;{AA,B}])+V((∑[E-{t};{AA1,B1}])+V({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t))" by auto
+  also have "…=((∑[D;{AA,B}])+V(∑[E-{t};{AA1,B1}]))+V({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t)"
+    using p1 p2 p3 mod_ab_gr.group_oper_assoc by auto
+  also have "…=(∑[D+(E-{t});{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}])+V({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t)"
+    using assms(9) by auto
+  ultimately have "(∑[D;{AA,B}])+V(∑[E;{AA1,B1}])=(∑[D+(E-{t});{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}])+V({⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t)" by auto
+  moreover have "{⟨k,(AA1`k)⋅S(B1`k)⟩. k∈Y}`t=(AA1`t)⋅S(B1`t)" using apply_equality[OF _ a1f] assms(7,4) unfolding FinPow_def by auto moreover
+  {
+    have dA:"domain({⟨⟨0,x⟩,AA`x⟩. x∈X})={⟨0,x⟩. x∈X}" unfolding domain_def by auto
+    have dA1:"domain({⟨⟨1,x⟩,AA1`x⟩. x∈Y})={⟨1,x⟩. x∈Y}" unfolding domain_def by auto
+    have "⟨1,t⟩∉domain({⟨⟨0,x⟩,AA`x⟩. x∈X})" by auto
+    then have "({⟨⟨1,x⟩,AA1`x⟩. x∈Y}∪{⟨⟨0,x⟩,AA`x⟩. x∈X})`⟨1,t⟩={⟨⟨1,x⟩,AA1`x⟩. x∈Y}`⟨1,t⟩" using fun_disjoint_apply1[of "⟨1,t⟩" "{⟨⟨0,x⟩,AA`x⟩. x∈X}"] by auto
+    moreover have "{⟨⟨1,x⟩,AA1`x⟩. x∈Y}∪{⟨⟨0,x⟩,AA`x⟩. x∈X}={⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y}" by auto
+    ultimately have "({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,t⟩={⟨⟨1,x⟩,AA1`x⟩. x∈Y}`⟨1,t⟩" by auto moreover
+    have "{⟨⟨1,x⟩,AA1`x⟩. x∈Y}:{1}×Y→R" unfolding Pi_def function_def using apply_type[OF assms(5)] by auto
+    then have "{⟨⟨1,x⟩,AA1`x⟩. x∈Y}`⟨1,t⟩=(AA1`t)" using apply_equality assms(7,4) unfolding FinPow_def by auto
+    ultimately have e1:"({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,t⟩=(AA1`t)" by auto
+    have dB:"domain({⟨⟨0,x⟩,B`x⟩. x∈X})={⟨0,x⟩. x∈X}" unfolding domain_def by auto
+    have dB1:"domain({⟨⟨1,x⟩,B1`x⟩. x∈Y})={⟨1,x⟩. x∈Y}" unfolding domain_def by auto
+    have "⟨1,t⟩∉domain({⟨⟨0,x⟩,B`x⟩. x∈X})" by auto
+    then have "({⟨⟨1,x⟩,B1`x⟩. x∈Y}∪{⟨⟨0,x⟩,B`x⟩. x∈X})`⟨1,t⟩={⟨⟨1,x⟩,B1`x⟩. x∈Y}`⟨1,t⟩" using fun_disjoint_apply1[of "⟨1,t⟩" "{⟨⟨0,x⟩,B`x⟩. x∈X}"] by auto
+    moreover have "{⟨⟨1,x⟩,B1`x⟩. x∈Y}∪{⟨⟨0,x⟩,B`x⟩. x∈X}={⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}" by auto
+    ultimately have "({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,t⟩={⟨⟨1,x⟩,B1`x⟩. x∈Y}`⟨1,t⟩" by auto moreover
+    have "{⟨⟨1,x⟩,B1`x⟩. x∈Y}:{1}×Y→ℳ" unfolding Pi_def function_def using apply_type[OF assms(6)] by auto
+    then have "{⟨⟨1,x⟩,B1`x⟩. x∈Y}`⟨1,t⟩=(B1`t)" using apply_equality assms(7,4) unfolding FinPow_def by auto
+    ultimately have e2:"({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,t⟩=(B1`t)" by auto
+    with e1 have "(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,t⟩)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,t⟩)=(AA1`t)⋅S(B1`t)" by auto
+    moreover have tXY:"⟨1,t⟩∈X+Y" unfolding sum_def using assms(7,4) unfolding FinPow_def by auto
+    {
+      fix s w assume as:"⟨s,w⟩∈{⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}"
+      then have s:"s∈X+Y" and w:"w=(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)" by auto
+      then have ss:"s∈{0}×X ∪ {1}×Y" unfolding sum_def by auto
+      {
+        assume "s∈{0}×X"
+        then obtain r where r:"r∈X" "s=⟨0,r⟩" by auto
+        with s have a:"⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨0,r⟩)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨0,r⟩)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto
+        have "({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨0,r⟩={⟨⟨0,x⟩,AA`x⟩. x∈X}`⟨0,r⟩" using fun_disjoint_apply1[of "⟨0,r⟩"
+          "{⟨⟨1,x⟩,AA1`x⟩. x∈Y}"] by auto
+        also have "…=AA`r" using r(1) apply_equality[of "⟨0,r⟩" "AA`r" "{⟨⟨0,x⟩,AA`x⟩. x∈X}" "{0}×X" "λp. R"] unfolding Pi_def function_def
+          using apply_type[OF assms(1)] by auto
+        ultimately have AAr:"({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨0,r⟩=AA`r" by auto
+        with a have a1:"⟨s,(AA`r)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨0,r⟩)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto
+        have "({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨0,r⟩={⟨⟨0,x⟩,B`x⟩. x∈X}`⟨0,r⟩" using fun_disjoint_apply1[of "⟨0,r⟩"
+          "{⟨⟨1,x⟩,B1`x⟩. x∈Y}"] by auto
+        also have "…=B`r" using r(1) apply_equality[of "⟨0,r⟩" "B`r" "{⟨⟨0,x⟩,B`x⟩. x∈X}" "{0}×X" "λp. ℳ"] unfolding Pi_def function_def
+          using apply_type[OF assms(2)] by auto
+        ultimately have Br:"({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨0,r⟩=B`r" by auto
+        with a1 have "⟨s,(AA`r)⋅S(B`r)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto moreover
+        have "(AA`r)⋅S(B`r)∈ℳ" using apply_type[OF coordinate_function[OF assms(1,2)] r(1)] apply_equality[OF _ coordinate_function[OF assms(1,2)]] r(1) by auto
+        ultimately have "⟨s,(AA`r)⋅S(B`r)⟩∈(X+Y)×ℳ" using s by auto moreover
+        from w r(2) AAr Br have "w=(AA`r)⋅S(B`r)" by auto
+        ultimately have "⟨s,w⟩∈(X+Y)×ℳ" by auto
+      }
+      moreover
+      {
+        assume "s∉{0}×X"
+        with ss have "s∈{1}×Y" by auto
+        then obtain r where r:"r∈Y" "s=⟨1,r⟩" by auto
+        with s have a:"⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,r⟩)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,r⟩)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto
+        have "({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,r⟩={⟨⟨1,x⟩,AA1`x⟩. x∈Y}`⟨1,r⟩" using fun_disjoint_apply2[of "⟨1,r⟩"
+          "{⟨⟨0,x⟩,AA`x⟩. x∈X}"] by auto
+        also have "…=AA1`r" using r(1) apply_equality[of "⟨1,r⟩" "AA1`r" "{⟨⟨1,x⟩,AA1`x⟩. x∈Y}" "{1}×Y" "λp. R"] unfolding Pi_def function_def
+          using apply_type[OF assms(5)] by auto
+        ultimately have AAr:"({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,r⟩=AA1`r" by auto
+        with a have a1:"⟨s,(AA1`r)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,r⟩)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto
+        have "({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,r⟩={⟨⟨1,x⟩,B1`x⟩. x∈Y}`⟨1,r⟩" using fun_disjoint_apply2[of "⟨1,r⟩"
+          "{⟨⟨0,x⟩,B`x⟩. x∈X}"] by auto
+        also have "…=B1`r" using r(1) apply_equality[of "⟨1,r⟩" "B1`r" "{⟨⟨1,x⟩,B1`x⟩. x∈Y}" "{1}×Y" "λp. ℳ"] unfolding Pi_def function_def
+          using apply_type[OF assms(6)] by auto
+        ultimately have Br:"({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,r⟩=B1`r" by auto
+        with a1 have "⟨s,(AA1`r)⋅S(B1`r)⟩∈
+          {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto moreover
+        have "(AA1`r)⋅S(B1`r)∈ℳ" using apply_type[OF coordinate_function[OF assms(5,6)] r(1)] apply_equality[OF _ coordinate_function[OF assms(5,6)]] r(1) by auto
+        ultimately have "⟨s,(AA1`r)⋅S(B1`r)⟩∈(X+Y)×ℳ" using s by auto moreover
+        from w r(2) AAr Br have "w=(AA1`r)⋅S(B1`r)" by auto
+        ultimately have "⟨s,w⟩∈(X+Y)×ℳ" by auto
+      }
+      ultimately have "⟨s,w⟩∈(X+Y)×ℳ" by auto
+    }
+    then have "{⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}⊆(X+Y)×ℳ" by auto
+    then have fun:"{⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}:X+Y→ℳ"
+      unfolding Pi_def function_def by auto
+    from tXY have pp:"⟨⟨1,t⟩,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,t⟩)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,t⟩)⟩∈
+      {⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}" by auto
+    have "{⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}`⟨1,t⟩=
+      (({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`⟨1,t⟩)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`⟨1,t⟩)" using apply_equality[OF pp fun] by auto
+    ultimately have "{⟨s,(({⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y})`s)⋅S(({⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y})`s)⟩. s∈X+Y}`⟨1,t⟩=(AA1`t)⋅S(B1`t)"
+      by auto
+  }
+  ultimately have "(∑[D;{AA,B}]) +V (∑[E;{AA1,B1}]) =
+    (∑[D+(E-{t});{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]) +V
+    (({⟨s, ((({⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y}) ` s) ⋅S (({⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}) ` s))⟩ .
+     s ∈ X + Y}) ` ⟨1, t⟩)" by auto moreover
+  have "D+(E-{t})=(D+E)-{⟨1,t⟩}" unfolding sum_def by auto ultimately
+  have A1:"(∑[D;{AA,B}]) +V (∑[E;{AA1,B1}]) =
+    (∑[(D+E)-{⟨1,t⟩};{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]) +V
+    (({⟨s, ((({⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y}) ` s) ⋅S (({⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}) ` s))⟩ .
+     s ∈ X + Y}) ` ⟨1, t⟩)" by auto
+  have f1:"{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X}:{0}×X→R" using apply_type[OF assms(1)] unfolding Pi_def function_def by auto
+  have f2:"{⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y}:{1}×Y→R" using apply_type[OF assms(5)] unfolding Pi_def function_def by auto
+  have "({0}×X)∩({1}×Y)=0" by auto
+  then have ffA:"({⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y}):X+Y→R" unfolding sum_def using fun_disjoint_Un[OF f1 f2] by auto 
+  have f1:"{⟨⟨0, x⟩, B ` x⟩ . x ∈ X}:{0}×X→ℳ" using apply_type[OF assms(2)] unfolding Pi_def function_def by auto
+  have f2:"{⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}:{1}×Y→ℳ" using apply_type[OF assms(6)] unfolding Pi_def function_def by auto
+  have "({0}×X)∩({1}×Y)=0" by auto
+  then have ffB:"({⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}):X+Y→ℳ" unfolding sum_def using fun_disjoint_Un[OF f1 f2] by auto
+  have "D+E⊆X+Y" using assms(3,4) unfolding FinPow_def sum_def by auto moreover
+  obtain nd ne where "nd∈nat" "D≈nd" "ne∈nat" "E≈ne" using assms(3,4) unfolding FinPow_def Finite_def by auto
+  then have "D+E≈nd+ne" "nd∈nat" "ne∈nat" using sum_eqpoll_cong by auto
+  then have "D+E≈nd #+ ne" using nat_sum_eqpoll_sum eqpoll_trans by auto
+  then have "∃n∈nat. D+E≈n" using add_type by auto
+  then have "Finite(D+E)" unfolding Finite_def by auto
+  ultimately have fin:"D+E∈FinPow(X+Y)" unfolding FinPow_def by auto
+  from assms(7) have "⟨1,t⟩∈D+E" unfolding sum_def by auto
+  with A1 show ?thesis using sum_one_element[OF ffA ffB fin] by auto
+qed
+
+text‹The addition of two linear combinations is a linear combination›
+
+theorem(in module0) linComb_sum:
+  assumes "AA:X→R" "AA1:Y→R" "B:X→ℳ" "B1:Y→ℳ" "D≠0" "D∈FinPow(X)" "E∈FinPow(Y)"
+  shows "(∑[D;{AA,B}])+V(∑[E;{AA1,B1}])=∑[D+E;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]"
+proof-
+  {
+    fix 𝔄 𝔅 𝔄1 𝔅1 assume fun:"𝔄:X→R" "𝔅:X→ℳ" "𝔄1:Y→R" "𝔅1:Y→ℳ"
+    have "((∑[D;{𝔄,𝔅}]) +V(∑[0;{𝔄1,𝔅1}])=∑[D+0;{{⟨⟨0,x⟩,𝔄`x⟩. x∈X}∪{⟨⟨1,x⟩,𝔄1`x⟩. x∈Y},{⟨⟨0,x⟩,𝔅`x⟩. x∈X}∪{⟨⟨1,x⟩,𝔅1`x⟩. x∈Y}}])" using linComb_sum_base_induct[OF fun(1,2) assms(6) fun(3,4)]
+      by auto
+  }
+  then have base:"∀AA∈X → R.
+       ∀B∈X → ℳ.
+          ∀AA1∈Y → R.
+             ∀B1∈Y → ℳ.
+                (∑[D;{AA,B}]) +V (∑[0;{AA1,B1}]) =
+                ∑[D + 0;{{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}}]" by auto
+  {
+    fix ℜ assume R:"ℜ∈FinPow(Y)" "ℜ≠0"
+    then obtain r where r:"r∈ℜ" by auto
+    {
+      fix 𝔄 𝔅 𝔄1 𝔅1 assume fun:"𝔄:X→R" "𝔅:X→ℳ" "𝔄1:Y→R" "𝔅1:Y→ℳ" and 
+        step:"∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. (∑[D;{AA,B}]) +V (∑[ℜ - {r};{AA1,B1}])=(∑[D+(ℜ - {r});{{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}}])"
+      then have "(∑[D;{𝔄,𝔅}]) +V (∑[ℜ;{𝔄1,𝔅1}])=(∑[D+ℜ;{{⟨⟨0, x⟩, 𝔄 ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, 𝔄1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, 𝔅 ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, 𝔅1 ` x⟩ . x ∈ Y}}])" using linComb_sum_ind_step[OF fun(1,2) assms(6) R(1) fun(3,4) r assms(5)]
+        by auto
+    }
+    then have "(∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. (∑[D;{AA,B}]) +V (∑[ℜ - {r};{AA1,B1}])=(∑[D+(ℜ - {r});{{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}}])) ⟶ 
+      (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. ((∑[D;{AA,B}]) +V(∑[ℜ;{AA1,B1}])=∑[D+ℜ;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]))" by auto
+    then have "∃r∈ℜ. (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. (∑[D;{AA,B}]) +V (∑[ℜ - {r};{AA1,B1}])=(∑[D+(ℜ - {r});{{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}}])) ⟶ 
+      (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. ((∑[D;{AA,B}]) +V(∑[ℜ;{AA1,B1}])=∑[D+ℜ;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]))" using r by auto
+  }
+  then have indstep:"∀ℜ∈FinPow(Y). ℜ≠0 ⟶ (∃r∈ℜ. (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. (∑[D;{AA,B}]) +V (∑[ℜ - {r};{AA1,B1}])=(∑[D+(ℜ - {r});{{⟨⟨0, x⟩, AA ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, AA1 ` x⟩ . x ∈ Y},{⟨⟨0, x⟩, B ` x⟩ . x ∈ X} ∪ {⟨⟨1, x⟩, B1 ` x⟩ . x ∈ Y}}])) ⟶ 
+    (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. ((∑[D;{AA,B}]) +V(∑[ℜ;{AA1,B1}])=∑[D+ℜ;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}])))" by auto
+  have "∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. ((∑[D;{AA,B}]) +V(∑[E;{AA1,B1}])=∑[D+E;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}])" 
+    using FinPow_ind_rem_one[where P="λE. (∀AA∈X→R. ∀B∈X→ℳ. ∀AA1∈Y→R. ∀B1∈Y→ℳ. ((∑[D;{AA,B}]) +V(∑[E;{AA1,B1}])=∑[D+E;{{⟨⟨0,x⟩,AA`x⟩. x∈X}∪{⟨⟨1,x⟩,AA1`x⟩. x∈Y},{⟨⟨0,x⟩,B`x⟩. x∈X}∪{⟨⟨1,x⟩,B1`x⟩. x∈Y}}]))",
+    OF base indstep assms(7)].
+  with assms(1-4) show ?thesis by auto
+qed
+
+subsubsection‹Linear dependency›
+
+text ‹Now, we have the conditions to define what linear independence means:›
+
+definition(in module0)
+  LinInde ("_{is linearly independent}" 89)
+  where "𝒯⊆ℳ ⟹ 𝒯{is linearly independent} ≡ (∀X∈nat. ∀AA∈X→R. ∀B∈inj(X,𝒯). ((∑[X;{AA,B}] = Θ ) ) ⟶ (∀m∈X. AA`m=𝟬))"
+
+text‹If a set has the zero element, then it is not linearly independent.›
+
+theorem(in module0) zero_set_dependent:
+  assumes "Θ∈T" "T⊆ℳ" "R≠{𝟬}"
+  shows "¬(T{is linearly independent})"
+proof
+  assume "T{is linearly independent}"
+  then have reg:"∀n∈nat. ∀AA∈n→R. ∀B∈inj(n,T).(∑[n;{AA,B}] =Θ ) ⟶ (∀m∈n. AA`m=𝟬)"
+    unfolding LinInde_def[OF assms(2)] by auto
+  from assms(3) obtain r where r:"r∈R" "r≠𝟬" using Ring_ZF_1_L2(1) by auto
+  let ?A="{⟨0,r⟩}"
+  let ?B="{⟨0,Θ⟩}"
+  have A:"?A:succ(0)→R" using `r∈R` unfolding Pi_def function_def domain_def by auto
+  have B:"?B:succ(0)→T" using assms(1) unfolding Pi_def function_def domain_def by auto
+  with assms(2) have B2:"?B:succ(0)→ℳ" unfolding Pi_def by auto
+  have C:"succ(0)∈nat" by auto
+  have fff:"{⟨m, (?A ` m) ⋅S (?B ` m)⟩ . m ∈ 1}:1→ℳ" using coordinate_function[OF A B2] by auto
+  have "?B∈inj(succ(0),T)" unfolding inj_def using apply_equality B by auto
+  with A C reg have "∑[succ(0);{?A,?B}] =Θ ⟶ (∀m∈succ(0). ?A`m=𝟬)" by blast
+  then have "∑[succ(0);{?A,?B}] =Θ ⟶ (?A`0=𝟬)" by blast
+  then have "∑[succ(0);{?A,?B}] =Θ ⟶ (r=𝟬)" using apply_equality[OF _ A,of 0 r] by auto
+  with r(2) have "∑[succ(0);{?A,?B}] ≠Θ" by auto
+  moreover have "∑[succ(0);{?A,?B}]=(?A`0) ⋅S (?B ` 0)" using linComb_one_element[OF _ A B2] unfolding succ_def by auto
+  also have "…=r⋅SΘ" using apply_equality A B by auto
+  also have "…=Θ" using zero_fixed r(1) by auto
+  ultimately show False by auto
+qed
+
+subsection‹Submodule›
+
+text‹A submodule is a subgroup that is invariant by the action›
+
+definition(in module0)
+  IsAsubmodule
+  where "IsAsubmodule(𝒩) ≡ (∀r∈R. ∀h∈𝒩. r⋅S h∈𝒩) ∧ IsAsubgroup(𝒩,AM)"
+
+lemma(in module0) sumodule_is_subgroup:
+  assumes "IsAsubmodule(𝒩)"
+  shows "IsAsubgroup(𝒩,AM)"
+  using assms unfolding IsAsubmodule_def by auto
+
+lemma(in module0) sumodule_is_subaction:
+  assumes "IsAsubmodule(𝒩)" "r∈R" "h∈𝒩"
+  shows "r⋅S h∈𝒩"
+  using assms unfolding IsAsubmodule_def by auto
+
+text‹For groups, we need to prove that the inverse function
+is closed in a set to prove that set to be a subgroup. In module, that is not necessary.›
+
+lemma(in module0) inverse_in_set:
+  assumes "∀r∈R. ∀h∈𝒩. r⋅S h∈𝒩" "𝒩⊆ℳ"
+  shows "∀h∈𝒩. (─h)∈𝒩"
+proof
+  fix h assume "h∈𝒩" moreover
+  then have "h∈ℳ" using assms(2) by auto
+  then have "(\<rm>𝟭)⋅S h=(─h)" using inv_module by auto moreover
+  have "(\<rm>𝟭)∈R" using Ring_ZF_1_L2(2) Ring_ZF_1_L3(1) by auto ultimately
+  show "(─h)∈𝒩" using assms(1) by force
+qed
+
+corollary(in module0) submoduleI:
+  assumes "𝒩⊆ℳ" "𝒩≠0" "𝒩{is closed under}AM"  "∀r∈R. ∀h∈𝒩. r⋅S h∈𝒩"
+  shows "IsAsubmodule(𝒩)" unfolding IsAsubmodule_def
+  using inverse_in_set[OF assms(4,1)] assms mod_ab_gr.group0_3_T3
+    by auto
+
+text‹Every module has at least two submodules: the whole module and the trivial module.›
+
+corollary(in module0) trivial_submodules:
+  shows "IsAsubmodule(ℳ)" and "IsAsubmodule({Θ})"
+  unfolding IsAsubmodule_def
+proof(safe)
+  have "AM:ℳ×ℳ→ℳ" using mod_ab_gr.group_oper_fun by auto
+  then have "AM⊆((ℳ×ℳ)×ℳ)" unfolding Pi_def by auto
+  then have "restrict(AM,ℳ×ℳ)=AM" unfolding restrict_def by blast
+  then show "IsAsubgroup(ℳ,AM)" using mAbGr unfolding IsAsubgroup_def by auto
+next
+  fix r h assume A:"r∈R" "h∈ℳ"
+  from A(1) have "H`r:ℳ→ℳ" using H_val_type(2) by auto
+  with A(2) show "r⋅Sh∈ℳ" using apply_type[of "H`r" ℳ "λt. ℳ"] by auto
+next
+  fix r assume "r∈R"
+  with zero_fixed show "r ⋅S Θ = Θ" by auto
+next
+  have "{Θ}≠0" by auto moreover
+  have "{Θ}⊆ℳ" using mod_ab_gr.group0_2_L2 by auto moreover
+  {
+    fix x y assume "x∈{Θ}" "y∈{Θ}"
+    then have "AM`⟨x,y⟩=Θ" using mod_ab_gr.group0_2_L2 by auto
+  }
+  then have "{Θ}{is closed under}AM" unfolding IsOpClosed_def by auto moreover
+  {
+    fix x assume "x∈{Θ}"
+    then have "GroupInv(ℳ, AM) `(x)= Θ" using mod_ab_gr.group_inv_of_one by auto
+  }
+  then have "∀x∈{Θ}. GroupInv(ℳ, AM) `(x)∈{Θ}" by auto ultimately
+  show "IsAsubgroup({Θ},AM)" using mod_ab_gr.group0_3_T3 by auto
+qed
+
+text‹The restriction of the action is an action.›
+
+lemma(in module0) action_submodule:
+  assumes "IsAsubmodule(𝒩)"
+  shows "{⟨r,restrict(H`r,𝒩)⟩. r∈R}:R→End(𝒩,restrict(AM,𝒩×𝒩))"
+proof-
+  have sub:"𝒩⊆ℳ" using mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms]] by auto
+  {
+    fix t assume "t∈{⟨r,restrict(H`r,𝒩)⟩. r∈R}"
+    then obtain r where t:"r∈R" "t=⟨r,restrict(H`r,𝒩)⟩" by auto
+    then have E:"H`r∈End(ℳ,AM)" using H_val_type(1) by auto
+    from t(1) have "H`r:ℳ→ℳ" using H_val_type(2) by auto
+    then have "restrict(H`r,𝒩):𝒩→ℳ" using restrict_fun sub by auto moreover
+    have "∀h∈𝒩. restrict(H`r,𝒩)`h∈𝒩" using restrict sumodule_is_subaction[OF assms `r∈R`] by auto
+    ultimately have HH:"restrict(H`r,𝒩):𝒩→𝒩" using func1_1_L1A by auto
+    {
+      fix g1 g2 assume H:"g1∈𝒩""g2∈𝒩"
+      with sub have G:"g1∈ℳ""g2∈ℳ" by auto
+      from H have AA:"AM`⟨g1,g2⟩=restrict(AM,𝒩×𝒩)`⟨g1,g2⟩" using restrict by auto
+      then have "(H`r)`(AM`⟨g1,g2⟩)=(H`r)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩)" by auto
+      then have "AM`⟨(H`r)`g1,(H`r)`g2⟩=(H`r)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩)" using E G
+        unfolding End_def Homomor_def IsMorphism_def by auto
+      with H have "restrict(AM,𝒩×𝒩)`⟨(H`r)`g1,(H`r)`g2⟩=(H`r)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩)" using sumodule_is_subaction[OF assms `r∈R`]
+        by auto moreover
+      from H have "AM`⟨g1,g2⟩∈𝒩" using sumodule_is_subgroup[OF assms] mod_ab_gr.group0_3_L6 by auto
+      then have "restrict(H`r,𝒩)`(AM`⟨g1,g2⟩)=(H`r)`(AM`⟨g1,g2⟩)" by auto
+      with AA have "restrict(H`r,𝒩)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩)=(H`r)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩)" by auto moreover
+      from H have "(H`r)`g1=restrict(H`r,𝒩)`g1""(H`r)`g2=restrict(H`r,𝒩)`g2" by auto ultimately
+      have "restrict(H`r,𝒩)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩) = restrict(AM,𝒩×𝒩)`⟨restrict(H`r,𝒩)`g1,restrict(H`r,𝒩)`g2⟩" by auto
+    }
+    then have "∀g1∈𝒩. ∀g2∈𝒩. restrict(H`r,𝒩)`(restrict(AM,𝒩×𝒩)`⟨g1,g2⟩) = restrict(AM,𝒩×𝒩)`⟨restrict(H`r,𝒩)`g1,restrict(H`r,𝒩)`g2⟩" by auto
+    then have "Homomor(restrict(H`r,𝒩),𝒩,restrict(AM,𝒩×𝒩),𝒩,restrict(AM,𝒩×𝒩))" using HH
+      unfolding Homomor_def IsMorphism_def by auto
+    with HH have "restrict(H`r,𝒩)∈End(𝒩,restrict(AM,𝒩×𝒩))" unfolding End_def by auto
+    then have "t∈R×End(𝒩,restrict(AM,𝒩×𝒩))" using t by auto
+  }
+  then have "{⟨r,restrict(H`r,𝒩)⟩. r∈R}⊆R×End(𝒩,restrict(AM,𝒩×𝒩))" by auto moreover
+  {
+    fix x y assume "⟨x,y⟩∈{⟨r,restrict(H`r,𝒩)⟩. r∈R}"
+    then have y:"x∈R""y=restrict(H`x,𝒩)" by auto
+    {
+      fix y' assume "⟨x,y'⟩∈{⟨r,restrict(H`r,𝒩)⟩. r∈R}"
+      then have "y'=restrict(H`x,𝒩)" by auto
+      with y(2) have "y=y'" by auto
+    }
+    then have "∀y'. ⟨x,y'⟩∈{⟨r,restrict(H`r,𝒩)⟩. r∈R} ⟶ y=y'" by auto
+  }
+  then have "∀x y. ⟨x,y⟩∈{⟨r,restrict(H`r,𝒩)⟩. r∈R} ⟶ (∀y'. ⟨x,y'⟩∈{⟨r,restrict(H`r,𝒩)⟩. r∈R} ⟶ y=y')" by auto
+  moreover
+  have "domain({⟨r,restrict(H`r,𝒩)⟩. r∈R})⊆R" unfolding domain_def by auto
+  ultimately show fun:"{⟨r,restrict(H`r,𝒩)⟩. r∈R}:R→End(𝒩,restrict(AM,𝒩×𝒩))" unfolding Pi_def function_def by auto
+qed
+
+text‹A submodule is a module with the restricted action.›
+
+corollary(in module0) submodule: 
+  assumes "IsAsubmodule(𝒩)"
+  shows "IsLeftModule(R,A,M,𝒩,restrict(AM,𝒩×𝒩),{⟨r,restrict(H`r,𝒩)⟩. r∈R})"
+  unfolding IsLeftModule_def IsAction_def ringHomomor_def IsMorphism_def
+proof(safe)
+  show "IsAring(R, A, M)" using ringAssum by auto
+  show g:"IsAgroup(𝒩, restrict(AM,𝒩×𝒩))" using sumodule_is_subgroup assms unfolding IsAsubgroup_def
+    by auto
+  have sub:"𝒩⊆ℳ" using mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms]] by auto
+  then show "restrict(AM,𝒩×𝒩) {is commutative on} 𝒩" using mAbGr
+    using func_ZF_4_L1[OF mod_ab_gr.group_oper_fun] by auto
+  show fun:"{⟨r,restrict(H`r,𝒩)⟩. r∈R}:R→End(𝒩,restrict(AM, 𝒩 × 𝒩))" using action_submodule assms by auto
+  then have Q:"{⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭=restrict(H`𝟭,𝒩)" using apply_equality Ring_ZF_1_L2(2)
+    by auto
+  then have "∀h∈𝒩. ({⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭)`h=restrict(H`𝟭,𝒩)`h" by auto
+  then have "∀h∈𝒩. ({⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭)`h=(H`𝟭)`h" using restrict by auto
+  then have "∀h∈𝒩. ({⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭)`h=h" using module_ax4
+    sub by auto
+  then have "∀h∈𝒩. ({⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭)`h=id(𝒩)`h" by auto moreover
+  have "id(𝒩):𝒩→𝒩" using id_inj unfolding inj_def by auto moreover
+  from Q have "{⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭:𝒩→ℳ" using restrict_fun[OF H_val_type(2)[OF Ring_ZF_1_L2(2)] sub]
+    by auto
+  ultimately have "{⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭=id(𝒩)" using fun_extension[of "{⟨r,restrict(H`r,𝒩)⟩. r∈R}`𝟭" 𝒩 "λ_. ℳ" "id(𝒩)"] by auto
+  also have "…=TheNeutralElement(End(𝒩, restrict(AM, 𝒩 × 𝒩)), restrict(Composition(𝒩), End(𝒩, restrict(AM, 𝒩 × 𝒩)) × End(𝒩, restrict(AM, 𝒩 × 𝒩))))" 
+    using group0.end_comp_monoid(2) sumodule_is_subgroup[OF assms] unfolding group0_def IsAsubgroup_def
+    by auto
+  ultimately show "{⟨r,restrict(H`r,𝒩)⟩. r∈R}`TheNeutralElement(R, M)=TheNeutralElement(End(𝒩, restrict(AM, 𝒩 × 𝒩)),   EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)))"
+    unfolding EndMult_def  by auto
+  fix r s assume AS:"r∈R""s∈R"
+  then have END:"restrict(H ` r, 𝒩)∈End(𝒩,restrict(AM, 𝒩 × 𝒩))""restrict(H ` s, 𝒩)∈End(𝒩,restrict(AM, 𝒩 × 𝒩))" using apply_type[OF fun]
+    apply_equality[OF _ fun] by auto
+  then have funf:"restrict(H ` r, 𝒩):𝒩→𝒩""restrict(H ` s, 𝒩):𝒩→𝒩" unfolding End_def by auto
+  from AS have rs:"r\<ra>s∈R""r⋅s∈R" using Ring_ZF_1_L4(1,3) by auto
+  then have EE:"{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (r\<ra>s)=restrict(H ` (r\<ra>s), 𝒩)" using apply_equality fun by auto
+  have m:"monoid0(𝒩,restrict(AM, 𝒩 × 𝒩))" unfolding monoid0_def
+    using g unfolding IsAgroup_def by auto
+  have f1:"{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (r\<ra>s):𝒩→𝒩" using apply_type[OF fun rs(1)] unfolding End_def by auto
+  have f:"(restrict(AM, 𝒩 × 𝒩) {lifted to function space over} 𝒩) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩:𝒩→𝒩" using monoid0.Group_ZF_2_1_L0[OF m _ funf]
+          AS apply_equality[OF _ fun] by auto
+  from END have "⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩ ∈ End(𝒩, restrict(AM, 𝒩 × 𝒩)) × End(𝒩, restrict(AM, 𝒩 × 𝒩))"
+       using apply_equality[OF _ fun] AS by auto
+  from apply_type[OF restrict_fun[OF monoid0.Group_ZF_2_1_L0A[OF m, of "restrict(AM,𝒩×𝒩) {lifted to function space over}𝒩" 𝒩], of "End(𝒩,restrict(AM, 𝒩 × 𝒩))×End(𝒩,restrict(AM, 𝒩 × 𝒩))"] this] 
+     have f2:"(EndAdd(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩):𝒩→𝒩"
+      unfolding EndAdd_def End_def by blast
+  {
+    fix g assume gh:"g∈𝒩"
+    have A:"((restrict(AM, 𝒩 × 𝒩)  {lifted to function space over} 𝒩) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=((restrict(AM, 𝒩 × 𝒩) {lifted to function space over} 𝒩) `
+          ⟨restrict(H ` r, 𝒩), restrict(H ` s, 𝒩)⟩)`g" using apply_equality[OF _ fun] AS by auto
+    from END have "⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩ ∈ End(𝒩, restrict(AM, 𝒩 × 𝒩)) × End(𝒩, restrict(AM, 𝒩 × 𝒩))"
+       using apply_equality[OF _ fun] AS by auto
+     with A have "(EndAdd(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=((restrict(AM, 𝒩 × 𝒩) {lifted to function space over} 𝒩) `
+          ⟨restrict(H ` r, 𝒩), restrict(H ` s, 𝒩)⟩)`g" unfolding EndAdd_def 
+       using restrict[of "(restrict(AM, 𝒩 × 𝒩)  {lifted to function space over} 𝒩)" "End(𝒩,restrict(AM, 𝒩 × 𝒩))×End(𝒩,restrict(AM, 𝒩 × 𝒩))" "⟨restrict(H ` r, 𝒩), restrict(H ` s, 𝒩)⟩"]
+      by auto
+    also have "…=restrict(AM,𝒩 × 𝒩)`⟨restrict(H ` r, 𝒩)`g, restrict(H ` s, 𝒩)`g⟩" using group0.Group_ZF_2_1_L3[OF _ _ funf gh] g
+      unfolding group0_def by auto
+    also have "…=AM`⟨restrict(H ` r, 𝒩)`g, restrict(H ` s, 𝒩)`g⟩" using apply_type[OF funf(1) gh] apply_type[OF funf(2) gh]
+      by auto
+    also have "…=AM`⟨(H ` r)`g, (H ` s)`g⟩" using gh by auto
+    also have "…=(H`(r\<ra>s))`g" using module_ax2 AS gh sub by auto
+    also have "…=restrict(H`(r\<ra>s),𝒩)`g" using gh by auto  
+    also have "…=({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (r\<ra>s))`g" using EE by auto
+    ultimately have "(EndAdd(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (r\<ra>s))`g" by auto
+  }
+  then have "∀g∈𝒩. (EndAdd(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (r\<ra>s))`g" by auto
+  then show "{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (A ` ⟨r, s⟩) =
+          EndAdd(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩" using fun_extension[OF f1 f2] by auto
+  have f1:"({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} `(r⋅s)):𝒩→𝒩" using apply_type[OF fun rs(2)] unfolding End_def by auto
+  have ff1:"{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r:𝒩→𝒩""{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s:𝒩→𝒩" using apply_type[OF fun] AS unfolding End_def by auto
+  then have "({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r)O({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s):𝒩→𝒩" using comp_fun by auto
+  then have f:"(Composition(𝒩) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩):𝒩→𝒩" using func_ZF_5_L2
+    [OF ff1] using EndMult_def by auto
+  from END have "⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩ ∈ End(𝒩, restrict(AM, 𝒩 × 𝒩)) × End(𝒩, restrict(AM, 𝒩 × 𝒩))"
+       using apply_equality[OF _ fun] AS by auto
+  from apply_type[OF restrict_fun[OF func_ZF_5_L1[of 𝒩], of "End(𝒩,restrict(AM, 𝒩 × 𝒩))×End(𝒩,restrict(AM, 𝒩 × 𝒩))"] this] 
+     have f2:"(EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)) `
+          ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩):𝒩→𝒩"
+      unfolding EndMult_def End_def by blast
+  {
+    fix g assume gh:"g∈𝒩"
+    have A:"(Composition(𝒩) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=
+      (Composition(𝒩) ` ⟨restrict(H ` r, 𝒩), restrict(H ` s,𝒩)⟩)`g" using apply_equality[OF _ fun] AS by auto
+    from END have "⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩ ∈ End(𝒩, restrict(AM, 𝒩 × 𝒩)) × End(𝒩, restrict(AM, 𝒩 × 𝒩))"
+       using apply_equality[OF _ fun] AS by auto
+     with A have "(EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g=
+      (Composition(𝒩) ` ⟨restrict(H ` r, 𝒩), restrict(H ` s,𝒩)⟩)`g" 
+       using restrict unfolding EndMult_def by auto
+    also have "…=(restrict(H ` r, 𝒩)O restrict(H ` s,𝒩))`g" using func_ZF_5_L2[OF funf] by auto
+    also have "…=restrict(H ` r, 𝒩)`( restrict(H` s,𝒩)`g)" using comp_fun_apply[OF funf(2) gh] by auto
+    also have "…=(H ` r)`((H ` s)`g)" using gh apply_type[OF funf(2) gh] by auto
+    also have "…=(H`(r⋅s))`g" using module_ax3 gh sub AS by auto
+    also have "…=restrict(H ` (r⋅s), 𝒩)`g" using gh by auto
+    also have "…=({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} `(r⋅s))`g" using apply_equality[OF _ fun] rs(2) by auto
+    ultimately have "({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} `(r⋅s))`g =(EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g"
+      by auto
+  }
+  then have "∀g∈𝒩. ({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} `(r⋅s))`g =(EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩)`g" by auto
+  then show "{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (M ` ⟨r, s⟩) =
+           EndMult(𝒩, restrict(AM, 𝒩 × 𝒩)) ` ⟨{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` r, {⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` s⟩" using fun_extension[OF f1 f2] by auto
+qed
+
+text‹If we consider linear combinations of elements in a submodule, then
+the linear combination is also in the submodule.›
+
+lemma(in module0) linear_comb_submod:
+  assumes "IsAsubmodule(𝒩)" "D∈FinPow(X)" "AA:X→R" "B:X→𝒩"
+  shows "∑[D;{AA,B}]∈𝒩"
+proof-
+  have fun:"AM:ℳ×ℳ→ℳ" using mod_ab_gr.group_oper_fun.
+  from assms(4) have BB:"B:X→ℳ" using mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms(1)]] func1_1_L1B by auto
+  {
+    fix A1 B1 assume fun:"A1:X→R" "B1:X→𝒩"
+    from fun(2) have fun2:"B1:X→ℳ" using mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms(1)]] func1_1_L1B by auto
+    have "0∈FinPow(X)" unfolding FinPow_def by auto
+    then have "∑[0;{A1,B1}]=Θ" using LinearComb_def[OF fun(1) fun2] by auto
+    then have "∑[0;{A1,B1}]∈𝒩" using assms(1) mod_ab_gr.group0_3_L5 unfolding IsAsubmodule_def by auto
+  }
+  then have base:"∀A1∈X→R. ∀B1∈X→𝒩. ∑[0;{A1,B1}]∈𝒩" by auto
+  {
+    fix RR assume a:"RR≠0" "RR∈FinPow(X)"
+    then obtain d where d:"d∈RR" by auto
+    {
+      fix A1 B1 assume fun:"A1:X→R" "B1:X→𝒩" and step:"∀A1∈X→R. ∀B1∈X→𝒩. ∑[RR-{d};{A1,B1}]∈𝒩"
+      have F:"{⟨m, ({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (A1 ` m)) ` (B1 ` m)⟩ . m ∈ X} : X → 𝒩" using module0.coordinate_function[OF _ fun]
+        submodule[OF assms(1)] unfolding module0_def IsLeftModule_def ring0_def module0_axioms_def by auto
+      {
+        fix m assume mx:"m∈X"
+        then have bh:"B1`m∈𝒩" using fun(2) apply_type by auto
+        from mx have ar:"A1`m∈R" using fun(1) apply_type by auto
+        then have A:"{⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R}`(A1`m)=restrict(H ` (A1`m), 𝒩)" using apply_equality action_submodule[OF assms(1)]
+          by auto
+        have B:"(restrict(H ` (A1`m), 𝒩)) ` (B1 ` m)=(H ` (A1`m))`(B1 ` m)"  using bh restrict by auto
+        with A have "({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (A1 ` m)) ` (B1 ` m)=(H ` (A1`m))`(B1 ` m)" by auto
+      }
+      then have eq1:"{⟨m, ({⟨r, restrict(H ` r, 𝒩)⟩ . r ∈ R} ` (A1 ` m)) ` (B1 ` m)⟩ . m ∈ X} ={⟨m, (H ` (A1`m))`(B1 ` m)⟩ . m ∈ X} " by auto
+      then have pd:"{⟨m, (H ` (A1`m))`(B1 ` m)⟩ . m ∈ X}`d∈𝒩" using d apply_type[OF F] a(2) unfolding FinPow_def by auto
+      from fun(2) have fun2:"B1:X→ℳ" using mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms(1)]] func1_1_L1B by auto
+      have "∑[RR;{A1,B1}]=(∑[RR-{d};{A1,B1}])+V({⟨k, (A1 ` k) ⋅S (B1 ` k)⟩ . k ∈ X} ` d)" using sum_one_element[OF fun(1) fun2 a(2) d].
+      also have "…∈𝒩" using pd step fun mod_ab_gr.group0_3_L6[OF sumodule_is_subgroup[OF assms(1)]] by auto
+      ultimately have "∑[RR;{A1,B1}]∈𝒩" by auto
+    }
+    then have "(∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR-{d};{AA1,BB1}]∈𝒩)⟶(∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR;{AA1,BB1}]∈𝒩)" by auto
+    with d have "∃d∈RR. ((∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR-{d};{AA1,BB1}]∈𝒩)⟶(∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR;{AA1,BB1}]∈𝒩))" by auto
+  }
+  then have step:"∀RR∈FinPow(X). RR≠0 ⟶ (∃d∈RR. ((∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR-{d};{AA1,BB1}]∈𝒩)⟶(∀AA1∈X→R. ∀BB1∈X→𝒩. ∑[RR;{AA1,BB1}]∈𝒩)))" by auto
+  show ?thesis using FinPow_ind_rem_one[OF base step] assms(2-4) by auto
+qed
+
+subsubsection‹Spans›
+
+text‹Since we know linear combinations, we can define the span of a subset
+of a module as the linear combinations of elements in that subset. We have already
+proven that the sum can be done only over finite numbers considering a bijection
+between a finite number and the original finite set, and that the function can be
+restricted to that finite number.›
+
+text‹The terms of a linear combination can be reordered so 
+that they are indexed by the elements of the module.›
+
+lemma(in module0) index_module:
+  assumes "AAA:X→R" "BB:X→ℳ" "D∈FinPow(X)"
+  shows "∃AA∈ℳ→R. ∑[D;{AAA,BB}]=∑[BB``D;{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``D. AA`x=𝟬)"
+proof-
+  let ?F="{⟨d,CommSetFold(A,AAA,D∩(BB-``({BB`d})))⟩. d∈D}"
+  let ?f1="{⟨d,D∩(BB-``({BB`d}))⟩. d∈D}"
+  have "?f1:D→{D∩(BB-``({BB`d})). d∈D}" unfolding Pi_def function_def by auto
+  then have "RepFun(D,λt. ?f1`t)={D∩(BB-``({BB`d})). d∈D}" using apply_equality by auto
+  with assms(3) have "Finite({D∩(BB-``({BB`d})). d∈D})" using Finite_RepFun unfolding FinPow_def by auto
+  then obtain n where "{D∩(BB-``({BB`d})). d∈D}≈n" and n:"n∈nat" unfolding Finite_def by auto
+  then have n2:"{D∩(BB-``({BB`d})). d∈D}≲n" using eqpoll_imp_lepoll by auto
+  {
+    fix T assume "T∈{D∩(BB-``({BB`d})). d∈D}"
+    then obtain d where d:"d∈D" "T=D∩(BB-``({BB`d}))" by auto
+    {
+      assume "d∉T"
+      with d have "d∉(BB-``({BB`d}))" by auto
+      then have "⟨d,BB`d⟩∉BB" using vimage_iff by auto
+      with d(1) assms(2,3) have "False" unfolding FinPow_def Pi_def using function_apply_Pair[of BB d] by auto
+    }
+    then have "T≠0" by auto
+  }
+  then have n3:"∀t∈{D∩(BB-``({BB`d})). d∈D}. id({D∩(BB-``({BB`d})). d∈D}) ` t ≠ 0" using id_def by auto
+  from n have "∀M N. M ≲ n ∧ (∀t∈M. N ` t ≠ 0) ⟶ (∃f. f ∈ Pi(M,λt. N ` t) ∧ (∀t∈M. f ` t ∈ N ` t))" using finite_choice[of n] unfolding AxiomCardinalChoiceGen_def
+    by auto
+  with n2 have "∀N. (∀t∈{D∩(BB-``({BB`d})). d∈D}. N ` t ≠ 0) ⟶ (∃f. f ∈ Pi({D∩(BB-``({BB`d})). d∈D},λt. N ` t) ∧ (∀t∈{D∩(BB-``({BB`d})). d∈D}. f ` t ∈ N ` t))"
+    by blast
+  with n3 have "∃f. f ∈ Pi({D∩(BB-``({BB`d})). d∈D},λt. id({D∩(BB-``({BB`d})). d∈D}) ` t) ∧ (∀t∈{D∩(BB-``({BB`d})). d∈D}. f ` t ∈ id({D∩(BB-``({BB`d})). d∈D}) ` t)"
+    by auto
+  then obtain ff where ff:"ff∈Pi({D∩(BB-``({BB`d})). d∈D},λt. id({D∩(BB-``({BB`d})). d∈D}) ` t)" "(∀t∈{D∩(BB-``({BB`d})). d∈D}. ff ` t ∈ id({D∩(BB-``({BB`d})). d∈D}) ` t)" by force
+  {
+    fix t assume as:"t∈{D∩(BB-``({BB`d})). d∈D}"
+    with ff(2) have "ff`t∈id({D∩(BB-``({BB`d})). d∈D}) ` t" by blast
+    with as have "ff`t∈t" using id_def by auto
+  }
+  then have ff2:"∀t∈{D∩(BB-``({BB`d})). d∈D}. ff ` t ∈t" by auto
+  have "∀x∈{D∩(BB-``({BB`d})). d∈D}. id({D∩(BB-``({BB`d})). d∈D})`x=x" using id_def by auto
+  with ff(1) have ff1:"ff∈Pi({D∩(BB-``({BB`d})). d∈D},λt. t)" unfolding Pi_def Sigma_def by auto
+  have case0:"∃AA∈ℳ→R. ∑[0;{AAA,BB}]=∑[BB``0;{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``0. AA`x=𝟬)"
+    proof
+      have "∑[0;{AAA,BB}]=Θ" using LinearComb_def[OF assms(1,2)] unfolding FinPow_def by auto moreover
+      let ?A="ConstantFunction(ℳ,𝟬)"
+      have "∑[0;{?A,id(ℳ)}]=Θ" using LinearComb_def[OF func1_3_L1[OF Ring_ZF_1_L2(1)], of "id(ℳ)" ℳ 0]
+        unfolding id_def FinPow_def by auto moreover
+      have "BB``0=0" by auto ultimately
+      show "∑[0;{AAA,BB}]=∑[BB``0;{?A,id(ℳ)}] ∧ (∀x∈ℳ-BB``0. ?A`x=𝟬)" using func1_3_L2 by auto
+      then show "?A:ℳ→R" using func1_3_L1[OF Ring_ZF_1_L2(1), of ℳ] by auto
+    qed
+  {
+    fix E assume E:"E∈FinPow(X)" "E≠0"
+    {
+      fix d assume d:"d∈E"
+      {
+        assume hyp:"∃AA∈ℳ→R. ∑[E-{d};{AAA,BB}]=∑[BB``(E-{d});{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``(E-{d}). AA`x=𝟬)"
+        from hyp obtain AA where AA:"AA∈ℳ→R" "∑[E-{d};{AAA,BB}]=∑[BB``(E-{d});{AA,id(ℳ)}]" "∀x∈ℳ-BB``(E-{d}). AA`x=𝟬" by auto
+        have "∑[E;{AAA,BB}] = (∑[E-{d};{AAA,BB}])+V({⟨e,(AAA`e)⋅S(BB`e)⟩. e∈X}`d)" using sum_one_element[OF assms(1,2) E(1) d].
+        with AA(2) also have "…=(∑[BB``(E-{d});{AA,id(ℳ)}])+V((AAA`d)⋅S(BB`d))" using d E(1) unfolding FinPow_def using apply_equality[OF _
+          coordinate_function[OF assms(1,2)]] by auto
+        ultimately have eq:"∑[E;{AAA,BB}] =(∑[BB``(E-{d});{AA,id(ℳ)}])+V((AAA`d)⋅S(BB`d))" by auto
+        have btype:"BB`d∈ℳ" using apply_type assms(2) d E(1) unfolding FinPow_def by auto
+        have "(E-{d})∈FinPow(X)" using E(1) unfolding FinPow_def using subset_Finite[of "E-{d}" E] by auto moreover
+        then have "{BB`x. x∈E-{d}}=BB``(E-{d})" using func_imagedef[OF assms(2), of "E-{d}"] unfolding FinPow_def
+          by auto
+        ultimately have fin:"Finite(BB``(E-{d}))" using Finite_RepFun[of "E-{d}" "λt. BB`t"] unfolding FinPow_def by auto
+        then have "Finite(BB``(E-{d})∪{BB`d})" using Finite_cons[of "BB``(E-{d})" "BB`d"] by auto
+        with btype have finpow:"BB``(E-{d})∪{BB`d}∈FinPow(ℳ)" using func1_1_L6(2)[OF assms(2)] unfolding FinPow_def by auto
+        {
+          assume as:"BB`d∉BB``(E-{d})"
+          then have T_def:"BB``(E-{d})=(BB``(E-{d})∪{BB`d})-{BB`d}" by auto
+          from as have sub:"BB``(E-{d})⊆ℳ-{BB`d}" using func1_1_L6(2)[OF assms(2)] by auto
+          let ?A="restrict(AA,ℳ-{BB`d})∪ConstantFunction({BB`d},AAA`d)"
+          have res:"restrict(AA,ℳ-{BB`d}):ℳ-{BB`d}→R" using restrict_fun[OF AA(1)] by auto
+          moreover have "AAA`d∈R" using apply_type assms(1) d E(1) unfolding FinPow_def by auto
+          then have con:"ConstantFunction({BB`d},AAA`d):{BB`d}→R" using func1_3_L1 by auto
+          moreover have "(G-{BB`d})∩{BB`d}=0" by auto moreover
+          have "R∪R=R" by auto moreover
+          have "(ℳ-{BB`d})∪{BB`d}=ℳ" using apply_type[OF assms(2)] d E(1) unfolding FinPow_def by auto ultimately
+          have A_fun:"?A:ℳ→R" using fun_disjoint_Un[of "restrict(AA,ℳ-{BB`d})" "ℳ-{BB`d}" R "ConstantFunction({BB`d},AAA`d)" "{BB`d}" R] by auto
+          have "?A`(BB`d)=ConstantFunction({BB`d},AAA`d)`(BB`d)" using as fun_disjoint_apply2 by auto moreover note btype
+          ultimately have A_app:"?A`(BB`d)=AAA`d" using as func1_3_L2 by auto
+          {
+            fix z assume "z∈restrict(?A,BB``(E-{d}))"
+            then have z:"z∈?A" "∃x∈BB `` (E - {d}). ∃y. z = ⟨x, y⟩" using restrict_iff by auto
+            then have "∃x∈BB `` (E - {d}). ∃y. z = ⟨x, y⟩" "z∈ConstantFunction({BB`d},AAA`d) ∨ z∈restrict(AA,ℳ-{BB`d})" by auto
+            then have "∃x∈BB `` (E - {d}). ∃y. z = ⟨x, y⟩" "z∈{BB`d}×{AAA`d} ∨ z∈restrict(AA,ℳ-{BB`d})" using ConstantFunction_def by auto
+            then have "fst(z)∈BB `` (E - {d})" "z=⟨BB`d,AAA`d⟩ ∨ z∈restrict(AA,ℳ-{BB`d})"  by auto
+            with as have "z∈restrict(AA,ℳ-{BB`d})" by auto
+            with z(2) have "z∈AA" "∃x∈BB `` (E - {d}). ∃y. z = ⟨x, y⟩" using restrict_iff by auto
+            then have "z∈restrict(AA,BB``(E-{d}))" using restrict_iff by auto
+          }
+          then have "restrict(?A,BB``(E-{d}))⊆restrict(AA,BB``(E-{d}))" by auto moreover
+          {
+            fix z assume z:"z∈restrict(AA,BB``(E-{d}))" "z∉restrict(?A,BB``(E-{d}))"
+            then have disj:"z∉?A ∨ (∀x∈BB``(E-{d}). ∀y. z ≠ ⟨x, y⟩)" using restrict_iff[of z ?A "BB``(E-{d})"] by auto moreover
+            with z(1) have z:"z∈AA" "∃x∈BB``(E-{d}). ∃y. z=⟨x, y⟩" using restrict_iff[of _ AA "BB``(E-{d})"] by auto moreover
+            from z(2) sub have "∃x∈ℳ-{BB`d}. ∃y. z=⟨x, y⟩" by auto
+            with z(1) have "z∈restrict(AA,ℳ-{BB`d})" using restrict_iff by auto
+            then have "z∈?A" by auto
+            with disj have "∀x∈BB``(E-{d}). ∀y. z ≠ ⟨x, y⟩" by auto
+            with z(2) have "False" by auto
+          }
+          then have "restrict(AA,BB``(E-{d}))⊆restrict(?A,BB``(E-{d}))" by auto ultimately
+          have resA:"restrict(AA,BB``(E-{d}))=restrict(?A,BB``(E-{d}))" by auto
+          have "∑[BB``(E-{d});{AA,id(ℳ)}]=∑[BB``(E-{d});{restrict(AA,BB``(E-{d})),restrict(id(ℳ), BB``(E-{d}))}]" using linComb_restrict_coord[OF AA(1) id_type, of "BB``(E-{d})"]
+            fin func1_1_L6(2)[OF assms(2)] unfolding FinPow_def by auto
+          also have "…=∑[BB``(E-{d});{restrict(?A,BB``(E-{d})),restrict(id(ℳ), BB``(E-{d}))}]" using resA by auto
+          also have "…=∑[BB``(E-{d});{?A,id(ℳ)}]" using linComb_restrict_coord[OF A_fun id_type, of "BB``(E-{d})"] fin func1_1_L6(2)[OF assms(2)] unfolding FinPow_def by auto
+          ultimately have "∑[BB``(E-{d});{AA,id(ℳ)}]=∑[(BB``(E-{d})∪{BB`d})-{BB`d};{?A,id(ℳ)}]" using T_def by auto
+          then have "(∑[BB``(E-{d});{AA,id(ℳ)}])+V((AAA`d)⋅S(BB`d))=(∑[(BB``(E-{d})∪{BB`d})-{BB`d};{?A,id(ℳ)}])+V((?A`(BB`d))⋅S(BB`d))" using A_app by auto
+          also have "…=(∑[(BB``(E-{d})∪{BB`d})-{BB`d};{?A,id(ℳ)}])+V((?A`(BB`d))⋅S(id(ℳ)`(BB`d)))" using id_conv[OF btype] by auto
+          also have "…=(∑[(BB``(E-{d})∪{BB`d})-{BB`d};{?A,id(ℳ)}])+V({⟨g,(?A`g)⋅S(id(ℳ)`g)⟩. g∈ℳ}`(BB`d))" using apply_equality[OF _ coordinate_function[OF A_fun id_type]
+            ,of "BB`d" "(?A`(BB`d))⋅S(id(ℳ)`(BB`d))"] btype by auto
+          also have "…=(∑[(BB``(E-{d})∪{BB`d});{?A,id(ℳ)}])" using sum_one_element[OF A_fun id_type finpow, of "BB`d"] by auto
+          ultimately have "(∑[BB``(E-{d});{AA,id(ℳ)}])+V((AAA`d)⋅S(BB`d))=∑[(BB``(E-{d})∪{BB`d});{?A,id(ℳ)}]" by auto
+          with eq have eq:"∑[E;{AAA,BB}] =∑[(BB``(E-{d})∪{BB`d});{?A,id(ℳ)}]" by auto
+          have "BB``(E-{d})∪{BB`d}={BB`x. x∈E-{d}}∪{BB`d}" using func_imagedef[OF assms(2), of "E-{d}"]
+            E(1) unfolding FinPow_def by force
+          also have "…={BB`x. x∈E}" using d by auto ultimately
+          have set:"BB``(E-{d})∪{BB`d}=BB``E" using func_imagedef[OF assms(2), of "E"] E(1) unfolding FinPow_def by auto
+          {
+            fix x assume x:"x∈ℳ-BB``E"
+            then have x1:"x≠BB`d" using d func_imagedef[OF assms(2), of E] E(1) unfolding FinPow_def by auto
+            then have "?A`x=restrict(AA,ℳ-{BB`d})`x" using fun_disjoint_apply1[of x "ConstantFunction({BB`d},AAA`d)"] unfolding
+              ConstantFunction_def by blast
+            with x x1 have "?A`x=AA`x" using restrict by auto moreover
+            from x set have "x∈ℳ-BB``(E-{d})" by auto ultimately
+            have "?A`x=𝟬" using AA(3) by auto
+          }
+          with set eq A_fun have "∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``E;{AA,id(ℳ)}] ∧ (∀x∈ℳ-(BB``E). AA`x=𝟬)" by auto
+        }
+        moreover
+        {
+          assume as:"BB`d∈BB``(E-{d})"
+          then have "BB``(E-{d})∪{BB`d}=BB``(E-{d})" by auto
+          then have finpow:"BB``(E-{d})∈FinPow(ℳ)" using finpow by auto
+          have sub:"E-{d}⊆X" using E(1) unfolding FinPow_def by force
+          with as have "BB`d∈{BB`f. f∈E-{d}}" using func_imagedef[OF assms(2), of "E-{d}"] by auto
+          then have "{BB`f. f∈E-{d}}={BB`f. f∈E}" by auto
+          then have im_eq:"BB``(E-{d})=BB``E" using func_imagedef[OF assms(2),of "E-{d}"] func_imagedef[OF assms(2),of E] sub E(1) unfolding FinPow_def
+            by auto
+          from as have "∑[BB``(E-{d});{AA,id(ℳ)}]=(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V({⟨g,(AA`g)⋅S(id(ℳ)`g)⟩. g∈ℳ}`(BB`d))" using sum_one_element[OF AA(1) id_type]
+            finpow by auto
+          also have "…=(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V((AA`(BB`d))⋅S(id(ℳ)`(BB`d)))" using apply_equality[OF _ coordinate_function[OF AA(1) id_type]]
+            btype by auto
+          also have "…=(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V((AA`(BB`d))⋅S(BB`d))" using id_conv btype by auto
+          ultimately have "∑[BB``(E-{d});{AA,id(ℳ)}]=(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V((AA`(BB`d))⋅S(BB`d))" by auto
+          then have "∑[E;{AAA,BB}] =((∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V((AA`(BB`d))⋅S(BB`d)))+V((AAA ` d)⋅S (BB ` d))" using eq by auto
+          moreover have "∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}]∈ℳ" using linComb_is_in_module[OF AA(1) id_type, of "BB``(E-{d})-{BB`d}"] finpow subset_Finite[of "BB``(E-{d})-{BB`d}" "BB``(E-{d})"] unfolding FinPow_def
+            by auto moreover
+          have "(AA`(BB`d))⋅S(BB`d)∈ℳ" using apply_type[OF AA(1) btype] apply_type[OF H_val_type(2)]
+            btype by auto  moreover
+          have "(AAA`d)⋅S(BB`d)∈ℳ" using apply_type apply_type[OF assms(1), of d] apply_type[OF H_val_type(2)]
+             btype d E(1) unfolding FinPow_def by auto ultimately
+          have "∑[E;{AAA,BB}] =(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V(((AA`(BB`d))⋅S(BB`d))+V((AAA ` d) ⋅S (BB ` d)))" 
+            using mod_ab_gr.group_oper_assoc by auto moreover
+          have "((AA`(BB`d))⋅S(BB`d))+V((AAA ` d) ⋅S (BB ` d))=((AA`(BB`d))\<ra>(AAA ` d))⋅S(BB`d)" using btype apply_type[OF assms(1), of d]
+            apply_type[OF AA(1) btype] d E(1) module_ax2 unfolding FinPow_def by auto
+          ultimately have eq:"∑[E;{AAA,BB}] =(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V(((AA`(BB`d))\<ra>(AAA ` d))⋅S(BB`d))" by auto
+          let ?A="restrict(AA,ℳ-{BB`d})∪ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d))"
+          have "(ℳ-{BB`d})∩({BB`d})=0" by auto moreover
+          have "(ℳ-{BB`d})∪({BB`d})=ℳ" using finpow as unfolding FinPow_def by auto moreover
+          have "restrict(AA,ℳ-{BB`d}):(ℳ-{BB`d})→R" using restrict_fun[OF AA(1), of "ℳ-{BB`d}"] finpow unfolding FinPow_def by auto moreover
+          have "AAA`d∈R" "AA`(BB`d)∈R" using apply_type assms(1) AA(1) btype d E(1) unfolding FinPow_def by auto
+          then have "(AA`(BB`d))\<ra>(AAA ` d)∈R" using Ring_ZF_1_L4(1) by auto
+          then have "ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d)):{BB`d}→R" using func1_3_L1 by auto
+          ultimately have A_fun:"?A:ℳ→R" using fun_disjoint_Un[of "restrict(AA,ℳ-{BB`d})" "ℳ-{BB`d}" R "ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d))" "{BB`d}" R] by auto
+          have "?A`(BB`d)=ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d))`(BB`d)" using as fun_disjoint_apply2 by auto moreover note btype
+          ultimately have A_app:"?A`(BB`d)=(AA`(BB`d))\<ra>(AAA ` d)" using as func1_3_L2 by auto
+          {
+            fix z assume "z∈restrict(?A,BB``(E-{d})-{BB`d})"
+            then have z:"∃x∈BB``(E-{d})-{BB`d}. ∃y. z=⟨x,y⟩" "z∈?A" using restrict_iff by auto
+            then have "∃x∈BB `` (E - {d})-{BB`d}. ∃y. z = ⟨x, y⟩" "z∈ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d)) ∨ z∈restrict(AA,ℳ-{BB`d})" by auto
+            then have "∃x∈BB `` (E - {d})-{BB`d}. ∃y. z = ⟨x, y⟩" "z∈{BB`d}×{(AA`(BB`d))\<ra>(AAA ` d)} ∨ z∈restrict(AA,ℳ-{BB`d})" using ConstantFunction_def by auto
+            then have "fst(z)∈BB `` (E - {d})-{BB`d}" "z=⟨BB`d,AAA`d⟩ ∨ z∈restrict(AA,ℳ-{BB`d})"  by auto
+            then have "z∈restrict(AA,ℳ-{BB`d})" by auto
+            with z(1) have "z∈AA" "∃x∈BB `` (E - {d})-{BB`d}. ∃y. z = ⟨x, y⟩" using restrict_iff by auto
+            then have "z∈restrict(AA,BB``(E-{d})-{BB`d})" using restrict_iff by auto
+          }
+          then have "restrict(?A,BB``(E-{d})-{BB`d})⊆restrict(AA,BB``(E-{d})-{BB`d})" by auto moreover
+          {
+            fix z assume z:"z∈restrict(AA,BB``(E-{d})-{BB`d})" "z∉restrict(?A,BB``(E-{d})-{BB`d})"
+            then have disj:"z∉?A ∨ (∀x∈BB``(E-{d})-{BB`d}. ∀y. z ≠ ⟨x, y⟩)" using restrict_iff[of z ?A "BB``(E-{d})-{BB`d}"] by auto moreover
+            with z(1) have z:"z∈AA" "∃x∈BB``(E-{d})-{BB`d}. ∃y. z=⟨x, y⟩" using restrict_iff[of _ AA "BB``(E-{d})-{BB`d}"] by auto moreover
+            from z(2) func1_1_L6(2)[OF assms(2)] have "∃x∈ℳ-{BB`d}. ∃y. z=⟨x, y⟩" by auto
+            with z(1) have "z∈restrict(AA,ℳ-{BB`d})" using restrict_iff by auto
+            then have "z∈?A" by auto
+            with disj have "∀x∈BB``(E-{d})-{BB`d}. ∀y. z ≠ ⟨x, y⟩" by auto
+            with z(2) have "False" by auto
+          }
+          then have "restrict(AA,BB``(E-{d})-{BB`d})⊆restrict(?A,BB``(E-{d})-{BB`d})" by auto ultimately
+          have resA:"restrict(AA,BB``(E-{d})-{BB`d})=restrict(?A,BB``(E-{d})-{BB`d})" by auto
+          have "Finite(BB``(E-{d})-{BB`d})" using finpow unfolding FinPow_def using subset_Finite[of "BB``(E-{d}) -{BB`d}"] by auto
+          with finpow have finpow2:"BB``(E-{d})-{BB`d}∈FinPow(ℳ)" unfolding FinPow_def by auto
+          have "∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}]=∑[BB``(E-{d})-{BB`d};{restrict(AA,BB``(E-{d})-{BB`d}),restrict(id(ℳ), BB``(E-{d})-{BB`d})}]" using linComb_restrict_coord[OF AA(1) id_type finpow2]
+            by auto
+          also have "…=∑[BB``(E-{d})-{BB`d};{restrict(?A,BB``(E-{d})-{BB`d}),restrict(id(ℳ), BB``(E-{d})-{BB`d})}]" using resA by auto
+          also have "…=∑[BB``(E-{d})-{BB`d};{?A,id(ℳ)}]" using linComb_restrict_coord[OF A_fun id_type finpow2] by auto
+          ultimately have "∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}]=∑[BB``(E-{d})-{BB`d};{?A,id(ℳ)}]" by auto
+          then have "(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V(((AA`(BB`d))\<ra>(AAA ` d))⋅S(BB`d))=(∑[BB``(E-{d})-{BB`d};{?A,id(ℳ)}])+V((?A`(BB`d))⋅S(BB`d))" using A_app by auto
+          also have "…=(∑[BB``(E-{d})-{BB`d};{?A,id(ℳ)}])+V((?A`(BB`d))⋅S(id(ℳ)`(BB`d)))" using id_conv[OF btype] by auto
+          also have "…=(∑[BB``(E-{d})-{BB`d};{?A,id(ℳ)}])+V({⟨g,(?A`g)⋅S(id(ℳ)`g)⟩. g∈ℳ}`(BB`d))" using apply_equality[OF _ coordinate_function[OF A_fun id_type]
+            ,of "BB`d" "(?A`(BB`d))⋅S(id(ℳ)`(BB`d))"] btype by auto
+          also have "…=(∑[BB``(E-{d});{?A,id(ℳ)}])" using sum_one_element[OF A_fun id_type finpow as] by auto
+          ultimately have "(∑[BB``(E-{d})-{BB`d};{AA,id(ℳ)}])+V(((AA`(BB`d))\<ra>(AAA ` d))⋅S(BB`d))=(∑[BB``(E-{d});{?A,id(ℳ)}])" by auto
+          with eq have sol:"∑[E;{AAA,BB}] =∑[BB``(E-{d});{?A,id(ℳ)}]" by auto
+          {
+            fix x assume x:"x∈ℳ-BB``E"
+            with as have x1:"x∈ℳ-{BB`d}" by auto
+            then have "?A`x=restrict(AA,ℳ-{BB`d})`x" using fun_disjoint_apply1[of x "ConstantFunction({BB`d},(AA`(BB`d))\<ra>(AAA ` d))"]
+              unfolding ConstantFunction_def by blast
+            with x1 have "?A`x=AA`x" using restrict by auto
+            with x im_eq have "?A`x=𝟬" using AA(3) by auto
+          }
+          with sol A_fun im_eq have "∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``(E);{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``E. AA`x=𝟬)" by auto
+        }
+        ultimately have "∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``E;{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``E. AA`x=𝟬)" by auto
+      }
+      then have "( ∃AA∈ℳ→R. (∑[E-{d};{AAA,BB}])=(∑[BB``(E-{d});{AA,id(ℳ)}]) ∧ (∀x∈ℳ-BB``(E-{d}). AA`x=𝟬)) ⟶ (∃AA∈ℳ→R. (∑[E;{AAA,BB}])=(∑[BB``E;{AA,id(ℳ)}]) ∧ (∀x∈ℳ-BB``E. AA`x=𝟬))" by auto
+    }
+    then have "∃d∈E. (( ∃AA∈ℳ→R. ∑[E-{d};{AAA,BB}]=∑[BB``(E-{d});{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``(E-{d}). AA`x=𝟬)) ⟶ (∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``(E);{AA,id(ℳ)}] ∧ (∀x∈ℳ-BB``E. AA`x=𝟬)))"
+      using E(2) by auto
+  }
+  then have "∀E∈FinPow(X). E≠0 ⟶ (∃d∈E. ((∃AA∈ℳ→R. ∑[E-{d};{AAA,BB}]=∑[BB``(E-{d});{AA,id(ℳ)}]∧ (∀x∈ℳ-BB``(E-{d}). AA`x=𝟬)) ⟶ (∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``(E);{AA,id(ℳ)}]∧ (∀x∈ℳ-BB``E. AA`x=𝟬))))"
+    by auto
+  then show ?thesis using FinPow_ind_rem_one[where ?P="λE. ∃AA∈ℳ→R. ∑[E;{AAA,BB}]=∑[BB``E;{AA,id(ℳ)}]∧ (∀x∈ℳ-BB``E. AA`x=𝟬)", OF case0 _ assms(3)] by auto
+qed
+
+text‹A span over a set is the collection over all linear combinations on those elements.›
+
+definition(in module0)
+  Span("{span of}_")
+  where "T⊆ℳ ⟹ {span of}T ≡ if T=0 then {Θ} else {∑[F;{AA,id(T)}]. ⟨F,AA⟩∈{⟨FF,B⟩∈FinPow(T)×(T→R). ∀m∈T-FF. B`m=𝟬}}"
+
+text‹The span of a subset is then a submodule and contains the original set.›
+
+theorem(in module0) linear_ind_set_comb_submodule:
+  assumes "T⊆ℳ"
+  shows "IsAsubmodule({span of}T)"
+  and "T⊆{span of}T"
+proof-
+  have "id(T):T→T" unfolding id_def by auto
+  then have idG:"id(T):T→ℳ" using assms func1_1_L1B by auto
+  {
+    assume A:"T=0"
+    from A assms have eq:"({span of}T)={Θ}" using Span_def by auto
+    have "∀r∈R. r⋅SΘ=Θ" using zero_fixed by auto
+    with eq have "∀r∈R. ∀g∈({span of}T). r⋅Sg∈({span of}T)" by auto moreover
+    from eq have "IsAsubgroup(({span of}T),AM)" using mod_ab_gr.trivial_normal_subgroup
+      unfolding IsAnormalSubgroup_def by auto
+    ultimately have "IsAsubmodule({span of}T)" unfolding IsAsubmodule_def by auto
+    with A have "IsAsubmodule({span of}T)" "T⊆{span of}T" by auto
+  }
+  moreover
+  {
+    assume A:"T≠0"
+    {
+      fix t assume asT:"t∈T"
+      then have "Finite({t})" by auto
+      with asT have FP:"{t}∈FinPow(T)" unfolding FinPow_def by auto moreover
+      from asT have Af:"{⟨t,𝟭⟩}∪{⟨r,𝟬⟩. r∈T-{t}}:T→R" unfolding Pi_def function_def using
+        Ring_ZF_1_L2(1,2) by auto moreover
+      {
+        fix m assume "m∈T-{t}"
+        with Af have "({⟨t,𝟭⟩}∪{⟨r,𝟬⟩. r∈T-{t}})`m=𝟬" using apply_equality by auto
+      }
+      ultimately have "∑[{t};{{⟨t,𝟭⟩}∪{⟨r,𝟬⟩. r∈T-{t}},id(T)}]∈{span of}T" unfolding Span_def[OF assms(1)] using A
+        by auto
+      then have "(({⟨t,𝟭⟩}∪{⟨r,𝟬⟩. r∈T-{t}})`t) ⋅S (id(T)`t) ∈{span of}T" using linComb_one_element[OF asT
+        Af idG] by auto
+      then have "(({⟨t,𝟭⟩}∪{⟨r,𝟬⟩. r∈T-{t}})`t) ⋅S t ∈{span of}T" using asT by auto
+      then have "(𝟭) ⋅S t ∈{span of}T" using apply_equality Af by auto moreover
+      have "(𝟭) ⋅S t=t" using module_ax4 assms asT by auto ultimately
+      have "t∈{span of}T" by auto
+    }
+    then have "T⊆{span of}T" by auto moreover
+    with A have "({span of}T)≠0" by auto moreover
+    {
+      fix l assume "l∈{span of}T"
+      with A obtain S AA where l:"l=∑[S;{AA,id(T)}]" "S∈FinPow(T)" "AA:T→R" "∀m∈T-S. AA`m=𝟬" unfolding Span_def[OF assms(1)]
+        by auto
+      from l(1) have "l∈ℳ" using linComb_is_in_module[OF l(3) _ l(2), of "id(T)"] idG unfolding FinPow_def by auto
+    }
+    then have sub:"({span of}T)⊆ℳ" by force moreover
+    {
+      fix T1 T2 assume as:"T1∈{span of}T"
+        "T2∈{span of}T"
+      with A obtain TT1 AA1 TT2 AA2 where T:"TT1∈FinPow(T)" "TT2∈FinPow(T)" "AA1:T→R"
+        "AA2:T→R" "T1=∑[TT1;{AA1,id(T)}]" "T2=∑[TT2;{AA2,id(T)}]" "∀m∈T-TT1. AA1`m=𝟬" "∀m∈T-TT2. AA2`m=𝟬" unfolding Span_def[OF assms(1)] by auto
+      {
+        assume A:"TT1=0"
+        then have "T1=∑[0;{AA1,id(T)}]" using T(5) by auto
+        also have "…=Θ" using LinearComb_def[OF T(3) idG T(1)] A by auto
+        ultimately have "T1+VT2=Θ+VT2" by auto
+        also have "…∈{span of}T" using sub as(2) mod_ab_gr.group0_2_L2 by auto
+        ultimately have "T1+VT2∈{span of}T" by auto
+      }
+      moreover
+      {
+        assume AA:"TT1≠0"
+        have "T1+VT2=∑[TT1+TT2;{{⟨⟨0,x⟩,AA1`x⟩. x∈T}∪{⟨⟨1,x⟩,AA2`x⟩. x∈T},{⟨⟨0,x⟩,id(T)`x⟩. x∈T}∪{⟨⟨1,x⟩,id(T)`x⟩. x∈T}}]" using linComb_sum[OF T(3,4) idG idG 
+          AA T(1,2)] T(5,6) by auto
+        also have "…=∑[TT1+TT2;{{⟨⟨0,x⟩,AA1`x⟩. x∈T}∪{⟨⟨1,x⟩,AA2`x⟩. x∈T},{⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T}}]" by auto
+        ultimately have eq:"T1+VT2=∑[TT1+TT2;{{⟨⟨0,x⟩,AA1`x⟩. x∈T}∪{⟨⟨1,x⟩,AA2`x⟩. x∈T},{⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T}}]" by auto
+        from T(1,2) obtain n1 n2 where fin:"TT1≈n1" "n1∈nat" "TT2≈n2" "n2∈nat" unfolding FinPow_def Finite_def by auto
+        then have "n1+n2≈n1#+n2" using nat_sum_eqpoll_sum by auto moreover
+        with fin(1,3) have "TT1+TT2≈n1#+n2" using sum_eqpoll_cong[] eqpoll_trans[of "TT1+TT2" "n1+n2" "n1#+n2"] by auto
+        then have "Finite(TT1+TT2)" unfolding Finite_def using add_type by auto
+        then have fin:"TT1+TT2∈FinPow(T+T)" using T(1,2) unfolding FinPow_def by auto moreover
+        have f1:"{⟨⟨0, x⟩, AA1 ` x⟩ . x ∈ T}:{0}×T→R" using apply_type[OF T(3)] unfolding Pi_def function_def by auto
+        have f2:"{⟨⟨1, x⟩, AA2 ` x⟩ . x ∈ T}:{1}×T→R" using apply_type[OF T(4)] unfolding Pi_def function_def by auto
+        have "({0}×T)∩({1}×T)=0" by auto
+        then have ffA:"({⟨⟨0, x⟩, AA1 ` x⟩ . x ∈ T} ∪ {⟨⟨1, x⟩, AA2 ` x⟩ . x ∈ T}):T+T→R" unfolding sum_def using fun_disjoint_Un[OF f1 f2] by auto moreover
+        have f1:"{⟨⟨0, x⟩, x⟩ . x ∈ T}:{0}×T→ℳ" using assms unfolding Pi_def function_def by blast
+        have f2:"{⟨⟨1, x⟩, x⟩ . x ∈ T}:{1}×T→ℳ" using assms unfolding Pi_def function_def by blast
+        have f1T:"{⟨⟨0, x⟩, x⟩ . x ∈ T}:{0}×T→T" using assms unfolding Pi_def function_def by blast
+        have f2T:"{⟨⟨1, x⟩, x⟩ . x ∈ T}:{1}×T→T" using assms unfolding Pi_def function_def by blast
+        have "({0}×T)∩({1}×T)=0" by auto
+        then have ffB:"({⟨⟨0, x⟩, x⟩ . x ∈ T} ∪ {⟨⟨1, x⟩, x⟩ . x ∈T}):T+T→ℳ" and ffBT:"({⟨⟨0, x⟩, x⟩ . x ∈ T} ∪ {⟨⟨1, x⟩, x⟩ . x ∈T}):T+T→T" unfolding sum_def using fun_disjoint_Un[OF f1 f2]
+          using fun_disjoint_Un[OF f1T f2T] by auto
+        obtain AA where AA:"∑[TT1+TT2;{{⟨⟨0,x⟩,AA1`x⟩. x∈T}∪{⟨⟨1,x⟩,AA2`x⟩. x∈T},{⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T}}]=
+          ∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{AA,id(ℳ)}]" "AA:ℳ→R" "∀x∈ℳ-({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2). AA`x=𝟬" 
+          using index_module[OF ffA ffB fin] by auto
+        from ffBT have sub:"({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)⊆T" using func1_1_L6(2) by auto
+        then have finpow:"({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)∈FinPow(T)" using fin Finite_RepFun[of "TT1+TT2" "λt. ({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})`t"] 
+          func_imagedef[OF ffBT, of "TT1+TT2"] unfolding FinPow_def by auto
+        {
+          fix R T assume "R∈Pow(T)"
+          then have "id(R)⊆R*T" using func1_1_L1B[OF id_type] by auto
+          then have "id(R)=restrict(id(T),R)" using right_comp_id_any[of "id(T)"] using left_comp_id[of "id(R)" R T] by force
+        }
+        then have reg:"∀T. ∀R∈Pow(T). id(R)=restrict(id(T),R)" by blast
+        then have "∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=
+          ∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(restrict(AA,T),({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)),id(({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))}]"
+          using linComb_restrict_coord[OF restrict_fun[OF AA(2) assms] func1_1_L1B[OF id_type assms] finpow] sub by auto moreover
+        from sub have " T ∩ ({⟨⟨0, x⟩, x⟩ . x ∈ T} ∪ {⟨⟨1, x⟩, x⟩ . x ∈ T}) `` (TT1 + TT2)=({⟨⟨0, x⟩, x⟩ . x ∈ T} ∪ {⟨⟨1, x⟩, x⟩ . x ∈ T}) `` (TT1 + TT2)" by auto
+        then have "restrict(restrict(AA,T),({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))=restrict(AA,({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))"
+          using restrict_restrict[of AA T "({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)"] by auto
+        ultimately have "∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=
+          ∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)),id(({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))}]" by auto
+        moreover have "({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)⊆ℳ" using sub assms by auto
+        with reg have "id(({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))=restrict(id(ℳ),({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))" by auto
+        ultimately have "∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=
+          ∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)),restrict(id(ℳ),({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2))}]"
+          by auto
+        also have "…=∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{AA,id(ℳ)}]" using linComb_restrict_coord[OF AA(2) id_type, of "({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)"] 
+          finpow unfolding FinPow_def using assms by force
+        ultimately have eq1:"∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=
+          ∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{AA,id(ℳ)}]" by auto
+        have "restrict(AA,T):T→R" using restrict_fun[OF AA(2) assms]. moreover
+        note finpow moreover
+        {
+          fix x assume x:"x∈T-({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)"
+          with assms have "x∈ℳ-({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)" by auto
+          with AA(3) have "AA`x=𝟬" by auto
+          with x have "restrict(AA,T)`x=𝟬" using restrict by auto
+        }
+        then have "∀x∈T-({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2). restrict(AA,T)`x=𝟬" by auto ultimately
+        have "⟨({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2),restrict(AA,T)⟩∈{⟨F,E⟩∈FinPow(T)×(T→R). ∀x∈T-F. E`x=𝟬}" by auto
+        then have "∃F∈FinPow(T). ∃E∈T→R. (∀x∈T-F. E`x=𝟬) ∧ (∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=∑[F;{E,id(T)}])"
+          using exI[of "λF. F∈FinPow(T) ∧ (∃E∈T→R. (∀x∈T-F. E`x=𝟬) ∧ (∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=∑[F;{E,id(T)}]))" "({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)"]
+          exI[of "λE. E∈T→R ∧ ((∀x∈T-(({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2)). E`x=𝟬) ∧ (∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]=∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{E,id(T)}]))"
+            "restrict(AA,T)"] by auto
+        then have "∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{restrict(AA,T),id(T)}]∈{∑[FF;{AA,id(T)}]. 
+          ⟨FF,AA⟩ ∈ {⟨F,E⟩∈FinPow(T)×(T→R). ∀x∈T-F. E`x=𝟬}}" by auto
+        with eq1 have "∑[({⟨⟨0,x⟩,x⟩. x∈T}∪{⟨⟨1,x⟩,x⟩. x∈T})``(TT1+TT2);{AA,id(ℳ)}]∈{span of}T" using A unfolding Span_def[OF assms]
+          by auto
+        with AA(1) eq have "T1+VT2∈{span of}T" by auto
+      }
+      ultimately have "T1+VT2∈{span of}T" by auto
+    }
+    then have "∀x∈{span of}T. ∀y∈{span of}T. x+Vy∈{span of}T" by blast
+    then have "({span of}T){is closed under}AM"  unfolding IsOpClosed_def by auto moreover
+    {
+      fix r TT assume "r∈R" "TT∈{span of}T"
+      with A obtain n AA where T:"r∈R" "TT=∑[n;{AA,id(T)}]" "n∈FinPow(T)" "AA:T→R" "∀x∈T-n. AA`x=𝟬"
+        unfolding Span_def[OF assms(1)] by auto
+      have "r⋅S(TT)=∑[n;{{⟨t,r⋅(AA`t)⟩.t∈T},id(T)}]" using linComb_action(1)[OF T(4) _ T(1) T(3), of "id(T)"] T(2)
+        func1_1_L1B[OF id_type assms] by auto moreover
+      have fun:"{⟨t,r⋅(AA`t)⟩.t∈T}:T→R" using linComb_action(2)[OF T(4) _ T(1,3)] func1_1_L1B[OF id_type assms] by auto
+        moreover
+      {
+        fix z assume z:"z∈T-n"
+        then have "{⟨t,r⋅(AA`t)⟩.t∈T}`z=r⋅(AA`z)" using apply_equality[of z "r⋅(AA`z)"
+          "{⟨t,r⋅(AA`t)⟩.t∈T}" T "λt. R"] using fun by auto
+        also have "…=r⋅𝟬" using T(5) z by auto
+        also have "…=𝟬" using Ring_ZF_1_L6(2)[OF T(1)] by auto
+        ultimately have "{⟨t,r⋅(AA`t)⟩.t∈T}`z=𝟬" by auto
+      }
+      then have "∀z∈T-n. {⟨t,r⋅(AA`t)⟩.t∈T}`z=𝟬" by auto ultimately
+      have "r⋅S(TT)∈{span of}T" unfolding Span_def[OF assms(1)] using A T(3) by auto
+    }
+    then have "∀r∈R. ∀TT∈{span of}T. r⋅S(TT)∈{span of}T" by blast
+    ultimately have "IsAsubmodule({span of}T)" "T⊆({span of}T)" using submoduleI by auto
+  }
+  ultimately show "IsAsubmodule({span of}T)" "T⊆({span of}T)" by auto
+qed
+
+
+text‹Given a linear combination, it is in the span of the image of the second function.›
+
+lemma (in module0) linear_comb_span:
+  assumes "AA:X→R" "B:X→ℳ" "D∈FinPow(X)"
+  shows "∑[D;{AA,B}]∈({span of}(B``D))"
+proof-
+  {
+    assume A:"B``D=0"
+    {
+      assume "D≠0"
+      then obtain d where "d∈D" by auto
+      then have "B`d∈B``D" using image_fun[OF assms(2)] assms(3) unfolding FinPow_def by auto
+      with A have "False" by auto
+    }
+    then have "D=0" by auto
+    then have "∑[D;{AA,B}]=Θ" using LinearComb_def[OF assms] by auto moreover
+    with A have ?thesis using Span_def by auto
+  }
+  moreover
+  {
+    assume A:"B``D≠0"
+    have sub:"B``D⊆ℳ" using assms(2) func1_1_L6(2) by auto
+    from assms obtain AB where AA:"∑[D;{AA,B}]=∑[B``D;{AB,id(ℳ)}]" "AB:ℳ→R" "∀x∈ℳ-B``D. AB`x=𝟬"
+      using index_module by blast
+    have fin:"Finite(B``D)" using func_imagedef[OF assms(2)] assms(3) unfolding FinPow_def
+      using Finite_RepFun[of D "λt. B`t"] by auto
+    with sub have finpow:"B``D∈FinPow(ℳ)" unfolding FinPow_def by auto
+    with AA(1) have "∑[D;{AA,B}]=∑[B``D;{restrict(AB,B``D),restrict(id(ℳ),B``D)}]"
+      using linComb_restrict_coord AA(2) id_type by auto
+    moreover have "restrict(id(ℳ),B``D)=id(ℳ) O id(B``D)" using right_comp_id_any by auto
+    then have "restrict(id(ℳ),B``D)=id(B``D)" using left_comp_id[of "id(B``D)"] sub by auto
+    ultimately have "∑[D;{AA,B}]=∑[B``D;{restrict(AB,B``D),id(B``D)}]" by auto moreover
+    have "restrict(AB,B``D):B``D→R" using AA(2) restrict_fun sub by auto moreover
+    have "∀x∈B``D-B``D. restrict(AB,B``D)`x=𝟬⇩R" by auto ultimately
+    have "∑[D;{AA,B}]∈{span of}(B``D)" using fin A unfolding Span_def[OF sub] FinPow_def by auto
+  }
+  ultimately show ?thesis by blast
+qed
+
+text‹It turns out that the span is the smallest submodule that contains the
+original set.›
+
+theorem(in module0) minimal_submodule:
+  assumes "T⊆𝒩" "IsAsubmodule(𝒩)"
+  shows "({span of}T)⊆𝒩"
+proof-
+  have as:"T⊆ℳ" using assms(1) mod_ab_gr.group0_3_L2[OF sumodule_is_subgroup[OF assms(2)]] by auto 
+  {
+    assume A:"T=0"
+    {
+      fix x assume "x∈{span of}T"
+      with A have "x=Θ" using Span_def[OF as] by auto
+      then have "x∈𝒩" using assms(2) unfolding IsAsubmodule_def
+        using mod_ab_gr.group0_3_L5 by auto
+    }
+    then have "({span of}T)⊆𝒩" by auto
+  }
+  moreover
+  {
+    assume A:"T≠0"
+    {
+      fix x assume "x∈{span of}T"
+      with A obtain n AA where "x=∑[n;{AA,id(T)}]" "n∈FinPow(T)" "AA:T→R"
+        unfolding Span_def[OF as] by auto
+      then have x:"x=∑[n;{AA,id(T)}]" "n∈FinPow(T)" "AA:T→R" "id(T):T→𝒩"
+        using assms(1) func1_1_L1B id_type[of T] by auto
+      then have "x∈𝒩" using linear_comb_submod assms(2) by auto
+    }
+    then have "({span of}T)⊆𝒩" by auto
+  }
+  ultimately show "({span of}T)⊆𝒩" by auto
+qed
+
+end
+ + + \ No newline at end of file diff --git a/docs/IsarMathLib/Module_ZF_2.html b/docs/IsarMathLib/Module_ZF_2.html new file mode 100644 index 0000000..060fdc4 --- /dev/null +++ b/docs/IsarMathLib/Module_ZF_2.html @@ -0,0 +1,389 @@ + + + + + +Theory Module_ZF_2 + + + + +
+

Theory Module_ZF_2

+
+ +
(*
+    This file is a part of IsarMathLib -
+    a library of formalized mathematics written for Isabelle/Isar.
+
+    Copyright (C) 2024  Daniel de la Concepcion Saez
+
+    This program is free software; Redistribution and use in source and binary forms,
+    with or without modification, are permitted provided that the following conditions are met:
+
+   1. Redistributions of source code must retain the above copyright notice,
+   this list of conditions and the following disclaimer.
+   2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation and/or
+   other materials provided with the distribution.
+   3. The name of the author may not be used to endorse or promote products
+   derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
+USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*)
+
+theory Module_ZF_2 imports Module_ZF_1 Ring_ZF_2
+
+begin
+
+text‹The most basic examples of modules, are subsets of the ring; since a ring is an abelian group
+when considering addition. ›
+
+subsection‹Ideals as Modules›
+
+text‹Let's show first that the ring acting on itself is a module; and then we will show that ideals
+are submodules.›
+
+text‹The map that takes every element to its left multiplication map, is a map to endomorphisms.›
+
+lemma (in ring0) action_regular_map:
+  shows "{⟨r,{⟨s,r⋅s⟩. s∈R}⟩. r∈R}:R→End(R,A)" unfolding Pi_def
+    function_def End_def Homomor_def IsMorphism_def apply auto
+  using Ring_ZF_1_L4(3) apply simp using Ring_ZF_1_L4(3) apply simp
+proof-
+  fix x g1 g2 assume as:"x∈R" "g1∈R" "g2∈R"
+  have f:"{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R}:R→R" unfolding Pi_def function_def apply auto
+    using Ring_ZF_1_L4(3) as(1) by auto
+  from f as(2) have g1:"{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R}`g1 = x⋅g1" using apply_equality by auto
+  from f as(3) have g2:"{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R}`g2 = x⋅g2" using apply_equality by auto
+  have "g1\<ra>g2 ∈R" using Ring_ZF_1_L4(1) as(3,2) by auto
+  then have "{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R} `(g1\<ra>g2) = x⋅(g1\<ra>g2)" using apply_equality f by auto
+  with g1 g2 show "{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R} ` (A ` ⟨g1, g2⟩) = A ` ⟨{⟨t, M ` ⟨x, t⟩⟩ . t ∈ R} ` g1, {⟨t, M ` ⟨x, t⟩⟩ . t ∈ R} ` g2⟩"
+    using ring_oper_distr(1)[of x g1 g2] as by auto
+qed
+
+text‹The previous map respects addition because of distribution›
+
+lemma (in ring0) action_regular_distrib:
+  assumes "g1 ∈ R" "g2 ∈ R"
+  shows "{⟨xa, M ` ⟨(A ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R} =
+       EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R} ⟩"
+proof(rule func_eq)
+  from assms have A:"g1\<ra>g2∈R" using Ring_ZF_1_L4(1) by auto
+  then have "{⟨r,{⟨s,r⋅s⟩. s∈R}⟩. r∈R}`(g1\<ra>g2) = {⟨xa, M ` ⟨(A ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R}" using
+    apply_equality action_regular_map by auto
+  then show f1:" {⟨xa, M ` ⟨(A ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R}:R→R" using 
+    apply_type[OF action_regular_map A] unfolding End_def by auto
+  have END:"{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}:End(R,A)" "{⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}:End(R,A)" using 
+     apply_type[OF action_regular_map assms(1)] apply_type[OF action_regular_map assms(2)]
+    apply_equality[OF _ action_regular_map] assms by auto
+  with apply_type[OF restrict_fun[OF monoid0.Group_ZF_2_1_L0A, of R A _ R "End(R,A)×End(R,A)"]] 
+  show f2:"EndAdd(R, A) `
+        ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩:R→R" 
+    unfolding EndAdd_def End_def using Ring_ZF_1_L1(2) unfolding group0_def monoid0_def IsAgroup_def by blast
+  {
+    fix x assume x:"x∈R"
+    then have " {⟨xa, M ` ⟨A ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = (g1\<ra>g2)⋅x" using apply_equality[OF _ f1] by auto
+    moreover
+    from END have "EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = (A {lifted to function space over} R)`⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" using restrict
+      unfolding EndAdd_def by auto
+    with END have "EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = A`⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}`x, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}`x⟩"
+      using group0.Group_ZF_2_1_L3[OF Ring_ZF_1_L1(2) _ _ _ x] unfolding EndAdd_def End_def by auto
+    then have "EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = (g1⋅x)\<ra>(g2⋅x)" using apply_equality x
+      END unfolding End_def by auto
+    moreover
+    have "(g1⋅x)\<ra>(g2⋅x)= (g1\<ra>g2)⋅x" using ring_oper_distr(2) x assms by auto
+    ultimately have " {⟨xa, M ` ⟨A ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" by auto
+  }
+  then show "∀x∈R. {⟨xa, M ` ⟨A ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = EndAdd(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" by auto
+qed
+
+text‹The previous map respects multiplication because of associativity›
+
+lemma (in ring0) action_regular_assoc:
+  assumes "g1 ∈ R" "g2 ∈ R"
+  shows "{⟨xa, M ` ⟨(M ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R} =
+       EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R} ⟩"
+proof(rule func_eq)
+  from assms have A:"g1⋅g2∈R" using Ring_ZF_1_L4(3) by auto
+  then have "{⟨r,{⟨s,r⋅s⟩. s∈R}⟩. r∈R}`(g1⋅g2) = {⟨xa, M ` ⟨(M ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R}" using
+    apply_equality action_regular_map by auto
+  then show f1:" {⟨xa, M ` ⟨(M ` ⟨g1, g2⟩), xa⟩⟩ . xa ∈ R}:R→R" using 
+    apply_type[OF action_regular_map A] unfolding End_def by auto
+  have END:"{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}:End(R,A)" "{⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}:End(R,A)" using 
+     apply_type[OF action_regular_map assms(1)] apply_type[OF action_regular_map assms(2)]
+    apply_equality[OF _ action_regular_map] assms by auto
+  with apply_type[OF restrict_fun[OF func_ZF_5_L1[of R], of "End(R,A)×End(R,A)"]] 
+  show f2:"EndMult(R, A) `
+        ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩:R→R" 
+    unfolding EndMult_def End_def  unfolding group0_def monoid0_def IsAgroup_def by blast
+  {
+    fix x assume x:"x∈R"
+    then have " {⟨xa, M ` ⟨M ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = (g1⋅g2)⋅x" using apply_equality[OF _ f1] by auto
+    moreover
+    from END have "EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = Composition(R)`⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" using restrict
+      unfolding EndMult_def by auto
+    with END have "EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = ({⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R} O {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R})`x"
+      unfolding End_def using  func_ZF_5_L2 by auto
+    then have "EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = {⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R} `({⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}`x)" using x
+      END comp_fun_apply[of "{⟨t,g2⋅t⟩. t∈R}" R R x] unfolding End_def by auto
+    then have "EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = {⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R} `(g2⋅x)"
+      using apply_equality END(2) x unfolding End_def by auto
+    then have "EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x = g1⋅(g2⋅x)"
+      using apply_equality END(1) Ring_ZF_1_L4(3)[OF assms(2) x] unfolding End_def by auto
+    moreover
+    have "g1⋅g2⋅x= g1⋅(g2⋅x)" using Ring_ZF_1_L11(2) x assms by auto
+    ultimately have " {⟨xa, M ` ⟨M ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" by auto
+  }
+  then show "∀x∈R. {⟨xa, M ` ⟨M ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R} ` x = EndMult(R, A) ` ⟨{⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}, {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}⟩ ` x" by auto
+qed
+
+text‹The previous map takes the unit element to the identity map›
+  
+lemma (in ring0) action_regular_neut:
+  shows "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭 = id(R)"
+proof (rule func_eq)
+  from apply_type[OF action_regular_map] have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭 :End(R,A)"
+    using Ring_ZF_1_L2(2) by auto
+  then show f1:"{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭 :R→R" unfolding End_def by auto
+  show "id(R):R→R" using id_inj unfolding inj_def by auto
+  {
+    fix x assume x:"x∈R"
+    have "({⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭) = {⟨xa, M ` ⟨𝟭, xa⟩⟩ . xa ∈ R} "
+      using apply_equality[OF _ action_regular_map] Ring_ZF_1_L2(2) by auto
+    with x f1 have "({⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭)`x = 𝟭⋅x" using apply_equality
+      by auto
+    then have "({⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭)`x = x" using Ring_ZF_1_L3(6) x by auto
+    then have "({⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭)`x = id(R)`x" using x by auto
+  }
+  then show " ∀x∈R. {⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` 𝟭 ` x = id(R) ` x" by auto
+qed
+
+text‹The previous map is an action›
+
+theorem(in ring0) action_regular:
+  shows "IsAction(R,A,M,R,A,{⟨r,{⟨s,r⋅s⟩. s∈R}⟩. r∈R})" unfolding IsAction_def ringHomomor_def
+  IsMorphism_def apply auto using action_regular_map apply simp prefer 3
+  using group0.end_comp_monoid(2)[OF Ring_ZF_1_L1(2)] action_regular_neut unfolding EndMult_def apply simp
+proof-
+  fix g1 g2 assume as: "g1 ∈ R" "g2 ∈ R"
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` (A ` ⟨g1, g2⟩) = {⟨xa, M ` ⟨A ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] Ring_ZF_1_L4(1) as by auto moreover
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g1 = {⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] as(1) by auto moreover
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g2 = {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] as(2) by auto moreover
+  note action_regular_distrib[OF as] ultimately
+  show "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` (A ` ⟨g1, g2⟩) =
+       EndAdd(R, A) ` ⟨{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g1, {⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g2⟩" by auto
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` (M ` ⟨g1, g2⟩) = {⟨xa, M ` ⟨M ` ⟨g1, g2⟩, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] Ring_ZF_1_L4(3) as by auto moreover
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g1 = {⟨xa, M ` ⟨g1, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] as(1) by auto moreover
+  have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g2 = {⟨xa, M ` ⟨g2, xa⟩⟩ . xa ∈ R}"
+    using apply_equality[OF _ action_regular_map] as(2) by auto moreover
+  note action_regular_assoc[OF as] ultimately
+  show "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` (M ` ⟨g1, g2⟩) =
+       (Composition(R) {in End} [R,A]) ` ⟨{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g1, {⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` g2⟩"
+    unfolding EndMult_def by auto
+qed
+
+text‹The action defines the Regular Module›
+
+theorem (in ring0) reg_module:
+  shows "module0(R,A,M,R,A,{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R})" unfolding module0_def
+  module0_axioms_def using ring0_axioms action_regular unfolding ring0_def IsAring_def by auto
+
+text‹Every ideal is a submodule of this regular action.›
+
+corollary (in ring0) ideal_submodule:
+  assumes "I◃R"
+  shows "module0.IsAsubmodule(R,A,{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R},I)"
+proof(rule module0.submoduleI[OF reg_module])
+  from ideal_dest_subset[OF assms] show "I ⊆ R" by auto
+  from ideal_dest_zero[OF assms] show "I≠0" by auto
+  {
+    fix r h assume as:"r:R" "h:I"
+    then have A:"{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` r = {⟨xa, M ` ⟨r, xa⟩⟩ . xa ∈ R}"
+      using apply_equality[OF _ action_regular_map] by auto
+    then have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` r `h= {⟨xa, M ` ⟨r, xa⟩⟩ . xa ∈ R}`h" by auto
+    moreover from A have "{⟨xa, M ` ⟨r, xa⟩⟩ . xa ∈ R}:R→R" using apply_type[OF action_regular_map as(1)] 
+      unfolding End_def by auto
+    then have "{⟨xa, M ` ⟨r, xa⟩⟩ . xa ∈ R}`h = r⋅h" using apply_equality as(2) ideal_dest_subset[OF assms] by auto
+    ultimately have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` r `h=r⋅h" by auto
+    then have "{⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` r `h:I" using as ideal_dest_mult(2) assms by auto
+  }
+  then show "∀r∈R. ∀h∈I. {⟨x, {⟨xa, M ` ⟨x, xa⟩⟩ . xa ∈ R}⟩ . x ∈ R} ` r ` h ∈ I" by auto
+  show "I{is closed under}A" using assms ideal_dest_sum unfolding IsOpClosed_def by auto
+qed
+
+subsection‹Annihilators›
+
+text‹An annihilator of a module subset is the set of elements of the ring whose action
+on that module subset is $0$.›
+
+definition (in module0) ann where
+"N ⊆ ℳ ⟹ ann(N) ≡ {r∈R. ∀n∈N. r⋅Sn =Θ}"
+
+text‹If the subset is a submodule, then the annihilator is an ideal.›
+
+lemma (in module0) ann_ideal:
+  assumes "IsAsubmodule(N)"
+  shows "ann(N)◃R" unfolding Ideal_def
+proof(safe)
+  have sub:"N ⊆ ℳ" using mod_ab_gr.group0_3_L2 using assms unfolding IsAsubmodule_def by auto
+  fix x y assume as:"x∈ann(N)" "y∈R"
+  {
+    fix n assume n:"n∈N"
+    then have "(x⋅y)⋅Sn=x⋅S(y⋅Sn)" using module_ax3 as assms sub unfolding ann_def[OF sub]
+      by auto
+    moreover have "y⋅Sn∈N" using n as(2) sumodule_is_subaction[OF assms] by auto
+    with as(1) have "x⋅S(y⋅Sn) = Θ" unfolding ann_def[OF sub] by auto
+    ultimately have "(x⋅y)⋅Sn=Θ" by auto
+  }
+  then have "∀n∈N. (x⋅y)⋅Sn=Θ" by auto
+  then show "x⋅y∈ann(N)" using as Ring_ZF_1_L4(3) unfolding ann_def[OF sub] by auto
+  {
+    fix n assume n:"n∈N"
+    then have "(y⋅x)⋅Sn=y⋅S(x⋅Sn)" using module_ax3 as assms sub unfolding ann_def[OF sub] by auto
+    moreover have "x⋅Sn=Θ" using n as(1) unfolding ann_def[OF sub] by auto
+    with as(2) have "y⋅S(x⋅Sn) = Θ" using zero_fixed by auto
+    ultimately have "(y⋅x)⋅Sn=Θ" by auto
+  }
+  then have "∀n∈N. (y⋅x)⋅Sn=Θ" by auto
+  then show "y⋅x∈ann(N)" using as Ring_ZF_1_L4(3) unfolding ann_def[OF sub] by auto
+next
+  have sub:"N ⊆ ℳ" using mod_ab_gr.group0_3_L2 using assms unfolding IsAsubmodule_def by auto
+  show "IsAsubgroup(ann(N),A)"
+  proof(rule add_group.group0_3_T3)
+    show "ann(N) ⊆ R" unfolding ann_def[OF sub] by auto
+    have "𝟬∈R" using Ring_ZF_1_L2(1) by auto
+    moreover have "∀n∈N. 𝟬⋅Sn=Θ" using mult_zero sub by auto
+    ultimately have "𝟬∈ann(N)" unfolding ann_def[OF sub] by auto
+    then show "ann(N)≠0" by auto
+    {
+      fix x assume "x∈ann(N)"
+      then have x:"x∈R" "∀n∈N. x⋅Sn=Θ" unfolding ann_def[OF sub] by auto
+      {
+        fix n assume n:"n∈N"
+        have "(\<rm>x)⋅Sn=(x⋅(\<rm>𝟭))⋅Sn" using Ring_ZF_1_L7(2)[of x 𝟭] Ring_ZF_1_L2(2)
+          Ring_ZF_1_L3(5)[of x] x(1) by auto
+        then have "(\<rm>x)⋅Sn=x⋅S((\<rm>𝟭)⋅Sn)" using module_ax3[of x "\<rm>𝟭" n]
+          using n sub x(1) Ring_ZF_1_L3(1)[OF Ring_ZF_1_L2(2)] by auto
+        moreover have "(\<rm>𝟭)⋅Sn∈N" using sumodule_is_subaction[OF assms Ring_ZF_1_L3(1)[OF Ring_ZF_1_L2(2)] n].
+        then have "x⋅S((\<rm>𝟭)⋅Sn) = Θ" using x(2) by auto
+        ultimately have "(\<rm>x)⋅Sn=Θ" by auto
+      }
+      then have "∀n∈N. (\<rm>x)⋅Sn=Θ" by auto moreover
+      have "(\<rm>x)∈R" using Ring_ZF_1_L3(1) x(1) by auto
+      ultimately have "(\<rm>x) ∈ ann(N)" unfolding ann_def[OF sub] by auto
+    }
+    then show "∀x∈ann(N). (\<rm>x) ∈ ann(N)" by auto
+    {
+      fix x y assume as:"x∈ann(N)" "y∈ann(N)"
+      from as(1) have x:"x∈R" unfolding ann_def[OF sub] by auto
+      from as(2) have y:"y∈R" unfolding ann_def[OF sub] by auto
+      {
+        fix n assume n:"n∈N"
+        from n as(1) have x0:"x⋅Sn=Θ" unfolding ann_def[OF sub] by auto
+        from n as(2) have y0:"y⋅Sn=Θ" unfolding ann_def[OF sub] by auto
+        have "(x\<ra>y)⋅Sn = (x⋅Sn) +V(y⋅Sn)" using module_ax2[of x y n] x y n sub by auto
+        with x0 y0 have "(x\<ra>y)⋅Sn =Θ +VΘ" by auto
+        then have "(x\<ra>y)⋅Sn =Θ" using zero_neutral(1) zero_in_mod by auto
+      }
+      then have "∀n∈N. (x\<ra>y)⋅Sn =Θ" by auto moreover
+      have "x\<ra>y:R" using Ring_ZF_1_L4(1) x y by auto
+      ultimately have "x\<ra>y∈ann(N)" unfolding ann_def[OF sub] by auto
+    }
+    then show "ann(N) {is closed under} A" unfolding IsOpClosed_def by auto
+  qed
+qed
+
+text‹Annihilator is reverse monotonic›
+
+lemma (in module0) ann_mono:
+  assumes "N ⊆ ℳ" "K ⊆ N"
+  shows "ann(N) ⊆ ann(K)"
+proof
+  fix x assume "x∈ann(N)"
+  then have "x∈R" "∀n∈N. x⋅Sn =Θ" unfolding ann_def[OF assms(1)] by auto
+  then have "x∈R" "∀n∈K. x⋅Sn =Θ" using assms(2) by auto
+  then have "x∈ {r ∈ R . ∀n∈K. r ⋅S n = Θ}" by auto moreover
+  from assms have "K ⊆ ℳ" by auto
+  ultimately show "x∈ann(K)" using ann_def[of K] by auto
+qed
+
+
+text‹If the ring is commutative, the annihilator of a subset shrinks to the annihilator
+of the generated submodule›
+
+lemma (in module0) comm_ann_of_ideal:
+  assumes "N ⊆ ℳ" "M {is commutative on} R"
+  shows "ann(N) = ann({span of}N)"
+proof
+  have "N ⊆ {span of}N" using linear_ind_set_comb_submodule(2) assms(1) by auto
+  moreover have "({span of}N) ⊆ ℳ" using trivial_submodules(1)
+    minimal_submodule[OF assms(1)] by auto moreover
+  note assms(1) ultimately show "ann({span of}N) ⊆ ann(N)" using ann_mono by auto
+  {
+    fix x assume "x∈ann(N)"
+    then have x:"x∈R" "∀n∈N. x⋅Sn =Θ" unfolding ann_def[OF assms(1)] by auto
+    let ?Q="{m∈ℳ. x⋅Sm=Θ}"
+    have "IsAsubmodule(?Q)"
+    proof (rule submoduleI)
+      show "?Q ⊆ ℳ" by auto
+      have "Θ∈?Q" using zero_fixed x(1) zero_in_mod by auto
+      then show "?Q≠0" by auto
+      {
+        fix t h assume as:"t∈R" "h:?Q"
+        from as(2) have h:"h∈ℳ" "x⋅Sh=Θ" by auto
+        have "x⋅S(t⋅Sh) = (x⋅t)⋅Sh" using module_ax3 as(1) x(1) h(1) by auto
+        then have "x⋅S(t⋅Sh) = (t⋅x)⋅Sh" using as(1) x(1) assms(2) unfolding IsCommutative_def by auto
+        then have "x⋅S(t⋅Sh) = t⋅S(x⋅Sh)" using module_ax3 as(1) x(1) h(1) by auto
+        with h(2) have "x⋅S(t⋅Sh) = t⋅SΘ" by auto
+        then have "x⋅S(t⋅Sh) = Θ" using zero_fixed as(1) by auto
+        moreover have "t⋅Sh∈ℳ" using as(1) h(1) apply_type[OF H_val_type(2)] by auto
+        ultimately have "t⋅Sh∈?Q" by auto
+      }
+      then show " ∀r∈R. ∀h∈{m ∈ ℳ . x ⋅S m = Θ}. r ⋅S h ∈ {m ∈ ℳ . x ⋅S m = Θ}" by auto
+      {
+        fix u v assume "u:?Q" "v:?Q"
+        then have uv:"u∈ℳ" "v∈ℳ" "x ⋅S u = Θ" "x ⋅S v = Θ" by auto
+        have "x⋅S(u+Vv) = x ⋅S u +V x ⋅S v" using module_ax1 uv(1,2) x(1) by auto
+        with uv(3,4) have "x⋅S(u+Vv) = Θ +V Θ" by auto
+        then have "x⋅S(u+Vv) = Θ" using zero_neutral(1) zero_in_mod by auto
+        moreover have "u+Vv:ℳ" using mod_ab_gr.group_op_closed uv(1,2) by auto
+        ultimately have "u+Vv:?Q" by auto
+      }
+      then show "?Q{is closed under}AM" unfolding IsOpClosed_def by auto
+    qed
+    moreover have "N ⊆ ?Q" using assms(1) x(2) by auto
+    ultimately have "({span of}N) ⊆ ?Q" using minimal_submodule by auto
+    then have "ann(?Q) ⊆ ann({span of}N)" using ann_mono[of ?Q "{span of}N"] by auto
+    moreover have "ann(?Q) = {r∈R. ∀n∈?Q. r⋅Sn = Θ}" using ann_def[of ?Q] by auto
+    then have "ann(?Q) = {r∈R. ∀n∈ℳ. x⋅Sn=Θ ⟶ r⋅Sn = Θ}" using ann_def[of ?Q] by auto
+    with x(1) have "x∈ann(?Q)" by auto
+    ultimately have "x∈ann({span of}N)" by auto
+  }
+  then show "ann(N) ⊆ ann({span of}N)" by auto
+qed
+
+text‹Annihilators on commutative rings are ideals›
+
+corollary (in module0) comm_ann_ideal:
+  assumes "N ⊆ ℳ" "M {is commutative on} R"
+  shows "ann(N) ◃R" using comm_ann_of_ideal[OF assms] linear_ind_set_comb_submodule(1)[OF assms(1)]
+    ann_ideal by auto
+
+end
+ + + \ No newline at end of file diff --git a/docs/IsarMathLib/document.pdf b/docs/IsarMathLib/document.pdf index 581b951..cbe9c39 100644 Binary files a/docs/IsarMathLib/document.pdf and b/docs/IsarMathLib/document.pdf differ diff --git a/docs/IsarMathLib/index.html b/docs/IsarMathLib/index.html index 0839b0d..e653bce 100644 --- a/docs/IsarMathLib/index.html +++ b/docs/IsarMathLib/index.html @@ -122,6 +122,10 @@

Theories

  • Module_ZF
    • +
  • Module_ZF_1
    • + +
  • Module_ZF_2
    • +
  • VectorSpace_ZF
  • OrderedField_ZF
    • diff --git a/docs/IsarMathLib/outline.pdf b/docs/IsarMathLib/outline.pdf index 74e2563..71d5805 100644 Binary files a/docs/IsarMathLib/outline.pdf and b/docs/IsarMathLib/outline.pdf differ diff --git a/docs/IsarMathLib/session_graph.pdf b/docs/IsarMathLib/session_graph.pdf index 211bbba..0a02286 100644 Binary files a/docs/IsarMathLib/session_graph.pdf and b/docs/IsarMathLib/session_graph.pdf differ