:: VECTSP_9 semantic presentation

registration

let c₁ be non empty 1-sorted ;
cluster non empty Element of K40(the carrier of a₁);
existence

proof end;

end;

theorem Th1: :: VECTSP_9:1

for b₁ being Nat
for b₂ being finite set st b₁ <= card b₂ holds
ex b₃ being finite Subset of b₂ st Card b₃ = b₁

proof end;

theorem Th2: :: VECTSP_9:2

for b₁ being set
for b₂ being Function st b₂ is one-to-one & b₁ in rng b₂ holds
Card (b₂ " {b₁}) = 1

proof end;

theorem Th3: :: VECTSP_9:3

for b₁ being set
for b₂ being Function st not b₁ in rng b₂ holds
Card (b₂ " {b₁}) = 0 by CARD_1:78, FUNCT_1:142;

theorem Th4: :: VECTSP_9:4

for b₁, b₂ being Function st rng b₁ = rng b₂ & b₁ is one-to-one & b₂ is one-to-one holds
b₁,b₂ are_fiberwise_equipotent

proof end;

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

proof end;

theorem Th5: :: VECTSP_9:5

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:6

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

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:8

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:9

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:10

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:11

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:12

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:13

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:14

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Basis of b₂
for b₄ being Vector of b₂ holds b₄ in Lin b₃

proof end;

theorem Th15: :: VECTSP_9:15

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:16

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:17

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:18

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:19

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:20

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:21

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:22

for b₁ being Field
for b₂ being VectSp of b₁
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: :: VECTSP_9:23

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄ being finite Subset of b₂ st VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult 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₄) & VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) = Lin (b₄ \/ b₅) ) )

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
redefine attr a₂ is finite-dimensional means :Def1: :: VECTSP_9:def 1
ex b₁ being finite Subset of a₂ st b₁ is Basis of a₂;
compatibility by MATRLIN:def 3;

end;

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

theorem Th24: :: VECTSP_9:24

for b₁ being Field
for b₂ being VectSp of b₁ st b₂ is finite-dimensional holds
for b₃ being Basis of b₂ holds b₃ is finite

proof end;

theorem Th25: :: VECTSP_9:25

for b₁ being Field
for b₂ being VectSp of b₁ 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: :: VECTSP_9:26

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

proof end;

theorem Th27: :: VECTSP_9:27

for b₁ being Field
for b₂ being VectSp of b₁ holds (0). b₂ is finite-dimensional

proof end;

theorem Th28: :: VECTSP_9:28

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂ st b₂ is finite-dimensional holds
b₃ is finite-dimensional

proof end;

registration

let c₁ be Field;
let c₂ be VectSp of c₁;
cluster strict finite-dimensional Subspace of a₂;
existence

proof end;

end;

registration

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

end;

registration

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
cluster strict finite-dimensional Subspace of a₂;
existence

proof end;

end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
assume E29: c₂ is finite-dimensional ;
func dim c₂ -> Nat means :Def2: :: VECTSP_9:def 2
for b₁ being Basis of a₂ holds a₃ = Card b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines dim VECTSP_9:def 2 :

theorem Th29: :: VECTSP_9:29

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Subspace of b₂ holds dim b₃ <= dim b₂

proof end;

theorem Th30: :: VECTSP_9:30

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

proof end;

theorem Th31: :: VECTSP_9:31

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁ holds dim b₂ = dim ((Omega). b₂)

proof end;

theorem Th32: :: VECTSP_9:32

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

proof end;

theorem Th33: :: VECTSP_9:33

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁ holds
( dim b₂ = 0 iff (Omega). b₂ = (0). b₂ )

proof end;

theorem Th34: :: VECTSP_9:34

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

proof end;

theorem Th35: :: VECTSP_9:35

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁ 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: :: VECTSP_9:36

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

proof end;

theorem Th37: :: VECTSP_9:37

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

proof end;

theorem Th38: :: VECTSP_9:38

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
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;

Lemma35: for b₁ being Field
for b₂ being Nat
for b₃ being finite-dimensional VectSp of b₁ st b₂ <= dim b₃ holds
ex b₄ being strict Subspace of b₃ st dim b₄ = b₂

proof end;

theorem Th39: :: VECTSP_9:39

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

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃ be Nat;
func c₃ Subspaces_of c₂ -> set means :Def3: :: VECTSP_9:def 3
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 Def3 defines Subspaces_of VECTSP_9:def 3 :

theorem Th40: :: VECTSP_9:40

for b₁ being Field
for b₂ being Nat
for b₃ being finite-dimensional VectSp of b₁ st b₂ <= dim b₃ holds
not b₂ Subspaces_of b₃ is empty

proof end;

theorem Th41: :: VECTSP_9:41

for b₁ being Field
for b₂ being Nat
for b₃ being finite-dimensional VectSp of b₁ st dim b₃ < b₂ holds
b₂ Subspaces_of b₃ = {}

proof end;

theorem Th42: :: VECTSP_9:42

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

proof end;