:: 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}) )
proofend;

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

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

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 &amp; ex C being finite Subset of V st
( C c= A &amp; card C = (card A) - (card B) &amp; UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
proofend;

definition
let V be RealUnitarySpace;
attrV 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 &amp; b1 is finite-dimensional )
proofend;
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
proofend;

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

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
proofend;

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

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
proofend;

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 &amp; b1 is strict )
proofend;
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
proofend;
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
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( for I being Basis of V holds b1 = card I ) &amp; ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proofend;
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
proofend;

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)
proofend;

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

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 )
proofend;

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

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 &amp; (Omega). V = Lin {v} ) )
proofend;

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 &amp; {u,v} is linearly-independent &amp; (Omega). V = Lin {u,v} ) )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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 ;
funcn 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 &amp; 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 &amp; dim W = n ) )
proofend;
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 &amp; dim W = n ) ) ) &amp; ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x &amp; dim W = n ) ) ) holds
b1 = b2
proofend;
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 &amp; 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
proofend;

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 = {}
proofend;

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
proofend;

begin

definition
let V be non empty RLSStruct ;
let S be Subset of V;
attrS is Affine  means :Def4: :: RUSUB_4:def 4
 for x, y being VECTOR of V
for a being Real st x in S &amp; 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 &amp; 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 &amp; {} V is Affine )
proofend;

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
proofend;

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 &amp; b1 is Affine )
proofend;
cluster empty Affine for Element of K11( the carrier of V);
existence
 ex b1 being Subset of V st
( b1 is empty &amp; b1 is Affine )
proofend;
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 &amp; 0. V in the carrier of W )
proofend;

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
proofend;

definition
let V be non empty RLSStruct ;
let S be non empty Subset of V;
attrS is Subspace-like  means :Def7: :: RUSUB_4:def 7
( 0. V in S &amp; ( for x, y being Element of V
for a being Real st x in S &amp; y in S holds
( x + y in S &amp; 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 &amp; ( for x, y being Element of V
for a being Real st x in S &amp; y in S holds
( x + y in S &amp; 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 &amp; A = the carrier of (Lin A) )
proofend;

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

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)
proofend;

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

definition
let V be non empty addLoopStr ;
let M be Subset of V;
let v be Element of V;
funcv + 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
proofend;
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
proofend;

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
proofend;

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
proofend;

definition
let V be non empty addLoopStr ;
let M, N be Subset of V;
funcM + N ->  Subset of V equals :: RUSUB_4:def 9
 {  (u + v) where u, v is Element of V : ( u in M &amp; v in N )  }  ;
coherence
  {  (u + v) where u, v is Element of V : ( u in M &amp; v in N )  }  is Subset of V
proofend;
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 &amp; v in N )  }  ;

definition
let V be non empty Abelian addLoopStr ;
let M, N be Subset of V;
:: original:+
redefine funcM + N ->  Subset of V;
commutativity
 for M, N being Subset of V holds M + N = N + M
proofend;
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
proofend;

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
proofend;

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

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
proofend;