:: Dimension of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002 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 V108() strict RealUnitarySpace-like finite-dimensional UNITSTR ;
existence
ex b₁ being RealUnitarySpace st
( b₁ is strict & b₁ 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 V108() strict RealUnitarySpace-like finite-dimensional Subspace of V;
existence
ex b₁ being Subspace of V st
( b₁ is finite-dimensional & b₁ is strict )

proof end;

end;

registration

let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional Subspace of V;
correctness
coherence
for b₁ being Subspace of V holds b₁ 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 V108() strict RealUnitarySpace-like finite-dimensional Subspace of V;
existence
ex b₁ being Subspace of V st b₁ is strict

proof end;

end;

begin

definition

canceled;
let V be RealUnitarySpace;
assume A1: V is finite-dimensional ;
func dim V -> Element of NAT means :Def3: :: RUSUB_4:def 3
for I being Basis of V holds it = card I;
existence
ex b₁ being Element of NAT st
for I being Basis of V holds b₁ = card I

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ( for I being Basis of V holds b₁ = card I ) & ( for I being Basis of V holds b₂ = card I ) holds
b₁ = b₂

proof end;

end;

:: deftheorem RUSUB_4:def 2 :
canceled;

:: deftheorem Def3 defines dim RUSUB_4:def 3 :
for V being RealUnitarySpace st V is finite-dimensional holds
for b₂ being Element of NAT holds
( b₂ = dim V iff for I being Basis of V holds b₂ = 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 :Def4: :: RUSUB_4:def 4
for x being set holds
( x in it iff ex W being strict Subspace of V st
( W = x & dim W = n ) );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff ex W being strict Subspace of V st
( W = x & dim W = n ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being set holds
( x in b₂ iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT
for b₃ being set holds
( b₃ = n Subspaces_of V iff for x being set holds
( x in b₃ 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 :Def5: :: RUSUB_4:def 5
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 Def5 defines Affine RUSUB_4:def 5 :
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 Element of K11( the carrier of V);
existence
ex b₁ being Subset of V st
( not b₁ is empty & b₁ is Affine )

proof end;

cluster empty Affine Element of K11( the carrier of V);
existence
ex b₁ being Subset of V st
( b₁ is empty & b₁ 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 6
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 6 :
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 7
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 7 :
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 :Def8: :: RUSUB_4:def 8
( 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 Def8 defines Subspace-like RUSUB_4:def 8 :
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

canceled;

theorem :: RUSUB_4:29

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:30

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 9
{ (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 9 :
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:31

canceled;

theorem :: RUSUB_4:32

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 Th33: :: RUSUB_4:33

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:34

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 10
{ (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 10 :
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 :: RUSUB_4:35

canceled;

theorem Th36: :: RUSUB_4:36

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:37

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:38

for V being non empty RLSStruct
for M, N being Affine Subset of V holds M /\ N is Affine

proof end;

theorem :: RUSUB_4:39

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;