The abstract of the Mizar article:

Linear Independence in Left Module over Domain

by

Michal Muzalewski, and

Wojciech Skaba

Received October 22, 1990

MML identifier: LMOD_5

[ Mizar article, MML identifier index ]

environ

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


begin

 reserve x for set,
         R for Ring,
         V for LeftMod of R,
         v,v1,v2 for Vector of V,
         A,B for Subset of V;

definition let R be non empty doubleLoopStr;
           let V be non empty VectSpStr over R;
 let IT be Subset of V;
 attr IT is linearly-independent means
:: LMOD_5:def 1
  for l be Linear_Combination of IT
   st Sum(l) = 0.V holds Carrier(l) = {};
 antonym IT is linearly-dependent;
end;

canceled;

theorem :: LMOD_5:2
   A c= B & B is linearly-independent implies A is linearly-independent;

theorem :: LMOD_5:3
 0.R <> 1_ R & A is linearly-independent
  implies not 0.V in A;

theorem :: LMOD_5:4
   {}(the carrier of V) is linearly-independent;

theorem :: LMOD_5:5
 0.R <> 1_ R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;

theorem :: LMOD_5:6
   0.R <> 1_ R implies
   {v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent;

theorem :: LMOD_5:7
  for R being domRing,
      V being LeftMod of R,
      L being Linear_Combination of V,
      a being Scalar of R holds
 a <> 0.R implies Carrier(a * L) = Carrier(L);

theorem :: LMOD_5:8
  for R being domRing,
      V being LeftMod of R,
      L being Linear_Combination of V,
      a being Scalar of R holds
   Sum(a * L) = a * Sum(L);

 reserve R for domRing,
         V for LeftMod of R,
         A,B for 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; let V; let A;
 func Lin(A) -> strict Subspace of V means
:: LMOD_5:def 2
  the carrier of it = {Sum(l) : not contradiction};
end;

theorem :: LMOD_5:9
 x in Lin(A) iff ex l st x = Sum(l);

theorem :: LMOD_5:10
 x in A implies x in Lin(A);

theorem :: LMOD_5:11
   Lin({}(the carrier of V)) = (0).V;

theorem :: LMOD_5:12
   Lin(A) = (0).V implies A = {} or A = {0.V};

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

theorem :: LMOD_5:14
   for V being strict LeftMod of R, A being Subset of V st
  0.R <> 1_ R &
  A = the carrier of V holds Lin(A) = V;

theorem :: LMOD_5:15
 A c= B implies Lin(A) is Subspace of Lin(B);

theorem :: LMOD_5:16
   for V being strict LeftMod of R, A,B being Subset of V
  st Lin(A) = V & A c= B holds Lin(B) = V;

theorem :: LMOD_5:17
   Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: LMOD_5:18
   Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);