:: VECTSP_7 semantic presentation

definition

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

end;

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

notation

let c₁ be Field;
let c₂ be VectSp of c₁;
let c₃ be Subset of c₂;
antonym linearly-dependent c₃ for linearly-independent c₃;

end;

theorem Th1: :: VECTSP_7:1

canceled;

theorem Th2: :: VECTSP_7:2

for b₁ being Field
for b₂ being VectSp 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: :: VECTSP_7:3

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
not 0. b₂ in b₃

proof end;

theorem Th4: :: VECTSP_7:4

for b₁ being Field
for b₂ being VectSp of b₁ holds {} the carrier of b₂ is linearly-independent

proof end;

registration

let c₁ be Field;
let c₂ be VectSp of c₁;
cluster linearly-independent Element of bool the carrier of a₂;
existence

proof end;

end;

theorem Th5: :: VECTSP_7:5

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂ holds
( {b₃} is linearly-independent iff b₃ <> 0. b₂ )

proof end;

theorem Th6: :: VECTSP_7:6

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

proof end;

theorem Th7: :: VECTSP_7:7

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂ holds
( not {b₃,(0. b₂)} is linearly-independent & not {(0. b₂),b₃} is linearly-independent ) by Th6;

theorem Th8: :: VECTSP_7:8

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄ being Vector of b₂ holds
( b₃ <> b₄ & {b₃,b₄} is linearly-independent iff ( b₄ <> 0. b₂ & ( for b₅ being Element of b₁ holds b₃ <> b₅ * b₄ ) ) )

proof end;

theorem Th9: :: VECTSP_7:9

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄ being Vector of b₂ holds
( ( b₃ <> b₄ & {b₃,b₄} is linearly-independent ) iff for b₅, b₆ being Element of b₁ st (b₅ * b₃) + (b₆ * b₄) = 0. b₂ holds
( b₅ = 0. b₁ & b₆ = 0. b₁ ) )

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
let c₃ be Subset of c₂;
func Lin c₃ -> strict Subspace of a₂ means :Def2: :: VECTSP_7: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 VECTSP_7:def 2 :

theorem Th10: :: VECTSP_7:10

canceled;

theorem Th11: :: VECTSP_7:11

canceled;

theorem Th12: :: VECTSP_7:12

for b₁ being set
for b₂ being Field
for b₃ being VectSp 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 Th13: :: VECTSP_7:13

for b₁ being set
for b₂ being Field
for b₃ being VectSp of b₂
for b₄ being Subset of b₃ st b₁ in b₄ holds
b₁ in Lin b₄

proof end;

theorem Th14: :: VECTSP_7:14

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

proof end;

theorem Th15: :: VECTSP_7:15

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

proof end;

theorem Th16: :: VECTSP_7:16

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂
for b₄ being strict Subspace of b₂ st b₃ = the carrier of b₄ holds
Lin b₃ = b₄

proof end;

theorem Th17: :: VECTSP_7:17

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃ being Subset of b₂ st b₃ = the carrier of b₂ holds
Lin b₃ = b₂

proof end;

theorem Th18: :: VECTSP_7:18

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

proof end;

theorem Th19: :: VECTSP_7:19

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

proof end;

theorem Th20: :: VECTSP_7:20

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

proof end;

theorem Th21: :: VECTSP_7:21

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

proof end;

theorem Th22: :: VECTSP_7:22

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
ex b₄ being Subset of b₂ st
( b₃ c= b₄ & b₄ is linearly-independent & Lin b₄ = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) )

proof end;

theorem Th23: :: VECTSP_7:23

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂ st Lin b₃ = b₂ holds
ex b₄ being Subset of b₂ st
( b₄ c= b₃ & b₄ is linearly-independent & Lin b₄ = b₂ )

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
mode Basis of c₂ -> Subset of a₂ means :Def3: :: VECTSP_7:def 3
( a₃ is linearly-independent & Lin a₃ = VectSpStr(# the carrier of a₂,the add of a₂,the Zero of a₂,the lmult of a₂ #) );
existence

proof end;

end;

:: deftheorem Def3 defines Basis VECTSP_7:def 3 :

theorem Th24: :: VECTSP_7:24

canceled;

theorem Th25: :: VECTSP_7:25

canceled;

theorem Th26: :: VECTSP_7:26

canceled;

theorem Th27: :: VECTSP_7:27

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
ex b₄ being Basis of b₂ st b₃ c= b₄

proof end;

theorem Th28: :: VECTSP_7:28

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subset of b₂ st Lin b₃ = b₂ holds
ex b₄ being Basis of b₂ st b₄ c= b₃

proof end;