The abstract of the Mizar article:

Free Modules

by

Michal Muzalewski

Received October 18, 1991

MML identifier: MOD_3

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCSDOM, VECTSP_1, ARYTM_1, RLVECT_1, VECTSP_2, RLVECT_2,
      FINSEQ_1, FINSET_1, FUNCT_1, RELAT_1, SEQ_1, BOOLE, RLVECT_3, RLSUB_1,
      FUNCT_2, PRELAMB, ZFMISC_1, TARSKI, ORDERS_1, MOD_3, HAHNBAN, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, FINSET_1, FINSEQ_1,
      RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, FRAENKEL, FINSEQ_4, RLVECT_1,
      ORDINAL1, ORDERS_1, RLVECT_2, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4,
      VECTSP_5, VECTSP_6, LMOD_5;
 constructors ORDERS_1, VECTSP_5, VECTSP_6, LMOD_5, RLVECT_2, FINSEQ_4,
      MEMBERED, XBOOLE_0;
 clusters VECTSP_2, VECTSP_4, RELSET_1, STRUCT_0, RLVECT_2, SUBSET_1, ARYTM_3,
      VECTSP_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

canceled;

theorem :: MOD_3:2
for R being non degenerated add-associative right_zeroed
     right_complementable (non empty doubleLoopStr) holds 0.R <> -1_ R;

 reserve x,y for set,
         R for Ring,
         V for LeftMod of R,
         L for Linear_Combination of V,
         a for Scalar of R,
         v,u for Vector of V,
         F,G for FinSequence of the carrier of V,
         C for finite Subset of V;

canceled 3;

theorem :: MOD_3:6
 Carrier(L) c= C implies ex F st
  F is one-to-one & rng F = C & Sum(L) = Sum(L (#) F);

theorem :: MOD_3:7
 Sum(a * L) = a * Sum(L);

 reserve X,Y,Z for set,
         A,B for Subset of V,
         T for finite Subset of V,
         l for Linear_Combination of A,
         f,g for Function of the carrier of V,the carrier of R;

definition let R,V,A;
 func Lin(A) -> strict Subspace of V means
:: MOD_3:def 1
   the carrier of it = {Sum(l) : not contradiction};
end;

canceled 3;

theorem :: MOD_3:11
 x in Lin(A) iff ex l st x = Sum(l);

theorem :: MOD_3:12
 x in A implies x in Lin(A);

theorem :: MOD_3:13
 Lin({}(the carrier of V)) = (0).V;

theorem :: MOD_3:14
   Lin(A) = (0).V implies A = {} or A = {0.V};

theorem :: MOD_3:15
 for W being strict Subspace of V
 holds 0.R <> 1_ R & A = the carrier of W implies Lin(A) = W;

theorem :: MOD_3:16
   for V being strict LeftMod of R
 for A being Subset of V
 holds 0.R <> 1_ R & A = the carrier of V implies Lin(A) = V;

theorem :: MOD_3:17
 A c= B implies Lin(A) is Subspace of Lin(B);

theorem :: MOD_3:18
   Lin(A) = V & A c= B implies Lin(B) = V;

theorem :: MOD_3:19
   Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: MOD_3:20
   Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);

definition let R,V;
 let IT be Subset of V;
 attr IT is base means
:: MOD_3:def 2
  IT is linearly-independent & Lin(IT) = the VectSpStr of V;
end;

definition let R;
 let IT be LeftMod of R;
 attr IT is free means
:: MOD_3:def 3
  ex B being Subset of IT st B is base;
end;

theorem :: MOD_3:21
 (0).V is free;

definition let R;
 cluster strict free LeftMod of R;
end;

reserve R for Skew-Field;
reserve a,b for Scalar of R;
reserve V for LeftMod of R;
reserve v,v1,v2,u for Vector of V;
reserve f for Function of the carrier of V,the carrier of R;

canceled;

theorem :: MOD_3:23
   {v} is linearly-independent iff v <> 0.V;

theorem :: MOD_3:24
 v1 <> v2 & {v1,v2} is linearly-independent iff
  v2 <> 0.V & for a holds v1 <> a * v2;

theorem :: MOD_3:25
   v1 <> v2 & {v1,v2} is linearly-independent iff
  for a,b st a * v1 + b * v2 = 0.V holds a = 0.R & b = 0.R;

theorem :: MOD_3:26
  for V being LeftMod of R
 for A being Subset of V
  holds A is linearly-independent implies
   ex B being Subset of V st A c= B & B is base;

theorem :: MOD_3:27
 for V being LeftMod of R
 for A being Subset of V
 holds Lin(A) = V implies ex B being Subset of V st
  B c= A & B is base;

theorem :: MOD_3:28
   for V being LeftMod of R holds V is free;

definition let R; let V be LeftMod of R;
 canceled;

 mode Basis of V -> Subset of V means
:: MOD_3:def 5
  it is base;
end;

theorem :: MOD_3:29
   for V being LeftMod of R
 for A being Subset of V holds
 A is linearly-independent implies ex I being Basis of V st A c= I;

theorem :: MOD_3:30
   for V being LeftMod of R
 for A being Subset of V
 holds Lin(A) = V implies ex I being Basis of V st I c= A;