:: by Micha{\l} Muzalewski and Wojciech Skaba

::

:: Received October 22, 1990

:: Copyright (c) 1990-2013 Association of Mizar Users

definition

let R be non empty doubleLoopStr ;

let V be non empty VectSpStr over R;

let IT be Subset of V;

end;
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 being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} ;

for l being Linear_Combination of IT st Sum l = 0. V holds

Carrier l = {} ;

:: deftheorem 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 = {} );

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;
let V be non empty VectSpStr over R;

let IT be Subset of V;

antonym linearly-dependent IT for linearly-independent ;

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

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

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

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

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

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)

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;

ex b_{1} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum }

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b_{2} = { (Sum l) where l is Linear_Combination of A : verum } holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: 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 b_{4} being strict Subspace of V holds

( b_{4} = Lin A iff the carrier of b_{4} = { (Sum l) where l is Linear_Combination of A : verum } );

for R being domRing

for V being LeftMod of R

for A being Subset of V

for b

( b

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 )

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

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

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

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

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

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

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

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)

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

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;