:: Dimension of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

theorem Th1: :: RUSUB_4:1
for V being RealUnitarySpace
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;

Lm1: for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
proof end;

Lm2: for X, x being set st not x in X holds
X \ {x} = X
proof end;

theorem Th2: :: RUSUB_4:2
for V being RealUnitarySpace
for A, B being finite Subset of V st UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar 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) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
proof end;

definition
let V be RealUnitarySpace;
attr V is finite-dimensional means :Def1: :: RUSUB_4:def 1
 ex A being finite Subset of V st A is Basis of V;
end;

:: deftheorem Def1 defines finite-dimensional RUSUB_4:def 1 :
for V being RealUnitarySpace holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

registration
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for UNITSTR ;
existence
ex b1 being RealUnitarySpace st
( b1 is strict & b1 is finite-dimensional )
proof end;
end;

theorem Th3: :: RUSUB_4:3
for V being RealUnitarySpace st V is finite-dimensional holds
for I being Basis of V holds I is finite
proof end;

theorem :: RUSUB_4:4
for V being RealUnitarySpace
for A being Subset of V st V is finite-dimensional & A is linearly-independent holds
A is finite
proof end;

theorem Th5: :: RUSUB_4:5
for V being RealUnitarySpace
for A, B being Basis of V st V is finite-dimensional holds
card A = card B
proof end;

theorem Th6: :: RUSUB_4:6
for V being RealUnitarySpace holds (0). V is finite-dimensional
proof end;

theorem Th7: :: RUSUB_4:7
for V being RealUnitarySpace
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
proof end;

registration
let V be RealUnitarySpace;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st
( b1 is finite-dimensional & b1 is strict )
proof end;
end;

registration
let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is finite-dimensional ;
by Th7;
end;

registration
let V be finite-dimensional RealUnitarySpace;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof end;
end;

begin

definition
let V be RealUnitarySpace;
assume A1: V is finite-dimensional ;
func dim V -> Element of NAT means :Def2: :: RUSUB_4:def 2
 for I being Basis of V holds it = card I;
existence
ex b1 being Element of NAT st
for I being Basis of V holds b1 = card I
proof end;
uniqueness
for b1, b2 being Element of NAT st ( for I being Basis of V holds b1 = card I ) & ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines dim RUSUB_4:def 2 :
for V being RealUnitarySpace st V is finite-dimensional holds
for b2 being Element of NAT holds
( b2 = dim V iff for I being Basis of V holds b2 = card I );

theorem Th8: :: RUSUB_4:8
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V holds dim W <= dim V
proof end;

theorem Th9: :: RUSUB_4:9
for V being finite-dimensional RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
proof end;

theorem Th10: :: RUSUB_4:10
for V being finite-dimensional RealUnitarySpace holds dim V = dim ((Omega). V)
proof end;

theorem :: RUSUB_4:11
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
proof end;

theorem Th12: :: RUSUB_4:12
for V being finite-dimensional RealUnitarySpace holds
( dim V = 0 iff (Omega). V = (0). V )
proof end;

