:: RLVECT_3 semantic presentation

Lemma1: for b₁ being RealLinearSpace
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Function of the carrier of b₁, REAL holds b₄ (#) (b₂ ^ b₃) = (b₄ (#) b₂) ^ (b₄ (#) b₃)

proof end;

theorem Th1: :: RLVECT_3:1

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃)

proof end;

theorem Th2: :: RLVECT_3:2

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being Linear_Combination of b₂ holds Sum (b₁ * b₃) = b₁ * (Sum b₃)

proof end;

theorem Th3: :: RLVECT_3:3

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds Sum (- b₂) = - (Sum b₂)

proof end;

theorem Th4: :: RLVECT_3:4

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds Sum (b₂ - b₃) = (Sum b₂) - (Sum b₃)

proof end;

definition

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

end;

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

notation

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
antonym linearly-dependent c₂ for linearly-independent c₂;

end;

theorem Th5: :: RLVECT_3:5

canceled;

theorem Th6: :: RLVECT_3:6

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

proof end;

theorem Th7: :: RLVECT_3:7

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

proof end;

theorem Th8: :: RLVECT_3:8

for b₁ being RealLinearSpace holds {} the carrier of b₁ is linearly-independent

proof end;

registration

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

proof end;

end;

theorem Th9: :: RLVECT_3:9

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds
( {b₂} is linearly-independent iff b₂ <> 0. b₁ )

proof end;

theorem Th10: :: RLVECT_3:10

for b₁ being RealLinearSpace holds not {(0. b₁)} is linearly-independent by Th9;

theorem Th11: :: RLVECT_3:11

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st {b₂,b₃} is linearly-independent holds
( b₂ <> 0. b₁ & b₃ <> 0. b₁ )

proof end;

theorem Th12: :: RLVECT_3:12

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds
( not {b₂,(0. b₁)} is linearly-independent & not {(0. b₁),b₂} is linearly-independent ) by Th11;

theorem Th13: :: RLVECT_3:13

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( b₂ <> b₃ & {b₂,b₃} is linearly-independent iff ( b₃ <> 0. b₁ & ( for b₄ being Real holds b₂ <> b₄ * b₃ ) ) )

proof end;

theorem Th14: :: RLVECT_3:14

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( ( b₂ <> b₃ & {b₂,b₃} is linearly-independent ) iff for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
func Lin c₂ -> strict Subspace of a₁ means :Def2: :: RLVECT_3:def 2
the carrier of a₃ = { (Sum b₁) where B is Linear_Combination of a₂ : verum } ;
existence

proof end;

uniqueness by RLSUB_1:38;

end;

:: deftheorem Def2 defines Lin RLVECT_3:def 2 :

theorem Th15: :: RLVECT_3:15

canceled;

theorem Th16: :: RLVECT_3:16

canceled;

theorem Th17: :: RLVECT_3:17

for b₁ being set
for b₂ being RealLinearSpace
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 Th18: :: RLVECT_3:18

for b₁ being set
for b₂ being RealLinearSpace
for b₃ being Subset of b₂ st b₁ in b₃ holds
b₁ in Lin b₃

proof end;

Lemma15: for b₁ being set
for b₂ being RealLinearSpace holds
( b₁ in (0). b₂ iff b₁ = 0. b₂ )

proof end;

theorem Th19: :: RLVECT_3:19

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

proof end;

theorem Th20: :: RLVECT_3:20

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

proof end;

theorem Th21: :: RLVECT_3:21

for b₁ being RealLinearSpace
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 Th22: :: RLVECT_3:22

for b₁ being strict RealLinearSpace
for b₂ being Subset of b₁ st b₂ = the carrier of b₁ holds
Lin b₂ = b₁

proof end;

Lemma17: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ /\ b₄ is Subspace of b₃

proof end;

Lemma18: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ & b₂ is Subspace of b₄ holds
b₂ is Subspace of b₃ /\ b₄

proof end;

Lemma19: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ is Subspace of b₃ + b₄

proof end;

Lemma20: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ & b₄ is Subspace of b₃ holds
b₂ + b₄ is Subspace of b₃

proof end;

theorem Th23: :: RLVECT_3:23

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

proof end;

theorem Th24: :: RLVECT_3:24

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

proof end;

theorem Th25: :: RLVECT_3:25

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

proof end;

theorem Th26: :: RLVECT_3:26

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

proof end;

Lemma22: for b₁ being non empty set
for b₂ being Choice_Function of b₁ st not {} in b₁ holds
( dom b₂ = b₁ & rng b₂ c= union b₁ )

proof end;

theorem Th27: :: RLVECT_3:27

for b₁ being RealLinearSpace
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₃ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) )

proof end;

theorem Th28: :: RLVECT_3:28

for b₁ being RealLinearSpace
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 RealLinearSpace;
mode Basis of c₁ -> Subset of a₁ means :Def3: :: RLVECT_3:def 3
( a₂ is linearly-independent & Lin a₂ = RLSStruct(# the carrier of a₁,the Zero of a₁,the add of a₁,the Mult of a₁ #) );
existence

proof end;

end;

:: deftheorem Def3 defines Basis RLVECT_3:def 3 :

theorem Th29: :: RLVECT_3:29

canceled;

theorem Th30: :: RLVECT_3:30

canceled;

theorem Th31: :: RLVECT_3:31

canceled;

theorem Th32: :: RLVECT_3:32

for b₁ being strict RealLinearSpace
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 Th33: :: RLVECT_3:33

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st Lin b₂ = b₁ holds
ex b₃ being Basis of b₁ st b₃ c= b₂

proof end;

theorem Th34: :: RLVECT_3:34

canceled;

theorem Th35: :: RLVECT_3:35

for b₁ being non empty set
for b₂ being Choice_Function of b₁ st not {} in b₁ holds
( dom b₂ = b₁ & rng b₂ c= union b₁ ) by Lemma22;

theorem Th36: :: RLVECT_3:36

for b₁ being set
for b₂ being RealLinearSpace holds
( b₁ in (0). b₂ iff b₁ = 0. b₂ ) by Lemma15;

theorem Th37: :: RLVECT_3:37

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ /\ b₄ is Subspace of b₃ by Lemma17;

theorem Th38: :: RLVECT_3:38

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ & b₂ is Subspace of b₄ holds
b₂ is Subspace of b₃ /\ b₄ by Lemma18;

theorem Th39: :: RLVECT_3:39

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ & b₄ is Subspace of b₃ holds
b₂ + b₄ is Subspace of b₃ by Lemma20;

theorem Th40: :: RLVECT_3:40

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ is Subspace of b₃ + b₄ by Lemma19;

theorem Th41: :: RLVECT_3:41

for b₁ being RealLinearSpace
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Function of the carrier of b₁, REAL holds b₄ (#) (b₂ ^ b₃) = (b₄ (#) b₂) ^ (b₄ (#) b₃) by Lemma1;