:: RUSUB_4 semantic presentation

theorem Th1: :: RUSUB_4:1

for b₁ being RealUnitarySpace
for b₂, b₃ being finite Subset of b₁
for b₄ being VECTOR of b₁ st b₄ in Lin (b₂ \/ b₃) & not b₄ in Lin b₃ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₅ in Lin (((b₂ \/ b₃) \ {b₅}) \/ {b₄}) )

proof end;

Lemma2: for b₁, b₂ being set st b₂ in b₁ holds
(b₁ \ {b₂}) \/ {b₂} = b₁

proof end;

Lemma3: for b₁, b₂ being set st not b₂ in b₁ holds
b₁ \ {b₂} = b₁

proof end;

theorem Th2: :: RUSUB_4:2

for b₁ being RealUnitarySpace
for b₂, b₃ being finite Subset of b₁ st UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) = Lin b₂ & b₃ is linearly-independent holds
( card b₃ <= card b₂ & ex b₄ being finite Subset of b₁ st
( b₄ c= b₂ & card b₄ = (card b₂) - (card b₃) & UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) = Lin (b₃ \/ b₄) ) )

proof end;

definition

let c₁ be RealUnitarySpace;
attr a₁ is finite-dimensional means :Def1: :: RUSUB_4:def 1
ex b₁ being finite Subset of a₁ st b₁ is Basis of a₁;

end;

:: deftheorem Def1 defines finite-dimensional RUSUB_4:def 1 :

registration

cluster strict finite-dimensional UNITSTR ;
existence

proof end;

end;

definition

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

end;

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

theorem Th3: :: RUSUB_4:3

for b₁ being RealUnitarySpace st b₁ is finite-dimensional holds
for b₂ being Basis of b₁ holds b₂ is finite

proof end;

theorem Th4: :: RUSUB_4:4

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁ st b₁ is finite-dimensional & b₂ is linearly-independent holds
b₂ is finite

proof end;

theorem Th5: :: RUSUB_4:5

for b₁ being RealUnitarySpace
for b₂, b₃ being Basis of b₁ st b₁ is finite-dimensional holds
Card b₂ = Card b₃

proof end;

theorem Th6: :: RUSUB_4:6

for b₁ being RealUnitarySpace holds (0). b₁ is finite-dimensional

proof end;

theorem Th7: :: RUSUB_4:7

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ st b₁ is finite-dimensional holds
b₂ is finite-dimensional

proof end;

registration

let c₁ be RealUnitarySpace;
cluster strict finite-dimensional Subspace of a₁;
existence

proof end;

end;

registration

let c₁ be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional Subspace of a₁;
correctness by Th7;

end;

registration

let c₁ be finite-dimensional RealUnitarySpace;
cluster strict finite-dimensional Subspace of a₁;
existence

proof end;

end;

definition

let c₁ be RealUnitarySpace;
assume E11: c₁ is finite-dimensional ;
func dim c₁ -> Nat means :Def3: :: RUSUB_4:def 3
for b₁ being Basis of a₁ holds a₂ = Card b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines dim RUSUB_4:def 3 :

theorem Th8: :: RUSUB_4:8

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Subspace of b₁ holds dim b₂ <= dim b₁

proof end;

theorem Th9: :: RUSUB_4:9

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Subset of b₁ st b₂ is linearly-independent holds
Card b₂ = dim (Lin b₂)

proof end;

theorem Th10: :: RUSUB_4:10

for b₁ being finite-dimensional RealUnitarySpace holds dim b₁ = dim ((Omega). b₁)

proof end;

theorem Th11: :: RUSUB_4:11

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Subspace of b₁ holds
( dim b₁ = dim b₂ iff (Omega). b₁ = (Omega). b₂ )

proof end;

theorem Th12: :: RUSUB_4:12

for b₁ being finite-dimensional RealUnitarySpace holds
( dim b₁ = 0 iff (Omega). b₁ = (0). b₁ )

proof end;

