:: LMOD_5 semantic presentation

definition

let R be non empty doubleLoopStr ;
let V be non empty VectSpStr of R;
let IT be Subset of V;
attr IT 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 :

notation

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

end;

theorem :: LMOD_5:1

canceled;

theorem :: LMOD_5:2

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 Th3: :: LMOD_5:3

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:4

for R being Ring
for V being LeftMod of R holds {} the carrier of V is linearly-independent

proof end;

theorem Th5: :: LMOD_5:5

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:6

for R being Ring
for V being LeftMod of R
for v being Vector of V st 0. R <> 1. R holds
( not {v,(0. V)} is linearly-independent & not {(0. V),v} is linearly-independent ) by Th5;

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 st a <> 0. R holds
Carrier (a * L) = Carrier L

proof end;

theorem Th8: :: LMOD_5:8

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)

proof end;

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

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def2 defines Lin LMOD_5:def 2 :

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 holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

proof end;

theorem Th10: :: LMOD_5:10

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

proof end;

theorem :: LMOD_5:11

for R being domRing
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V

proof end;

theorem :: LMOD_5:12

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)} )

proof end;

theorem Th13: :: LMOD_5:13

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:14

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 Th15: :: LMOD_5:15

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

proof end;

theorem :: LMOD_5:16

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:17

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)

proof end;

theorem :: LMOD_5:18

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)

proof end;