:: RUSUB_2 semantic presentation

definition

let c₁ be RealUnitarySpace;
let c₂, c₃ be Subspace of c₁;
func c₂ + c₃ -> strict Subspace of a₁ means :Def1: :: RUSUB_2:def 1
the carrier of a₄ = { (b₁ + b₂) where B is VECTOR of a₁, B is VECTOR of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
existence

proof end;

uniqueness by RUSUB_1:24;

end;

:: deftheorem Def1 defines + RUSUB_2:def 1 :

definition

let c₁ be RealUnitarySpace;
let c₂, c₃ be Subspace of c₁;
func c₂ /\ c₃ -> strict Subspace of a₁ means :Def2: :: RUSUB_2:def 2
the carrier of a₄ = the carrier of a₂ /\ the carrier of a₃;
existence

proof end;

uniqueness by RUSUB_1:24;

end;

:: deftheorem Def2 defines /\ RUSUB_2:def 2 :

theorem Th1: :: RUSUB_2:1

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄ being set holds
( b₄ in b₂ + b₃ iff ex b₅, b₆ being VECTOR of b₁ st
( b₅ in b₂ & b₆ in b₃ & b₄ = b₅ + b₆ ) )

proof end;

theorem Th2: :: RUSUB_2:2

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄ being VECTOR of b₁ st ( b₄ in b₂ or b₄ in b₃ ) holds
b₄ in b₂ + b₃

proof end;

theorem Th3: :: RUSUB_2:3

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄ being set holds
( b₄ in b₂ /\ b₃ iff ( b₄ in b₂ & b₄ in b₃ ) )

proof end;

Lemma6: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

Lemma7: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds the carrier of b₂ c= the carrier of (b₂ + b₃)

proof end;

Lemma8: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being strict Subspace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ + b₃ = b₃

proof end;

theorem Th4: :: RUSUB_2:4

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ holds b₂ + b₂ = b₂ by Lemma8;

theorem Th5: :: RUSUB_2:5

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds b₂ + b₃ = b₃ + b₂ by Lemma6;

theorem Th6: :: RUSUB_2:6

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th7: :: RUSUB_2:7

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ is Subspace of b₂ + b₃ & b₃ is Subspace of b₂ + b₃ )

proof end;

theorem Th8: :: RUSUB_2:8

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being strict Subspace of b₁ holds
( b₂ is Subspace of b₃ iff b₂ + b₃ = b₃ )

proof end;

theorem Th9: :: RUSUB_2:9

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ holds
( ((0). b₁) + b₂ = b₂ & b₂ + ((0). b₁) = b₂ )

proof end;

theorem Th10: :: RUSUB_2:10

for b₁ being RealUnitarySpace holds
( ((0). b₁) + ((Omega). b₁) = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) & ((Omega). b₁) + ((0). b₁) = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) )

proof end;

theorem Th11: :: RUSUB_2:11

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds
( ((Omega). b₁) + b₂ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) & b₂ + ((Omega). b₁) = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) )

proof end;

theorem Th12: :: RUSUB_2:12

for b₁ being strict RealUnitarySpace holds ((Omega). b₁) + ((Omega). b₁) = b₁ by Th11;

theorem Th13: :: RUSUB_2:13

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ holds b₂ /\ b₂ = b₂

proof end;

theorem Th14: :: RUSUB_2:14

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds b₂ /\ b₃ = b₃ /\ b₂

proof end;

theorem Th15: :: RUSUB_2:15

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds b₂ /\ (b₃ /\ b₄) = (b₂ /\ b₃) /\ b₄

proof end;

Lemma17: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds the carrier of (b₂ /\ b₃) c= the carrier of b₂

proof end;

theorem Th16: :: RUSUB_2:16

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ /\ b₃ is Subspace of b₂ & b₂ /\ b₃ is Subspace of b₃ )

proof end;

theorem Th17: :: RUSUB_2:17

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being strict Subspace of b₁ holds
( b₃ is Subspace of b₂ iff b₃ /\ b₂ = b₃ )

proof end;

theorem Th18: :: RUSUB_2:18

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds
( ((0). b₁) /\ b₂ = (0). b₁ & b₂ /\ ((0). b₁) = (0). b₁ )

proof end;

theorem Th19: :: RUSUB_2:19

for b₁ being RealUnitarySpace holds
( ((0). b₁) /\ ((Omega). b₁) = (0). b₁ & ((Omega). b₁) /\ ((0). b₁) = (0). b₁ ) by Th18;

theorem Th20: :: RUSUB_2:20

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ holds
( ((Omega). b₁) /\ b₂ = b₂ & b₂ /\ ((Omega). b₁) = b₂ )

