:: RUSUB_4 semantic presentation

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 Zero of V,the add 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 Zero of V,the add 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 :

registration

cluster strict finite-dimensional UNITSTR ;
existence

proof end;

end;

definition

let V be RealUnitarySpace;
redefine attr V is finite-dimensional means :Def2: :: RUSUB_4:def 2
ex I being finite Subset of V st I is Basis of V;
compatibility by Def1;

end;

:: deftheorem Def2 defines finite-dimensional RUSUB_4:def 2 :

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 strict finite-dimensional Subspace of V;
existence

proof end;

end;

registration

let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional Subspace of V;
correctness by Th7;

end;

registration

let V be finite-dimensional RealUnitarySpace;
cluster strict finite-dimensional Subspace of V;
existence

proof end;

end;

definition

let V be RealUnitarySpace;
assume A1: V is finite-dimensional ;
func dim V -> Nat means :Def3: :: RUSUB_4:def 3
for I being Basis of V holds it = Card I;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines dim RUSUB_4:def 3 :

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;

Lm3: for V being finite-dimensional RealUnitarySpace
for n being 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 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :

theorem :: RUSUB_4:19

for V being finite-dimensional RealUnitarySpace
for n being 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 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 Nat holds n Subspaces_of W c= n Subspaces_of V

proof end;

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 :

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 RealLinearSpace-like 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 K40(the carrier of V);
existence

proof end;

cluster empty Affine Element of K40(the carrier of V);
existence

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 by RLSUB_1:def 2;

end;

:: deftheorem defines Up RUSUB_4:def 6 :

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 by RUSUB_1:def 1;

end;

:: deftheorem defines Up RUSUB_4:def 7 :

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
( the Zero of 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 :

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 RealLinearSpace
for W being strict Subspace of V holds W = Lin (Up W) by RLVECT_3:21;

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;

theorem :: RUSUB_4:31

for V being RealUnitarySpace
for W being strict Subspace of V holds W = Lin (Up W) by RUSUB_3:5;

definition

let V be non empty LoopStr ;
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

proof end;

end;

:: deftheorem defines + RUSUB_4:def 9 :

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 RealLinearSpace-like 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 LoopStr ;
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

proof end;

end;

:: deftheorem defines + RUSUB_4:def 10 :

theorem Th35: :: RUSUB_4:35

for V being non empty Abelian LoopStr
for M, N being Subset of V holds N + M = M + N

proof end;

definition

let V be non empty Abelian LoopStr ;
let M, N be Subset of V;
:: original: +
redefine func M + N -> Subset of V;
commutativity by Th35;

end;

theorem Th36: :: RUSUB_4:36

for V being non empty LoopStr
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 RealLinearSpace-like 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 RealLinearSpace-like RLSStruct
for M, N being Affine Subset of V holds M + N is Affine

proof end;