:: Linear Independence in Left Module over Domain
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

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

:: deftheorem Def1 defines linearly-independent LMOD_5:def_1_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );

notation
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let IT be Subset of V;
antonym  linearly-dependent IT for  linearly-independent ;
end;

theorem :: LMOD_5:1
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proofend;

theorem Th2: :: LMOD_5:2
for R being Ring
for V being LeftMod of R
for A being Subset of V st 0. R <> 1. R &amp; A is linearly-independent holds
not 0. V in A
proofend;

theorem :: LMOD_5:3
for R being Ring
for V being LeftMod of R holds {} the carrier of V is linearly-independent
proofend;

theorem Th4: :: LMOD_5:4
for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st 0. R <> 1. R &amp; {v1,v2} is linearly-independent holds
( v1 <> 0. V &amp; v2 <> 0. V )
proofend;

theorem :: LMOD_5:5
for R being Ring
for V being LeftMod of R
for v being Vector of V st 0. R <> 1. R holds
( {v,(0. V)} is linearly-dependent &amp; {(0. V),v} is linearly-dependent ) by Th4;

theorem Th6: :: LMOD_5:6
for R being domRing
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
proofend;

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

definition
let R be domRing;
let V be LeftMod of R;
let A be Subset of V;
func Lin A ->  strict Subspace of V means :Def2: :: LMOD_5:def 2
 the carrier of it =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }
proofend;
uniqueness
 for b1, b2 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  &amp; the carrier of b2 =  {  (Sum l) where l is Linear_Combination of A : verum  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def2 defines Lin LMOD_5:def_2_:_
 for R being domRing
for V being LeftMod of R
for A being Subset of V
for b4 being strict Subspace of V holds
( b4 = Lin A iff the carrier of b4 =  {  (Sum l) where l is Linear_Combination of A : verum  }  );

theorem Th8: :: LMOD_5:8
for x being set
for R being domRing
for V being LeftMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proofend;

theorem Th9: :: LMOD_5:9
for x being set
for R being domRing
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
proofend;

theorem :: LMOD_5:10
for R being domRing
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
proofend;

theorem :: LMOD_5:11
for R being domRing
for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proofend;

theorem Th12: :: LMOD_5:12
for R being domRing
for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st 0. R <> 1. R &amp; A = the carrier of W holds
Lin A = W
proofend;

theorem :: LMOD_5:13
for R being domRing
for V being strict LeftMod of R
for A being Subset of V st 0. R <> 1. R &amp; A = the carrier of V holds
Lin A = V
proofend;

theorem Th14: :: LMOD_5:14
for R being domRing
for V being LeftMod of R
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proofend;

theorem :: LMOD_5:15
for R being domRing
for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V &amp; A c= B holds
Lin B = V
proofend;

theorem :: LMOD_5:16
for R being domRing
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proofend;

theorem :: LMOD_5:17
for R being domRing
for V being LeftMod of R
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proofend;