proof end;

theorem Th21: :: RUSUB_2:21

for b₁ being strict RealUnitarySpace holds ((Omega). b₁) /\ ((Omega). b₁) = b₁

proof end;

Lemma22: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds the carrier of (b₂ /\ b₃) c= the carrier of (b₂ + b₃)

proof end;

theorem Th22: :: RUSUB_2:22

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds b₂ /\ b₃ is Subspace of b₂ + b₃

proof end;

Lemma23: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds the carrier of ((b₂ /\ b₃) + b₃) = the carrier of b₃

proof end;

theorem Th23: :: RUSUB_2:23

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being strict Subspace of b₁ holds (b₂ /\ b₃) + b₃ = b₃

proof end;

Lemma25: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds the carrier of (b₂ /\ (b₂ + b₃)) = the carrier of b₂

proof end;

theorem Th24: :: RUSUB_2:24

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being strict Subspace of b₁ holds b₃ /\ (b₃ + b₂) = b₃

proof end;

Lemma27: for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds the carrier of ((b₂ /\ b₃) + (b₃ /\ b₄)) c= the carrier of (b₃ /\ (b₂ + b₄))

proof end;

theorem Th25: :: RUSUB_2:25

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds (b₂ /\ b₃) + (b₃ /\ b₄) is Subspace of b₃ /\ (b₂ + b₄)

proof end;

Lemma28: for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
the carrier of (b₃ /\ (b₂ + b₄)) = the carrier of ((b₂ /\ b₃) + (b₃ /\ b₄))

proof end;

theorem Th26: :: RUSUB_2:26

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₃ /\ (b₂ + b₄) = (b₂ /\ b₃) + (b₃ /\ b₄)

proof end;

Lemma30: for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds the carrier of (b₃ + (b₂ /\ b₄)) c= the carrier of ((b₂ + b₃) /\ (b₃ + b₄))

proof end;

theorem Th27: :: RUSUB_2:27

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ holds b₃ + (b₂ /\ b₄) is Subspace of (b₂ + b₃) /\ (b₃ + b₄)

proof end;

Lemma31: for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
the carrier of (b₃ + (b₂ /\ b₄)) = the carrier of ((b₂ + b₃) /\ (b₃ + b₄))

proof end;

theorem Th28: :: RUSUB_2:28

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is Subspace of b₃ holds
b₃ + (b₂ /\ b₄) = (b₂ + b₃) /\ (b₃ + b₄)

proof end;

theorem Th29: :: RUSUB_2:29

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Subspace of b₁ st b₂ is strict Subspace of b₄ holds
b₂ + (b₃ /\ b₄) = (b₂ + b₃) /\ b₄

proof end;

theorem Th30: :: RUSUB_2:30

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁ holds
( b₂ + b₃ = b₃ iff b₂ /\ b₃ = b₂ )

proof end;

theorem Th31: :: RUSUB_2:31

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being strict Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ + b₄ is Subspace of b₃ + b₄

proof end;

theorem Th32: :: RUSUB_2:32

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( ( b₂ is Subspace of b₃ or b₃ is Subspace of b₂ ) iff ex b₄ being Subspace of b₁ st the carrier of b₄ = the carrier of b₂ \/ the carrier of b₃ )

proof end;

definition

let c₁ be RealUnitarySpace;
func Subspaces c₁ -> set means :Def3: :: RUSUB_2:def 3
for b₁ being set holds
( b₁ in a₂ iff b₁ is strict Subspace of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Subspaces RUSUB_2:def 3 :

registration

let c₁ be RealUnitarySpace;
cluster Subspaces a₁ -> non empty ;
coherence

proof end;

end;

theorem Th33: :: RUSUB_2:33

for b₁ being strict RealUnitarySpace holds b₁ in Subspaces b₁

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂, c₃ be Subspace of c₁;
pred c₁ is_the_direct_sum_of c₂,c₃ means :Def4: :: RUSUB_2:def 4
( UNITSTR(# the carrier of a₁,the Zero of a₁,the add of a₁,the Mult of a₁,the scalar of a₁ #) = a₂ + a₃ & a₂ /\ a₃ = (0). a₁ );

end;

:: deftheorem Def4 defines is_the_direct_sum_of RUSUB_2:def 4 :

Lemma35: for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ st ( for b₃ being VECTOR of b₁ holds b₃ in b₂ ) holds
b₂ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #)

proof end;

Lemma36: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ + b₃ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) iff for b₄ being VECTOR of b₁ ex b₅, b₆ being VECTOR of b₁ st
( b₅ in b₂ & b₆ in b₃ & b₄ = b₅ + b₆ ) )

proof end;

Lemma37: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ ex b₃ being strict Subspace of b₁ st b₁ is_the_direct_sum_of b₃,b₂

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Subspace of c₁;
mode Linear_Compl of c₂ -> Subspace of a₁ means :Def5: :: RUSUB_2:def 5
a₁ is_the_direct_sum_of a₃,a₂;
existence

proof end;

end;

:: deftheorem Def5 defines Linear_Compl RUSUB_2:def 5 :

registration

let c₁ be RealUnitarySpace;
let c₂ be Subspace of c₁;
cluster strict Linear_Compl of a₂;
existence

proof end;

end;

Lemma39: for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
b₁ is_the_direct_sum_of b₃,b₂

proof end;

theorem Th34: :: RUSUB_2:34

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
b₃ is Linear_Compl of b₂

proof end;

theorem Th35: :: RUSUB_2:35

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂ holds
( b₁ is_the_direct_sum_of b₃,b₂ & b₁ is_the_direct_sum_of b₂,b₃ )

proof end;

theorem Th36: :: RUSUB_2:36

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂ holds
( b₂ + b₃ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) & b₃ + b₂ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) )