theorem Th13: :: RUSUB_4:13

for b₁ being finite-dimensional RealUnitarySpace holds
( dim b₁ = 1 iff ex b₂ being VECTOR of b₁ st
( b₂ <> 0. b₁ & (Omega). b₁ = Lin {b₂} ) )

proof end;

theorem Th14: :: RUSUB_4:14

for b₁ being finite-dimensional RealUnitarySpace holds
( dim b₁ = 2 iff ex b₂, b₃ being VECTOR of b₁ st
( b₂ <> b₃ & {b₂,b₃} is linearly-independent & (Omega). b₁ = Lin {b₂,b₃} ) )

proof end;

theorem Th15: :: RUSUB_4:15

for b₁ being finite-dimensional RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds (dim (b₂ + b₃)) + (dim (b₂ /\ b₃)) = (dim b₂) + (dim b₃)

proof end;

theorem Th16: :: RUSUB_4:16

for b₁ being finite-dimensional RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds dim (b₂ /\ b₃) >= ((dim b₂) + (dim b₃)) - (dim b₁)

proof end;

theorem Th17: :: RUSUB_4:17

for b₁ being finite-dimensional RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
dim b₁ = (dim b₂) + (dim b₃)

proof end;

Lemma17: for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Nat st b₂ <= dim b₁ holds
ex b₃ being strict Subspace of b₁ st dim b₃ = b₂

proof end;

theorem Th18: :: RUSUB_4:18

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Nat holds
( b₃ <= dim b₁ iff ex b₄ being strict Subspace of b₁ st dim b₄ = b₃ ) by Lemma17, Th8;

definition

