:: RMOD_5 semantic presentation

definition

let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
attr IT is linearly-independent means :Def1: :: RMOD_5:def 1
for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} ;

end;

:: deftheorem Def1 defines linearly-independent RMOD_5:def 1 :

notation

let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
antonym linearly-dependent IT for linearly-independent IT;

end;

theorem :: RMOD_5:1

canceled;

theorem :: RMOD_5:2

for R being Ring
for V being RightMod 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: :: RMOD_5:3

for R being Ring
for V being RightMod 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 :: RMOD_5:4

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

proof end;

theorem Th5: :: RMOD_5:5

for R being Ring
for V being RightMod 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 :: RMOD_5:6

for R being Ring
for V being RightMod 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;

definition

let R be domRing;
let V be RightMod of R;
let A be Subset of V;
func Lin A -> strict Submodule of V means :Def2: :: RMOD_5:def 2
the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence

proof end;

uniqueness by RMOD_2:37;

end;

:: deftheorem Def2 defines Lin RMOD_5:def 2 :

theorem :: RMOD_5:7

canceled;

theorem :: RMOD_5:8

canceled;

theorem Th9: :: RMOD_5:9

for x being set
for R being domRing
for V being RightMod 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: :: RMOD_5:10

for x being set
for R being domRing
for V being RightMod of R
for A being Subset of V st x in A holds
x in Lin A

proof end;

theorem :: RMOD_5:11

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

proof end;

theorem :: RMOD_5:12

for R being domRing
for V being RightMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )

proof end;

theorem Th13: :: RMOD_5:13

for R being domRing
for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W

proof end;

theorem :: RMOD_5:14

for R being domRing
for V being strict RightMod 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: :: RMOD_5:15

for R being domRing
for V being RightMod of R
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B

proof end;

theorem :: RMOD_5:16

for R being domRing
for V being strict RightMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V

proof end;

theorem :: RMOD_5:17

for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)

proof end;

theorem :: RMOD_5:18

for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)

proof end;