proof end;

theorem Th37: :: RUSUB_2:37

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂ holds
( b₂ /\ b₃ = (0). b₁ & b₃ /\ b₂ = (0). b₁ )

proof end;

theorem Th38: :: RUSUB_2:38

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
b₁ is_the_direct_sum_of b₃,b₂ by Lemma39;

theorem Th39: :: RUSUB_2:39

for b₁ being RealUnitarySpace holds
( b₁ is_the_direct_sum_of (0). b₁, (Omega). b₁ & b₁ is_the_direct_sum_of (Omega). b₁, (0). b₁ )

proof end;

theorem Th40: :: RUSUB_2:40

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂ holds b₂ is Linear_Compl of b₃

proof end;

theorem Th41: :: RUSUB_2:41

for b₁ being RealUnitarySpace holds
( (0). b₁ is Linear_Compl of (Omega). b₁ & (Omega). b₁ is Linear_Compl of (0). b₁ )

proof end;

Lemma44: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being set holds
( b₄ in b₃ + b₂ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₄ = b₃ + b₅ ) )

proof end;

theorem Th42: :: RUSUB_2:42

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄ being Coset of b₂
for b₅ being Coset of b₃ st b₄ meets b₅ holds
b₄ /\ b₅ is Coset of b₂ /\ b₃

proof end;

Lemma46: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ ex b₄ being Coset of b₂ st b₃ in b₄

proof end;

theorem Th43: :: RUSUB_2:43

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( b₁ is_the_direct_sum_of b₂,b₃ iff for b₄ being Coset of b₂
for b₅ being Coset of b₃ ex b₆ being VECTOR of b₁ st b₄ /\ b₅ = {b₆} )

proof end;

theorem Th44: :: RUSUB_2:44

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ + b₃ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) iff for b₄ being VECTOR of b₁ ex b₅, b₆ being VECTOR of b₁ st
( b₅ in b₂ & b₆ in b₃ & b₄ = b₅ + b₆ ) ) by Lemma36;

theorem Th45: :: RUSUB_2:45

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st b₁ is_the_direct_sum_of b₂,b₃ & b₄ = b₅ + b₆ & b₄ = b₇ + b₈ & b₅ in b₂ & b₇ in b₂ & b₆ in b₃ & b₈ in b₃ holds
( b₅ = b₇ & b₆ = b₈ )

proof end;