let c₁ be finite-dimensional RealUnitarySpace;
let c₂ be Nat;
func c₂ Subspaces_of c₁ -> set means :Def4: :: RUSUB_4:def 4
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being strict Subspace of a₁ st
( b₂ = b₁ & dim b₂ = a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :

theorem Th19: :: RUSUB_4:19

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Nat st b₂ <= dim b₁ holds
not b₂ Subspaces_of b₁ is empty

proof end;

theorem Th20: :: RUSUB_4:20

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Nat st dim b₁ < b₂ holds
b₂ Subspaces_of b₁ = {}

proof end;

theorem Th21: :: RUSUB_4:21

for b₁ being finite-dimensional RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Nat holds b₃ Subspaces_of b₂ c= b₃ Subspaces_of b₁

proof end;

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
attr a₂ is Affine means :Def5: :: RUSUB_4:def 5
for b₁, b₂ being VECTOR of a₁
for b₃ being Real st b₁ in a₂ & b₂ in a₂ holds
((1 - b₃) * b₁) + (b₃ * b₂) in a₂;

end;

:: deftheorem Def5 defines Affine RUSUB_4:def 5 :

theorem Th22: :: RUSUB_4:22

for b₁ being non empty RLSStruct holds
( [#] b₁ is Affine & {} b₁ is Affine )

proof end;

theorem Th23: :: RUSUB_4:23

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being VECTOR of b₁ holds {b₂} is Affine

proof end;

registration

let c₁ be non empty RLSStruct ;
cluster non empty Affine Element of K40(the carrier of a₁);
existence

proof end;

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

proof end;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be Subspace of c₁;
func Up c₂ -> non empty Subset of a₁ equals :: RUSUB_4:def 6
the carrier of a₂;
coherence by RLSUB_1:def 2;

end;

:: deftheorem Def6 defines Up RUSUB_4:def 6 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Subspace of c₁;
func Up c₂ -> non empty Subset of a₁ equals :: RUSUB_4:def 7
the carrier of a₂;
coherence by RUSUB_1:def 1;

end;

:: deftheorem Def7 defines Up RUSUB_4:def 7 :

theorem Th24: :: RUSUB_4:24

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds
( Up b₂ is Affine & 0. b₁ in the carrier of b₂ )

proof end;

theorem Th25: :: RUSUB_4:25

for b₁ being RealLinearSpace
for b₂ being Affine Subset of b₁ st 0. b₁ in b₂ holds
for b₃ being VECTOR of b₁
for b₄ being Real st b₃ in b₂ holds
b₄ * b₃ in b₂

proof end;

definition

let c₁ be non empty RLSStruct ;
let c₂ be non empty Subset of c₁;
attr a₂ is Subspace-like means :Def8: :: RUSUB_4:def 8
( the Zero of a₁ in a₂ & ( for b₁, b₂ being Element of a₁
for b₃ being Real st b₁ in a₂ & b₂ in a₂ holds
( b₁ + b₂ in a₂ & b₃ * b₁ in a₂ ) ) );

end;

:: deftheorem Def8 defines Subspace-like RUSUB_4:def 8 :

theorem Th26: :: RUSUB_4:26

for b₁ being RealLinearSpace
for b₂ being non empty Affine Subset of b₁ st 0. b₁ in b₂ holds
( b₂ is Subspace-like & b₂ = the carrier of (Lin b₂) )

proof end;

theorem Th27: :: RUSUB_4:27

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds Up b₂ is Subspace-like

proof end;

theorem Th28: :: RUSUB_4:28

for b₁ being RealLinearSpace
for b₂ being strict Subspace of b₁ holds b₂ = Lin (Up b₂) by RLVECT_3:21;

theorem Th29: :: RUSUB_4:29

for b₁ being RealUnitarySpace
for b₂ being non empty Affine Subset of b₁ st 0. b₁ in b₂ holds
b₂ = the carrier of (Lin b₂)

proof end;

theorem Th30: :: RUSUB_4:30

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds Up b₂ is Subspace-like

proof end;

theorem Th31: :: RUSUB_4:31

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ holds b₂ = Lin (Up b₂) by RUSUB_3:5;

definition

let c₁ be non empty LoopStr ;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
func c₃ + c₂ -> Subset of a₁ equals :: RUSUB_4:def 9
{ (a₃ + b₁) where B is Element of a₁ : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines + RUSUB_4:def 9 :

theorem Th32: :: RUSUB_4:32

for b₁ being RealLinearSpace
for b₂ being strict Subspace of b₁
for b₃ being Subset of b₁
for b₄ being VECTOR of b₁ st Up b₂ = b₃ holds
b₄ + b₂ = b₄ + b₃

proof end;

theorem Th33: :: RUSUB_4:33

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂ being Affine Subset of b₁
for b₃ being VECTOR of b₁ holds b₃ + b₂ is Affine

proof end;

theorem Th34: :: RUSUB_4:34

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁
for b₃ being Subset of b₁
for b₄ being VECTOR of b₁ st Up b₂ = b₃ holds
b₄ + b₂ = b₄ + b₃

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Subset of c₁;
func c₂ + c₃ -> Subset of a₁ equals :: RUSUB_4:def 10
{ (b₁ + b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def10 defines + RUSUB_4:def 10 :

theorem Th35: :: RUSUB_4:35

for b₁ being non empty Abelian LoopStr
for b₂, b₃ being Subset of b₁ holds b₃ + b₂ = b₂ + b₃

proof end;

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be Subset of c₁;
redefine func + as c₂ + c₃ -> Subset of a₁;
commutativity by Th35;

end;

theorem Th36: :: RUSUB_4:36

for b₁ being non empty LoopStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds {b₃} + b₂ = b₃ + b₂

proof end;

theorem Th37: :: RUSUB_4:37

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂ being Affine Subset of b₁
for b₃ being VECTOR of b₁ holds {b₃} + b₂ is Affine

proof end;

theorem Th38: :: RUSUB_4:38

for b₁ being non empty RLSStruct
for b₂, b₃ being Affine Subset of b₁ holds b₂ /\ b₃ is Affine

proof end;

theorem Th39: :: RUSUB_4:39

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂, b₃ being Affine Subset of b₁ holds b₂ + b₃ is Affine

proof end;