theorem :: RUSUB_4:13
for V being finite-dimensional RealUnitarySpace holds
( dim V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
proof end;

theorem :: RUSUB_4:14
for V being finite-dimensional RealUnitarySpace 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 Th15: :: RUSUB_4:15
for V being finite-dimensional RealUnitarySpace
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
proof end;

theorem :: RUSUB_4:16
for V being finite-dimensional RealUnitarySpace
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
proof end;

theorem :: RUSUB_4:17
for V being finite-dimensional RealUnitarySpace
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;

begin

Lm3: for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
proof end;

theorem :: RUSUB_4:18
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V
for n being Element of NAT holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm3, Th8;

definition
let V be finite-dimensional RealUnitarySpace;
let n be Element of NAT ;
func n Subspaces_of V -> set means :Def3: :: RUSUB_4:def 3
 for x being set holds
( x in it iff ex W being strict Subspace of V st
( W = x & dim W = n ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Subspaces_of RUSUB_4:def 3 :
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT
for b3 being set holds
( b3 = n Subspaces_of V iff for x being set holds
( x in b3 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );

theorem :: RUSUB_4:19
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
not n Subspaces_of V is empty
proof end;

theorem :: RUSUB_4:20
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st dim V < n holds
n Subspaces_of V = {}
proof end;

theorem :: RUSUB_4:21
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V
for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V
proof end;

begin

definition
let V be non empty RLSStruct ;
let S be Subset of V;
attr S is Affine means :Def4: :: RUSUB_4:def 4
 for x, y being VECTOR of V
for a being Real st x in S & y in S holds
((1 - a) * x) + (a * y) in S;
end;

:: deftheorem Def4 defines Affine RUSUB_4:def 4 :
for V being non empty RLSStruct
for S being Subset of V holds
( S is Affine iff for x, y being VECTOR of V
for a being Real st x in S & y in S holds
((1 - a) * x) + (a * y) in S );

theorem Th22: :: RUSUB_4:22
for V being non empty RLSStruct holds
( [#] V is Affine & {} V is Affine )
proof end;

theorem :: RUSUB_4:23
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being VECTOR of V holds {v} is Affine
proof end;

registration
let V be non empty RLSStruct ;
cluster non empty Affine for Element of K11( the carrier of V);
existence
ex b1 being Subset of V st
( not b1 is empty & b1 is Affine )
proof end;
cluster empty Affine for Element of K11( the carrier of V);
existence
ex b1 being Subset of V st
( b1 is empty & b1 is Affine )
proof end;
end;

definition
let V be RealLinearSpace;
let W be Subspace of V;
func Up W -> non empty Subset of V equals :: RUSUB_4:def 5
 the carrier of W;
coherence
the carrier of W is non empty Subset of V by RLSUB_1:def 2;
end;

:: deftheorem defines Up RUSUB_4:def 5 :
for V being RealLinearSpace
for W being Subspace of V holds Up W = the carrier of W;

definition
let V be RealUnitarySpace;
let W be Subspace of V;
func Up W -> non empty Subset of V equals :: RUSUB_4:def 6
 the carrier of W;
coherence
the carrier of W is non empty Subset of V by RUSUB_1:def 1;
end;

:: deftheorem defines Up RUSUB_4:def 6 :
for V being RealUnitarySpace
for W being Subspace of V holds Up W = the carrier of W;

theorem :: RUSUB_4:24
for V being RealLinearSpace
for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )
proof end;

theorem Th25: :: RUSUB_4:25
for V being RealLinearSpace
for A being Affine Subset of V st 0. V in A holds
for x being VECTOR of V
for a being Real st x in A holds
a * x in A
proof end;

definition
let V be non empty RLSStruct ;
let S be non empty Subset of V;
attr S is Subspace-like means :Def7: :: RUSUB_4:def 7
( 0. V in S & ( for x, y being Element of V
for a being Real st x in S & y in S holds
( x + y in S & a * x in S ) ) );
end;

:: deftheorem Def7 defines Subspace-like RUSUB_4:def 7 :
for V being non empty RLSStruct
for S being non empty Subset of V holds
( S is Subspace-like iff ( 0. V in S & ( for x, y being Element of V
for a being Real st x in S & y in S holds
( x + y in S & a * x in S ) ) ) );

theorem Th26: :: RUSUB_4:26
for V being RealLinearSpace
for A being non empty Affine Subset of V st 0. V in A holds
( A is Subspace-like & A = the carrier of (Lin A) )
proof end;

theorem :: RUSUB_4:27
for V being RealLinearSpace
for W being Subspace of V holds Up W is Subspace-like
proof end;

theorem :: RUSUB_4:28
for V being RealUnitarySpace
for A being non empty Affine Subset of V st 0. V in A holds
A = the carrier of (Lin A)
proof end;

theorem :: RUSUB_4:29
for V being RealUnitarySpace
for W being Subspace of V holds Up W is Subspace-like
proof end;

definition
let V be non empty addLoopStr ;
let M be Subset of V;
let v be Element of V;
func v + M -> Subset of V equals :: RUSUB_4:def 8
 { (v + u) where u is Element of V : u in M } ;
coherence
{ (v + u) where u is Element of V : u in M } is Subset of V
proof end;
end;

:: deftheorem defines + RUSUB_4:def 8 :
for V being non empty addLoopStr
for M being Subset of V
for v being Element of V holds v + M = { (v + u) where u is Element of V : u in M } ;

theorem :: RUSUB_4:30
for V being RealLinearSpace
for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
proof end;

theorem Th31: :: RUSUB_4:31
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Affine Subset of V
for v being VECTOR of V holds v + M is Affine
proof end;

theorem :: RUSUB_4:32
for V being RealUnitarySpace
for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
proof end;

definition
let V be non empty addLoopStr ;
let M, N be Subset of V;
func M + N -> Subset of V equals :: RUSUB_4:def 9
 { (u + v) where u, v is Element of V : ( u in M & v in N ) } ;
coherence
{ (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V
proof end;
end;

:: deftheorem defines + RUSUB_4:def 9 :
for V being non empty addLoopStr
for M, N being Subset of V holds M + N = { (u + v) where u, v is Element of V : ( u in M & v in N ) } ;

definition
let V be non empty Abelian addLoopStr ;
let M, N be Subset of V;
:: original: +
redefine func M + N -> Subset of V;
commutativity
for M, N being Subset of V holds M + N = N + M
proof end;
end;

theorem Th33: :: RUSUB_4:33
for V being non empty addLoopStr
for M being Subset of V
for v being Element of V holds {v} + M = v + M
proof end;

theorem :: RUSUB_4:34
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Affine Subset of V
for v being VECTOR of V holds {v} + M is Affine
proof end;

theorem :: RUSUB_4:35
for V being non empty RLSStruct
for M, N being Affine Subset of V holds M /\ N is Affine
proof end;

theorem :: RUSUB_4:36
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M, N being Affine Subset of V holds M + N is Affine
proof end;