theorem Th46: :: RUSUB_2:46

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st b₁ = b₂ + b₃ & ex b₄ being VECTOR of b₁ st
for b₅, b₆, b₇, b₈ being VECTOR of b₁ st b₄ = b₅ + b₆ & b₄ = b₇ + b₈ & b₅ in b₂ & b₇ in b₂ & b₆ in b₃ & b₈ in b₃ holds
( b₅ = b₇ & b₆ = b₈ ) holds
b₁ is_the_direct_sum_of b₂,b₃

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be VECTOR of c₁;
let c₃, c₄ be Subspace of c₁;
assume E49: c₁ is_the_direct_sum_of c₃,c₄ ;
func c₂ |-- c₃,c₄ -> Element of [:the carrier of a₁,the carrier of a₁:] means :Def6: :: RUSUB_2:def 6
( a₂ = (a₅ `1 ) + (a₅ `2 ) & a₅ `1 in a₃ & a₅ `2 in a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines |-- RUSUB_2:def 6 :

theorem Th47: :: RUSUB_2:47

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Subspace of b₁ st b₁ is_the_direct_sum_of b₃,b₄ holds
(b₂ |-- b₃,b₄) `1 = (b₂ |-- b₄,b₃) `2

proof end;

theorem Th48: :: RUSUB_2:48

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Subspace of b₁ st b₁ is_the_direct_sum_of b₃,b₄ holds
(b₂ |-- b₃,b₄) `2 = (b₂ |-- b₄,b₃) `1

proof end;

theorem Th49: :: RUSUB_2:49

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂
for b₄ being VECTOR of b₁
for b₅ being Element of [:the carrier of b₁,the carrier of b₁:] st (b₅ `1 ) + (b₅ `2 ) = b₄ & b₅ `1 in b₂ & b₅ `2 in b₃ holds
b₅ = b₄ |-- b₂,b₃

proof end;

theorem Th50: :: RUSUB_2:50

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂
for b₄ being VECTOR of b₁ holds ((b₄ |-- b₂,b₃) `1 ) + ((b₄ |-- b₂,b₃) `2 ) = b₄

proof end;

theorem Th51: :: RUSUB_2:51

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂
for b₄ being VECTOR of b₁ holds
( (b₄ |-- b₂,b₃) `1 in b₂ & (b₄ |-- b₂,b₃) `2 in b₃ )

proof end;

theorem Th52: :: RUSUB_2:52

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂
for b₄ being VECTOR of b₁ holds (b₄ |-- b₂,b₃) `1 = (b₄ |-- b₃,b₂) `2

proof end;

theorem Th53: :: RUSUB_2:53

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Linear_Compl of b₂
for b₄ being VECTOR of b₁ holds (b₄ |-- b₂,b₃) `2 = (b₄ |-- b₃,b₂) `1

proof end;

definition

let c₁ be RealUnitarySpace;
func SubJoin c₁ -> BinOp of Subspaces a₁ means :Def7: :: RUSUB_2:def 7
for b₁, b₂ being Element of Subspaces a₁
for b₃, b₄ being Subspace of a₁ st b₁ = b₃ & b₂ = b₄ holds
a₂ . b₁,b₂ = b₃ + b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines SubJoin RUSUB_2:def 7 :

definition

let c₁ be RealUnitarySpace;
func SubMeet c₁ -> BinOp of Subspaces a₁ means :Def8: :: RUSUB_2:def 8
for b₁, b₂ being Element of Subspaces a₁
for b₃, b₄ being Subspace of a₁ st b₁ = b₃ & b₂ = b₄ holds
a₂ . b₁,b₂ = b₃ /\ b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines SubMeet RUSUB_2:def 8 :

theorem Th54: :: RUSUB_2:54

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is Lattice

proof end;

registration

let c₁ be RealUnitarySpace;
cluster LattStr(# (Subspaces a₁),(SubJoin a₁),(SubMeet a₁) #) -> Lattice-like ;
coherence by Th54;

end;

theorem Th55: :: RUSUB_2:55

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is lower-bounded

proof end;

theorem Th56: :: RUSUB_2:56

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is upper-bounded

proof end;

theorem Th57: :: RUSUB_2:57

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is 01_Lattice

proof end;

theorem Th58: :: RUSUB_2:58

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is modular

proof end;

theorem Th59: :: RUSUB_2:59

for b₁ being RealUnitarySpace holds LattStr(# (Subspaces b₁),(SubJoin b₁),(SubMeet b₁) #) is complemented

proof end;

registration

let c₁ be RealUnitarySpace;
cluster LattStr(# (Subspaces a₁),(SubJoin a₁),(SubMeet a₁) #) -> Lattice-like modular lower-bounded upper-bounded complemented ;
coherence by Th55, Th56, Th58, Th59;

end;

theorem Th60: :: RUSUB_2:60

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being strict Subspace of b₁ st b₂ is Subspace of b₃ holds
b₂ /\ b₄ is Subspace of b₃ /\ b₄

proof end;

theorem Th61: :: RUSUB_2:61

for b₁ being RealUnitarySpace
for b₂ being strict Subspace of b₁ st ( for b₃ being VECTOR of b₁ holds b₃ in b₂ ) holds
b₂ = UNITSTR(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁,the scalar of b₁ #) by Lemma35;

theorem Th62: :: RUSUB_2:62

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ ex b₄ being Coset of b₂ st b₃ in b₄ by Lemma46;

theorem Th63: :: RUSUB_2:63

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being set holds
( b₄ in b₃ + b₂ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₄ = b₃ + b₅ ) ) by Lemma44;