:: RLVECT_5 semantic presentation

theorem Th1: :: RLVECT_5:1

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

proof end;

theorem Th2: :: RLVECT_5:2

for b₁ being 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 Th3: :: RLVECT_5:3

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being VECTOR of b₁ holds
( b₃ in Carrier b₂ iff ex b₄ being VECTOR of b₁ st
( b₃ = b₄ & b₂ . b₄ <> 0 ) )

proof end;

Lemma4: for b₁, b₂ being set st b₂ in b₁ holds
(b₁ \ {b₂}) \/ {b₂} = b₁

proof end;

theorem Th4: :: RLVECT_5:4

canceled;

theorem Th5: :: RLVECT_5:5

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃, b₄ being FinSequence of the carrier of b₁
for b₅ being Permutation of dom b₃ st b₄ = b₃ * b₅ holds
Sum (b₂ (#) b₃) = Sum (b₂ (#) b₄)

proof end;

theorem Th6: :: RLVECT_5:6

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being FinSequence of the carrier of b₁ st Carrier b₂ misses rng b₃ holds
Sum (b₂ (#) b₃) = 0. b₁

proof end;

theorem Th7: :: RLVECT_5:7

for b₁ being RealLinearSpace
for b₂ being FinSequence of the carrier of b₁ st b₂ is one-to-one holds
for b₃ being Linear_Combination of b₁ st Carrier b₃ c= rng b₂ holds
Sum (b₃ (#) b₂) = Sum b₃

proof end;

theorem Th8: :: RLVECT_5:8

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being FinSequence of the carrier of b₁ ex b₄ being Linear_Combination of b₁ st
( Carrier b₄ = (rng b₃) /\ (Carrier b₂) & b₂ (#) b₃ = b₄ (#) b₃ )

proof end;

theorem Th9: :: RLVECT_5:9

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being Subset of b₁
for b₄ being FinSequence of the carrier of b₁ st rng b₄ c= the carrier of (Lin b₃) holds
ex b₅ being Linear_Combination of b₃ st Sum (b₂ (#) b₄) = Sum b₅

proof end;

theorem Th10: :: RLVECT_5:10

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being Subset of b₁ st Carrier b₂ c= the carrier of (Lin b₃) holds
ex b₄ being Linear_Combination of b₃ st Sum b₂ = Sum b₄

proof end;

theorem Th11: :: RLVECT_5:11

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Linear_Combination of b₁ st Carrier b₃ c= the carrier of b₂ holds
for b₄ being Linear_Combination of b₂ st b₄ = b₃ | the carrier of b₂ holds
( Carrier b₃ = Carrier b₄ & Sum b₃ = Sum b₄ )

proof end;

theorem Th12: :: RLVECT_5:12

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Linear_Combination of b₂ ex b₄ being Linear_Combination of b₁ st
( Carrier b₃ = Carrier b₄ & Sum b₃ = Sum b₄ )

proof end;

theorem Th13: :: RLVECT_5:13

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Linear_Combination of b₁ st Carrier b₃ c= the carrier of b₂ holds
ex b₄ being Linear_Combination of b₂ st
( Carrier b₄ = Carrier b₃ & Sum b₄ = Sum b₃ )

proof end;

theorem Th14: :: RLVECT_5:14

for b₁ being RealLinearSpace
for b₂ being Basis of b₁
for b₃ being VECTOR of b₁ holds b₃ in Lin b₂

proof end;

theorem Th15: :: RLVECT_5:15

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Subset of b₂ st b₃ is linearly-independent holds
b₃ is linearly-independent Subset of b₁

proof end;

theorem Th16: :: RLVECT_5:16

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

proof end;

theorem Th17: :: RLVECT_5:17

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Basis of b₂ ex b₄ being Basis of b₁ st b₃ c= b₄

proof end;

theorem Th18: :: RLVECT_5:18

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ is linearly-independent holds
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
for b₄ being Subset of b₁ st b₄ = b₂ \ {b₃} holds
not b₃ in Lin b₄

proof end;

theorem Th19: :: RLVECT_5:19

for b₁ being RealLinearSpace
for b₂ being Basis of b₁
for b₃ being non empty Subset of b₁ st b₃ misses b₂ holds
for b₄ being Subset of b₁ st b₄ = b₂ \/ b₃ holds
not b₄ is linearly-independent

proof end;

theorem Th20: :: RLVECT_5:20

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

proof end;

theorem Th21: :: RLVECT_5:21

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Lin b₃ = Lin b₄

proof end;

theorem Th22: :: RLVECT_5:22

for b₁ being RealLinearSpace
for b₂, b₃ being finite Subset of b₁
for b₄ being VECTOR of b₁ st b₄ in Lin (b₂ \/ b₃) & not b₄ in Lin b₃ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₅ in Lin (((b₂ \/ b₃) \ {b₅}) \/ {b₄}) )

proof end;

theorem Th23: :: RLVECT_5:23

for b₁ being RealLinearSpace
for b₂, b₃ being finite Subset of b₁ st RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) = Lin b₂ & b₃ is linearly-independent holds
( card b₃ <= card b₂ & ex b₄ being finite Subset of b₁ st
( b₄ c= b₂ & card b₄ = (card b₂) - (card b₃) & RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) = Lin (b₃ \/ b₄) ) )

proof end;

definition

let c₁ be RealLinearSpace;
attr a₁ is finite-dimensional means :Def1: :: RLVECT_5:def 1
ex b₁ being finite Subset of a₁ st b₁ is Basis of a₁;

end;

:: deftheorem Def1 defines finite-dimensional RLVECT_5:def 1 :

registration

cluster strict finite-dimensional RLSStruct ;
existence

proof end;

end;

definition

let c₁ be RealLinearSpace;
redefine attr a₁ is finite-dimensional means :Def2: :: RLVECT_5:def 2
ex b₁ being finite Subset of a₁ st b₁ is Basis of a₁;
compatibility by Def1;

end;

:: deftheorem Def2 defines finite-dimensional RLVECT_5:def 2 :

theorem Th24: :: RLVECT_5:24

for b₁ being RealLinearSpace st b₁ is finite-dimensional holds
for b₂ being Basis of b₁ holds b₂ is finite

proof end;

theorem Th25: :: RLVECT_5:25

for b₁ being RealLinearSpace st b₁ is finite-dimensional holds
for b₂ being Subset of b₁ st b₂ is linearly-independent holds
b₂ is finite

proof end;

theorem Th26: :: RLVECT_5:26

for b₁ being RealLinearSpace st b₁ is finite-dimensional holds
for b₂, b₃ being Basis of b₁ holds Card b₂ = Card b₃

proof end;

theorem Th27: :: RLVECT_5:27

for b₁ being RealLinearSpace holds (0). b₁ is finite-dimensional

proof end;

theorem Th28: :: RLVECT_5:28

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ st b₁ is finite-dimensional holds
b₂ is finite-dimensional

proof end;

registration

let c₁ be RealLinearSpace;
cluster strict finite-dimensional Subspace of a₁;
existence

proof end;

end;

registration

let c₁ be finite-dimensional RealLinearSpace;
cluster -> finite-dimensional Subspace of a₁;
correctness by Th28;

end;

registration

let c₁ be finite-dimensional RealLinearSpace;
cluster strict finite-dimensional Subspace of a₁;
existence

proof end;

end;

definition

let c₁ be RealLinearSpace;
assume E30: c₁ is finite-dimensional ;
func dim c₁ -> Nat means :Def3: :: RLVECT_5:def 3
for b₁ being Basis of a₁ holds a₂ = Card b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines dim RLVECT_5:def 3 :

theorem Th29: :: RLVECT_5:29

for b₁ being finite-dimensional RealLinearSpace
for b₂ being Subspace of b₁ holds dim b₂ <= dim b₁

proof end;

theorem Th30: :: RLVECT_5:30

for b₁ being finite-dimensional RealLinearSpace
for b₂ being Subset of b₁ st b₂ is linearly-independent holds
Card b₂ = dim (Lin b₂)

proof end;

theorem Th31: :: RLVECT_5:31

for b₁ being finite-dimensional RealLinearSpace holds dim b₁ = dim ((Omega). b₁)

proof end;

theorem Th32: :: RLVECT_5:32

for b₁ being finite-dimensional RealLinearSpace
for b₂ being Subspace of b₁ holds
( dim b₁ = dim b₂ iff (Omega). b₁ = (Omega). b₂ )

proof end;

theorem Th33: :: RLVECT_5:33

for b₁ being finite-dimensional RealLinearSpace holds
( dim b₁ = 0 iff (Omega). b₁ = (0). b₁ )

proof end;

theorem Th34: :: RLVECT_5:34

for b₁ being finite-dimensional RealLinearSpace holds
( dim b₁ = 1 iff ex b₂ being VECTOR of b₁ st
( b₂ <> 0. b₁ & (Omega). b₁ = Lin {b₂} ) )

proof end;

theorem Th35: :: RLVECT_5:35

for b₁ being finite-dimensional RealLinearSpace holds
( dim b₁ = 2 iff ex b₂, b₃ being VECTOR of b₁ st
( b₂ <> b₃ & {b₂,b₃} is linearly-independent & (Omega). b₁ = Lin {b₂,b₃} ) )

proof end;

theorem Th36: :: RLVECT_5:36

for b₁ being finite-dimensional RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds (dim (b₂ + b₃)) + (dim (b₂ /\ b₃)) = (dim b₂) + (dim b₃)

proof end;

theorem Th37: :: RLVECT_5:37

for b₁ being finite-dimensional RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds dim (b₂ /\ b₃) >= ((dim b₂) + (dim b₃)) - (dim b₁)

proof end;

theorem Th38: :: RLVECT_5:38

for b₁ being finite-dimensional RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
dim b₁ = (dim b₂) + (dim b₃)

proof end;

Lemma36: for b₁ being Nat
for b₂ being finite-dimensional RealLinearSpace st b₁ <= dim b₂ holds
ex b₃ being strict Subspace of b₂ st dim b₃ = b₁

proof end;

theorem Th39: :: RLVECT_5:39

for b₁ being Nat
for b₂ being finite-dimensional RealLinearSpace holds
( b₁ <= dim b₂ iff ex b₃ being strict Subspace of b₂ st dim b₃ = b₁ ) by Lemma36, Th29;

definition

let c₁ be finite-dimensional RealLinearSpace;
let c₂ be Nat;
func c₂ Subspaces_of c₁ -> set means :Def4: :: RLVECT_5:def 4
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being strict Subspace of a₁ st
( b₂ = b₁ & dim b₂ = a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Subspaces_of RLVECT_5:def 4 :

theorem Th40: :: RLVECT_5:40

for b₁ being Nat
for b₂ being finite-dimensional RealLinearSpace st b₁ <= dim b₂ holds
not b₁ Subspaces_of b₂ is empty

proof end;

theorem Th41: :: RLVECT_5:41

for b₁ being Nat
for b₂ being finite-dimensional RealLinearSpace st dim b₂ < b₁ holds
b₁ Subspaces_of b₂ = {}

proof end;

theorem Th42: :: RLVECT_5:42

for b₁ being Nat
for b₂ being finite-dimensional RealLinearSpace
for b₃ being Subspace of b₂ holds b₁ Subspaces_of b₃ c= b₁ Subspaces_of b₂

proof end;