:: RUSUB_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: RUSUB_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 strict finite-dimensional UNITSTR ;
existence
ex b1 being RealUnitarySpace st
( b1 is strict & b1 is finite-dimensional )
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
( V is finite-dimensional iff ex I being finite Subset of V st I is Basis of V )
by Def1;
end;

:: deftheorem Def2 defines finite-dimensional RUSUB_4:def 2 :
for V being RealUnitarySpace holds
( V is finite-dimensional iff ex I being finite Subset of V st I is Basis of V );

theorem Th3: :: RUSUB_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace holds (0). V is finite-dimensional
proof end;

theorem Th7: :: RUSUB_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 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 strict finite-dimensional Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
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
ex b1 being Nat st
for I being Basis of V holds b1 = Card I
proof end;
uniqueness
for b1, b2 being 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 Def3 defines dim RUSUB_4:def 3 :
for V being RealUnitarySpace st V is finite-dimensional holds
for b2 being Nat holds
( b2 = dim V iff for I being Basis of V holds b2 = Card I );

theorem Th8: :: RUSUB_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V holds dim W <= dim V
proof end;

theorem Th9: :: RUSUB_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being finite-dimensional RealUnitarySpace holds dim V = dim ((Omega). V)
proof end;

theorem :: RUSUB_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being finite-dimensional RealUnitarySpace holds
( dim V = 0 iff (Omega). V = (0). V )
proof end;

theorem :: RUSUB_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 Def4 defines Subspaces_of RUSUB_4:def 4 :
for V being finite-dimensional RealUnitarySpace
for n being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty RLSStruct holds
( [#] V is Affine & {} V is Affine )
proof end;

theorem :: RUSUB_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Subset of V st
( not b1 is empty & b1 is Affine )
proof end;
cluster empty Affine Element of K40(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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for V being non empty RLSStruct
for S being non empty Subset of V holds
( S is Subspace-like iff ( 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 ) ) ) );

theorem Th26: :: RUSUB_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for W being Subspace of V holds Up W is Subspace-like
proof end;

theorem :: RUSUB_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for W being strict Subspace of V holds W = Lin (Up W) by RLVECT_3:21;

theorem :: RUSUB_4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealUnitarySpace
for W being Subspace of V holds Up W is Subspace-like
proof end;

theorem :: RUSUB_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ (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 LoopStr
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:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ (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 LoopStr
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 ) } ;

theorem Th35: :: RUSUB_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
for M, N being Subset of V holds M + N = N + M
by Th35;
end;

theorem Th36: :: RUSUB_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;