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


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
proof end;

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 & A is linearly-independent holds
not 0. V in A
proof end;

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

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 & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof end;

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 & {(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
proof end;

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) by VECTSP_7:22;

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 ) by VECTSP_7:7;

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 by VECTSP_7:8;

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

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)} ) by VECTSP_7:10;

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 & A = the carrier of W holds
Lin A = W
proof end;

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 & A = the carrier of V holds
Lin A = V
proof end;

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 by VECTSP_7:13;

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 & A c= B holds
Lin B = V
proof end;

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) by VECTSP_7:15;

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) by VECTSP_7:16;