:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama

::

:: Received October 9, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

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}) )

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;

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

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;

end;
attr V is finite-dimensional means :Def1: :: RUSUB_4:def 1

ex A being finite Subset of V st A is Basis of V;

ex A being finite Subset of V st A is Basis of V;

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

for V being RealUnitarySpace holds

( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

registration

ex b_{1} being RealUnitarySpace st

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

cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() strict RealUnitarySpace-like finite-dimensional for UNITSTR ;

existence ex b

( b

proof 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

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

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

for A, B being Basis of V st V is finite-dimensional holds

card A = card B

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

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

W is finite-dimensional

proof end;

registration

let V be RealUnitarySpace;

ex b_{1} being Subspace of V st

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

end;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() strict RealUnitarySpace-like finite-dimensional for Subspace of V;

existence ex b

( b

proof end;

registration

let V be finite-dimensional RealUnitarySpace;

correctness

coherence

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

by Th7;

end;
correctness

coherence

for b

by Th7;

registration

let V be finite-dimensional RealUnitarySpace;

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

end;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V123() strict RealUnitarySpace-like finite-dimensional for Subspace of V;

existence ex b

proof end;

definition

let V be RealUnitarySpace;

assume A1: V is finite-dimensional ;

ex b_{1} being Element of NAT st

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

for b_{1}, b_{2} being Element of 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;
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 for I being Basis of V holds it = card I;

ex b

for I being Basis of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines dim RUSUB_4:def 2 :

for V being RealUnitarySpace st V is finite-dimensional holds

for b_{2} being Element of NAT holds

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

for V being RealUnitarySpace st V is finite-dimensional holds

for b

( b

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)

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

card A = dim (Lin A)

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 )

for W being Subspace of V holds

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

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} ) )

( 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} ) )

( 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)

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)

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)

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

definition

let V be finite-dimensional RealUnitarySpace;

let n be Element of NAT ;

ex b_{1} being set st

for x being object 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 object holds

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

( W = x & dim W = n ) ) ) & ( for x being object 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 n be Element of NAT ;

func n Subspaces_of V -> set means :Def3: :: RUSUB_4:def 3

for x being object holds

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

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

existence for x being object holds

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

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

ex b

for x being object 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 object holds

( x in b

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

b

proof end;

:: deftheorem Def3 defines Subspaces_of RUSUB_4:def 3 :

for V being finite-dimensional RealUnitarySpace

for n being Element of NAT

for b_{3} being set holds

( b_{3} = n Subspaces_of V iff for x being object holds

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

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

for V being finite-dimensional RealUnitarySpace

for n being Element of NAT

for b

( b

( x in b

( 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

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

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

for W being Subspace of V

for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V

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

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

for v being VECTOR of V holds {v} is Affine

proof end;

registration

let V be non empty RLSStruct ;

existence

ex b_{1} being Subset of V st

( not b_{1} is empty & b_{1} is Affine )

ex b_{1} being Subset of V st

( b_{1} is empty & b_{1} is Affine )

end;
existence

ex b

( not b

proof end;

existence ex b

( b

proof end;

definition

let V be RealLinearSpace;

let W be Subspace of V;

coherence

the carrier of W is non empty Subset of V by RLSUB_1:def 2;

end;
let W be Subspace of V;

coherence

the carrier of W is non empty Subset of V by RLSUB_1:def 2;

:: deftheorem defines Up RUSUB_4:def 5 :

for V being RealLinearSpace

for W being Subspace of V holds Up W = the carrier of W;

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;

coherence

the carrier of W is non empty Subset of V by RUSUB_1:def 1;

end;
let W be Subspace of V;

coherence

the carrier of W is non empty Subset of V by RUSUB_1:def 1;

:: deftheorem defines Up RUSUB_4:def 6 :

for V being RealUnitarySpace

for W being Subspace of V holds Up W = the carrier of W;

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 )

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

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;

:: deftheorem 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 ) ) ) );

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

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

for A being non empty Affine Subset of V st 0. V in A holds

A = the carrier of (Lin A)

proof end;

definition

let V be non empty addLoopStr ;

let M be Subset of V;

let v be Element of V;

coherence

{ (v + u) where u is Element of V : u in M } is Subset of V

end;
let M be Subset of V;

let v be Element of V;

coherence

{ (v + u) where u is Element of V : u in M } is Subset of V

proof 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 } ;

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

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

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

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;

{ (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V

end;
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 ) } ;

{ (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V

proof 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 ) } ;

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

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

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

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

for M being Affine Subset of V

for v being VECTOR of V holds {v} + M 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

for M, N being Affine Subset of V holds M + N is Affine

proof end;