:: by Mariusz \.Zynel

::

:: Received October 6, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

registration

let S be non empty 1-sorted ;

existence

not for b_{1} being Subset of S holds b_{1} is empty

end;
existence

not for b

proof end;

Lm1: for X, x being set st x in X holds

(X \ {x}) \/ {x} = X

proof end;

:: More On Linear Combinations

theorem Th1: :: VECTSP_9:1

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for F, G being FinSequence of the carrier of V

for P being Permutation of (dom F) st G = F * P holds

Sum (L (#) F) = Sum (L (#) G)

for V being VectSp of GF

for L being Linear_Combination of V

for F, G being FinSequence of the carrier of V

for P being Permutation of (dom F) st G = F * P holds

Sum (L (#) F) = Sum (L (#) G)

proof end;

theorem Th2: :: VECTSP_9:2

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

for V being VectSp of GF

for L being Linear_Combination of V

for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

proof end;

theorem Th3: :: VECTSP_9:3

for GF being Field

for V being VectSp of GF

for F being FinSequence of the carrier of V st F is one-to-one holds

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

for V being VectSp of GF

for F being FinSequence of the carrier of V st F is one-to-one holds

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

proof end;

theorem Th4: :: VECTSP_9:4

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for F being FinSequence of the carrier of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

for V being VectSp of GF

for L being Linear_Combination of V

for F being FinSequence of the carrier of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

proof end;

theorem Th5: :: VECTSP_9:5

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum (L (#) F) = Sum K

for V being VectSp of GF

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum (L (#) F) = Sum K

proof end;

theorem Th6: :: VECTSP_9:6

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

for V being VectSp of GF

for L being Linear_Combination of V

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

proof end;

theorem Th7: :: VECTSP_9:7

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

for V being VectSp of GF

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

proof end;

theorem Th8: :: VECTSP_9:8

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

for V being VectSp of GF

for W being Subspace of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem Th9: :: VECTSP_9:9

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

for V being VectSp of GF

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

proof end;

:: More On Linear Independence & Basis

theorem Th10: :: VECTSP_9:10

for GF being Field

for V being VectSp of GF

for I being Basis of V

for v being Vector of V holds v in Lin I

for V being VectSp of GF

for I being Basis of V

for v being Vector of V holds v in Lin I

proof end;

registration

let GF be Field;

let V be VectSp of GF;

existence

ex b_{1} being Subset of V st b_{1} is linearly-independent

end;
let V be VectSp of GF;

existence

ex b

proof end;

theorem Th11: :: VECTSP_9:11

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for A being Subset of W st A is linearly-independent holds

A is linearly-independent Subset of V

for V being VectSp of GF

for W being Subspace of V

for A being Subset of W st A is linearly-independent holds

A is linearly-independent Subset of V

proof end;

theorem Th12: :: VECTSP_9:12

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

proof end;

theorem Th13: :: VECTSP_9:13

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for A being Basis of W ex B being Basis of V st A c= B

for V being VectSp of GF

for W being Subspace of V

for A being Basis of W ex B being Basis of V st A c= B

proof end;

theorem Th14: :: VECTSP_9:14

for GF being Field

for V being VectSp of GF

for A being Subset of V st A is linearly-independent holds

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

for V being VectSp of GF

for A being Subset of V st A is linearly-independent holds

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

proof end;

theorem Th15: :: VECTSP_9:15

for GF being Field

for V being VectSp of GF

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

for V being VectSp of GF

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

proof end;

theorem Th16: :: VECTSP_9:16

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Subspace of W

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Subspace of W

proof end;

theorem Th17: :: VECTSP_9:17

for GF being Field

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

for V being VectSp of GF

for W being Subspace of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

proof end;

begin

::

:: Steinitz Theorem

::

:: Exchange Lemma

:: Steinitz Theorem

::

:: Exchange Lemma

theorem Th18: :: VECTSP_9:18

for GF being Field

for V being VectSp of GF

for A, B being finite Subset of V

for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being Vector of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

for V being VectSp of GF

for A, B being finite Subset of V

for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being Vector of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

proof end;

theorem Th19: :: VECTSP_9:19

for GF being Field

for V being VectSp of GF

for A, B being finite Subset of V st VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds

( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )

for V being VectSp of GF

for A, B being finite Subset of V st VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds

( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )

proof end;

begin

::

:: Finite-Dimensional Vector Spaces

::

:: Finite-Dimensional Vector Spaces

::

theorem Th20: :: VECTSP_9:20

for GF being Field

for V being VectSp of GF st V is finite-dimensional holds

for I being Basis of V holds I is finite

for V being VectSp of GF st V is finite-dimensional holds

for I being Basis of V holds I is finite

proof end;

theorem :: VECTSP_9:21

for GF being Field

for V being VectSp of GF st V is finite-dimensional holds

for A being Subset of V st A is linearly-independent holds

A is finite

for V being VectSp of GF st V is finite-dimensional holds

for A being Subset of V st A is linearly-independent holds

A is finite

proof end;

theorem Th22: :: VECTSP_9:22

for GF being Field

for V being VectSp of GF st V is finite-dimensional holds

for A, B being Basis of V holds card A = card B

for V being VectSp of GF st V is finite-dimensional holds

for A, B being Basis of V holds card A = card B

proof end;

theorem Th24: :: VECTSP_9:24

for GF being Field

for V being VectSp of GF

for W being Subspace of V st V is finite-dimensional holds

W is finite-dimensional

for V being VectSp of GF

for W being Subspace of V st V is finite-dimensional holds

W is finite-dimensional

proof end;

registration

let GF be Field;

let V be VectSp of GF;

ex b_{1} being Subspace of V st

( b_{1} is strict & b_{1} is finite-dimensional )

end;
let V be VectSp of GF;

cluster non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() finite-dimensional for Subspace of V;

existence ex b

( b

proof end;

registration

let GF be Field;

let V be finite-dimensional VectSp of GF;

correctness

coherence

for b_{1} being Subspace of V holds b_{1} is finite-dimensional ;

by Th24;

end;
let V be finite-dimensional VectSp of GF;

correctness

coherence

for b

by Th24;

registration

let GF be Field;

let V be finite-dimensional VectSp of GF;

ex b_{1} being Subspace of V st b_{1} is strict

end;
let V be finite-dimensional VectSp of GF;

cluster non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() finite-dimensional for Subspace of V;

existence ex b

proof end;

begin

::

:: Dimension of a Vector Space

::

:: Dimension of a Vector Space

::

definition

let GF be Field;

let V be VectSp of GF;

assume A1: V is finite-dimensional ;

existence

ex b_{1} being Nat st

for I being Basis of V holds b_{1} = card I

for b_{1}, b_{2} being Nat st ( for I being Basis of V holds b_{1} = card I ) & ( for I being Basis of V holds b_{2} = card I ) holds

b_{1} = b_{2}

end;
let V be VectSp of GF;

assume A1: V is finite-dimensional ;

existence

ex b

for I being Basis of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines dim VECTSP_9:def 1 :

for GF being Field

for V being VectSp of GF st V is finite-dimensional holds

for b_{3} being Nat holds

( b_{3} = dim V iff for I being Basis of V holds b_{3} = card I );

for GF being Field

for V being VectSp of GF st V is finite-dimensional holds

for b

( b

theorem Th25: :: VECTSP_9:25

for GF being Field

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds dim W <= dim V

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds dim W <= dim V

proof end;

theorem Th26: :: VECTSP_9:26

for GF being Field

for V being finite-dimensional VectSp of GF

for A being Subset of V st A is linearly-independent holds

card A = dim (Lin A)

for V being finite-dimensional VectSp of GF

for A being Subset of V st A is linearly-independent holds

card A = dim (Lin A)

proof end;

theorem :: VECTSP_9:28

for GF being Field

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds

( dim V = dim W iff (Omega). V = (Omega). W )

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds

( dim V = dim W iff (Omega). V = (Omega). W )

proof end;

theorem Th29: :: VECTSP_9:29

for GF being Field

for V being finite-dimensional VectSp of GF holds

( dim V = 0 iff (Omega). V = (0). V )

for V being finite-dimensional VectSp of GF holds

( dim V = 0 iff (Omega). V = (0). V )

proof end;

theorem :: VECTSP_9:30

for GF being Field

for V being finite-dimensional VectSp of GF holds

( dim V = 1 iff ex v being Vector of V st

( v <> 0. V & (Omega). V = Lin {v} ) )

for V being finite-dimensional VectSp of GF holds

( dim V = 1 iff ex v being Vector of V st

( v <> 0. V & (Omega). V = Lin {v} ) )

proof end;

theorem :: VECTSP_9:31

for GF being Field

for V being finite-dimensional VectSp of GF holds

( dim V = 2 iff ex u, v being Vector of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

for V being finite-dimensional VectSp of GF holds

( dim V = 2 iff ex u, v being Vector of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

proof end;

theorem Th32: :: VECTSP_9:32

for GF being Field

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)

proof end;

theorem :: VECTSP_9:33

for GF being Field

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)

proof end;

theorem :: VECTSP_9:34

for GF being Field

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

dim V = (dim W1) + (dim W2)

for V being finite-dimensional VectSp of GF

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

dim V = (dim W1) + (dim W2)

proof end;

Lm2: for GF being Field

for n being Nat

for V being finite-dimensional VectSp of GF st n <= dim V holds

ex W being strict Subspace of V st dim W = n

proof end;

theorem :: VECTSP_9:35

definition

let GF be Field;

let V be finite-dimensional VectSp of GF;

let n be Nat;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex W being strict Subspace of V st

( W = x & dim W = n ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) & ( for x being set holds

( x in b_{2} iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) holds

b_{1} = b_{2}

end;
let V be finite-dimensional VectSp of GF;

let n be Nat;

func n Subspaces_of V -> set means :Def2: :: VECTSP_9:def 2

for x being set holds

( x in it iff ex W being strict Subspace of V st

( W = x & dim W = n ) );

existence for x being set holds

( x in it iff ex W being strict Subspace of V st

( W = x & dim W = n ) );

ex b

for x being set holds

( x in b

( W = x & dim W = n ) )

proof end;

uniqueness for b

( x in b

( W = x & dim W = n ) ) ) & ( for x being set holds

( x in b

( W = x & dim W = n ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Subspaces_of VECTSP_9:def 2 :

for GF being Field

for V being finite-dimensional VectSp of GF

for n being Nat

for b_{4} being set holds

( b_{4} = n Subspaces_of V iff for x being set holds

( x in b_{4} iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) );

for GF being Field

for V being finite-dimensional VectSp of GF

for n being Nat

for b

( b

( x in b

( W = x & dim W = n ) ) );

theorem :: VECTSP_9:36

for GF being Field

for n being Nat

for V being finite-dimensional VectSp of GF st n <= dim V holds

not n Subspaces_of V is empty

for n being Nat

for V being finite-dimensional VectSp of GF st n <= dim V holds

not n Subspaces_of V is empty

proof end;

theorem :: VECTSP_9:37

for GF being Field

for n being Nat

for V being finite-dimensional VectSp of GF st dim V < n holds

n Subspaces_of V = {}

for n being Nat

for V being finite-dimensional VectSp of GF st dim V < n holds

n Subspaces_of V = {}

proof end;

theorem :: VECTSP_9:38

for GF being Field

for n being Nat

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V

for n being Nat

for V being finite-dimensional VectSp of GF

for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V

proof end;

:: Preliminaries

::