:: LMOD_5 semantic presentation

definition

let c₁ be non empty doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Subset of c₂;
attr a₃ is linearly-independent means :Def1: :: LMOD_5:def 1
for b₁ being Linear_Combination of a₃ st Sum b₁ = 0. a₂ holds
Carrier b₁ = {} ;

end;

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

notation

let c₁ be non empty doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Subset of c₂;
antonym linearly-dependent c₃ for linearly-independent c₃;

end;

theorem Th1: :: LMOD_5:1

canceled;

theorem Th2: :: LMOD_5:2

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ c= b₄ & b₄ is linearly-independent holds
b₃ is linearly-independent

proof end;

theorem Th3: :: LMOD_5:3

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ & b₃ is linearly-independent holds
not 0. b₂ in b₃

proof end;

theorem Th4: :: LMOD_5:4

for b₁ being Ring
for b₂ being LeftMod of b₁ holds {} the carrier of b₂ is linearly-independent

proof end;

theorem Th5: :: LMOD_5:5

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃, b₄ being Vector of b₂ st 0. b₁ <> 1. b₁ & {b₃,b₄} is linearly-independent holds
( b₃ <> 0. b₂ & b₄ <> 0. b₂ )

proof end;

theorem Th6: :: LMOD_5:6

for b₁ being Ring
for b₂ being LeftMod of b₁
for b₃ being Vector of b₂ st 0. b₁ <> 1. b₁ holds
( not {b₃,(0. b₂)} is linearly-independent & not {(0. b₂),b₃} is linearly-independent ) by Th5;

theorem Th7: :: LMOD_5:7

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃ being Linear_Combination of b₂
for b₄ being Scalar of b₁ st b₄ <> 0. b₁ holds
Carrier (b₄ * b₃) = Carrier b₃

proof end;

theorem Th8: :: LMOD_5:8

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃ being Linear_Combination of b₂
for b₄ being Scalar of b₁ holds Sum (b₄ * b₃) = b₄ * (Sum b₃)

proof end;

definition

let c₁ be domRing;
let c₂ be LeftMod of c₁;
let c₃ be Subset of c₂;
func Lin c₃ -> strict Subspace of a₂ means :Def2: :: LMOD_5:def 2
the carrier of a₄ = { (Sum b₁) where B 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 b₁ being set
for b₂ being domRing
for b₃ being LeftMod of b₂
for b₄ being Subset of b₃ holds
( b₁ in Lin b₄ iff ex b₅ being Linear_Combination of b₄ st b₁ = Sum b₅ )

proof end;

theorem Th10: :: LMOD_5:10

for b₁ being set
for b₂ being domRing
for b₃ being LeftMod of b₂
for b₄ being Subset of b₃ st b₁ in b₄ holds
b₁ in Lin b₄

proof end;

theorem Th11: :: LMOD_5:11

for b₁ being domRing
for b₂ being LeftMod of b₁ holds Lin ({} the carrier of b₂) = (0). b₂

proof end;

theorem Th12: :: LMOD_5:12

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂ holds
( not Lin b₃ = (0). b₂ or b₃ = {} or b₃ = {(0. b₂)} )

proof end;

theorem Th13: :: LMOD_5:13

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃ being Subset of b₂
for b₄ being strict Subspace of b₂ st 0. b₁ <> 1. b₁ & b₃ = the carrier of b₄ holds
Lin b₃ = b₄

proof end;

theorem Th14: :: LMOD_5:14

for b₁ being domRing
for b₂ being strict LeftMod of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ & b₃ = the carrier of b₂ holds
Lin b₃ = b₂

proof end;

theorem Th15: :: LMOD_5:15

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ c= b₄ holds
Lin b₃ is Subspace of Lin b₄

proof end;

theorem Th16: :: LMOD_5:16

for b₁ being domRing
for b₂ being strict LeftMod of b₁
for b₃, b₄ being Subset of b₂ st Lin b₃ = b₂ & b₃ c= b₄ holds
Lin b₄ = b₂

proof end;

theorem Th17: :: LMOD_5:17

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ holds Lin (b₃ \/ b₄) = (Lin b₃) + (Lin b₄)

proof end;

theorem Th18: :: LMOD_5:18

for b₁ being domRing
for b₂ being LeftMod of b₁
for b₃, b₄ being Subset of b₂ holds Lin (b₃ /\ b₄) is Subspace of (Lin b₃) /\ (Lin b₄)

proof end;