:: RLSUB_2 semantic presentation

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be Subspace of c₁;
func c₂ + c₃ -> strict Subspace of a₁ means :Def1: :: RLSUB_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 RLSUB_1:38;

end;

:: deftheorem Def1 defines + RLSUB_2:def 1 :

definition

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

proof end;

uniqueness by RLSUB_1:38;

end;

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

theorem Th1: :: RLSUB_2:1

canceled;

theorem Th2: :: RLSUB_2:2

canceled;

theorem Th3: :: RLSUB_2:3

canceled;

theorem Th4: :: RLSUB_2:4

canceled;

theorem Th5: :: RLSUB_2:5

for b₁ being RealLinearSpace
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 Th6: :: RLSUB_2:6

for b₁ being RealLinearSpace
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 Th7: :: RLSUB_2:7

for b₁ being RealLinearSpace
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 RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

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

proof end;

Lemma8: for b₁ being RealLinearSpace
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 Th8: :: RLSUB_2:8

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

theorem Th9: :: RLSUB_2:9

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

theorem Th10: :: RLSUB_2:10

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

proof end;

theorem Th11: :: RLSUB_2:11

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

proof end;

theorem Th12: :: RLSUB_2:12

for b₁ being RealLinearSpace
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 Th13: :: RLSUB_2:13

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

proof end;

theorem Th14: :: RLSUB_2:14

for b₁ being RealLinearSpace holds
( ((0). b₁) + ((Omega). b₁) = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) & ((Omega). b₁) + ((0). b₁) = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) ) by Th13;

theorem Th15: :: RLSUB_2:15

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

proof end;

theorem Th16: :: RLSUB_2:16

for b₁ being strict RealLinearSpace holds ((Omega). b₁) + ((Omega). b₁) = b₁ by Th15;

theorem Th17: :: RLSUB_2:17

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

proof end;

theorem Th18: :: RLSUB_2:18

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

proof end;

theorem Th19: :: RLSUB_2:19

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

proof end;

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

proof end;

theorem Th20: :: RLSUB_2:20

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

proof end;

theorem Th21: :: RLSUB_2:21

for b₁ being RealLinearSpace
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 Th22: :: RLSUB_2:22

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

proof end;

theorem Th23: :: RLSUB_2:23

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

theorem Th24: :: RLSUB_2:24

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

proof end;

theorem Th25: :: RLSUB_2:25

for b₁ being strict RealLinearSpace holds ((Omega). b₁) /\ ((Omega). b₁) = b₁ by Th24;

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

proof end;

theorem Th26: :: RLSUB_2:26

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

proof end;

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

proof end;

theorem Th27: :: RLSUB_2:27

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

proof end;

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

proof end;

theorem Th28: :: RLSUB_2:28

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

proof end;

Lemma27: for b₁ being RealLinearSpace
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 Th29: :: RLSUB_2:29

for b₁ being RealLinearSpace
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 RealLinearSpace
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 Th30: :: RLSUB_2:30

for b₁ being RealLinearSpace
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 RealLinearSpace
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 Th31: :: RLSUB_2:31

for b₁ being RealLinearSpace
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 RealLinearSpace
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 Th32: :: RLSUB_2:32

for b₁ being RealLinearSpace
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 Th33: :: RLSUB_2:33

for b₁ being RealLinearSpace
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 Th34: :: RLSUB_2:34

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

proof end;

theorem Th35: :: RLSUB_2:35

for b₁ being RealLinearSpace
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 Th36: :: RLSUB_2:36

for b₁ being RealLinearSpace
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 RealLinearSpace;
func Subspaces c₁ -> set means :Def3: :: RLSUB_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 RLSUB_2:def 3 :

registration

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

proof end;

end;

theorem Th37: :: RLSUB_2:37

canceled;

theorem Th38: :: RLSUB_2:38

canceled;

theorem Th39: :: RLSUB_2:39

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

proof end;

definition

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

end;

:: deftheorem Def4 defines is_the_direct_sum_of RLSUB_2:def 4 :

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

proof end;

Lemma36: for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ + b₃ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult 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 non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ = b₃ + b₄ iff b₃ = b₂ - b₄ )

proof end;

Lemma38: for b₁ being RealLinearSpace
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 RealLinearSpace;
let c₂ be Subspace of c₁;
mode Linear_Compl of c₂ -> Subspace of a₁ means :Def5: :: RLSUB_2:def 5
a₁ is_the_direct_sum_of a₃,a₂;
existence

proof end;

end;

:: deftheorem Def5 defines Linear_Compl RLSUB_2:def 5 :

registration

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

proof end;

end;

Lemma40: for b₁ being RealLinearSpace
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 Th40: :: RLSUB_2:40

canceled;

theorem Th41: :: RLSUB_2:41

canceled;

theorem Th42: :: RLSUB_2:42

for b₁ being RealLinearSpace
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 Th43: :: RLSUB_2:43

for b₁ being RealLinearSpace
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 Th44: :: RLSUB_2:44

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

proof end;

theorem Th45: :: RLSUB_2:45

for b₁ being RealLinearSpace
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 Th46: :: RLSUB_2:46

for b₁ being RealLinearSpace
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 Lemma40;

theorem Th47: :: RLSUB_2:47

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

proof end;

theorem Th48: :: RLSUB_2:48

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

proof end;

theorem Th49: :: RLSUB_2:49

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

proof end;

theorem Th50: :: RLSUB_2:50

for b₁ being RealLinearSpace
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 RealLinearSpace
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 Th51: :: RLSUB_2:51

for b₁ being RealLinearSpace
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 Th52: :: RLSUB_2:52

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds
( b₂ + b₃ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult 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 Th53: :: RLSUB_2:53

for b₁ being RealLinearSpace
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;

Lemma49: for b₁, b₂ being set st b₁ c< b₂ holds
ex b₃ being set st
( b₃ in b₂ & not b₃ in b₁ )

proof end;

theorem Th54: :: RLSUB_2:54

for b₁ being RealLinearSpace
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 RealLinearSpace;
let c₂ be VECTOR of c₁;
let c₃, c₄ be Subspace of c₁;
assume E50: c₁ is_the_direct_sum_of c₃,c₄ ;
func c₂ |-- c₃,c₄ -> Element of [:the carrier of a₁,the carrier of a₁:] means :Def6: :: RLSUB_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 |-- RLSUB_2:def 6 :

theorem Th55: :: RLSUB_2:55

canceled;

theorem Th56: :: RLSUB_2:56

canceled;

theorem Th57: :: RLSUB_2:57

canceled;

theorem Th58: :: RLSUB_2:58

canceled;

theorem Th59: :: RLSUB_2:59

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

proof end;

theorem Th60: :: RLSUB_2:60

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

proof end;

theorem Th61: :: RLSUB_2:61

for b₁ being RealLinearSpace
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 Th62: :: RLSUB_2:62

for b₁ being RealLinearSpace
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 Th63: :: RLSUB_2:63

for b₁ being RealLinearSpace
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 Th64: :: RLSUB_2:64

for b₁ being RealLinearSpace
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 Th65: :: RLSUB_2:65

for b₁ being RealLinearSpace
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 RealLinearSpace;
func SubJoin c₁ -> BinOp of Subspaces a₁ means :Def7: :: RLSUB_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 RLSUB_2:def 7 :

definition

let c₁ be RealLinearSpace;
func SubMeet c₁ -> BinOp of Subspaces a₁ means :Def8: :: RLSUB_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 RLSUB_2:def 8 :

theorem Th66: :: RLSUB_2:66

canceled;

theorem Th67: :: RLSUB_2:67

canceled;

theorem Th68: :: RLSUB_2:68

canceled;

theorem Th69: :: RLSUB_2:69

canceled;

theorem Th70: :: RLSUB_2:70

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

proof end;

registration

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

end;

theorem Th71: :: RLSUB_2:71

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

proof end;

theorem Th72: :: RLSUB_2:72

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

proof end;

theorem Th73: :: RLSUB_2:73

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

proof end;

theorem Th74: :: RLSUB_2:74

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

proof end;

Lemma60: for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ is_a_complement_of b₃ iff ( b₂ "\/" b₃ = Top b₁ & b₂ "/\" b₃ = Bottom b₁ ) )

proof end;

Lemma61: for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "/\" b₂ = b₂ ) holds
b₂ = Bottom b₁

proof end;

Lemma62: for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "\/" b₂ = b₂ ) holds
b₂ = Top b₁

proof end;

theorem Th75: :: RLSUB_2:75

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

proof end;

registration

let c₁ be RealLinearSpace;
cluster LattStr(# (Subspaces a₁),(SubJoin a₁),(SubMeet a₁) #) -> Lattice-like modular lower-bounded upper-bounded complemented ;
coherence by Th71, Th72, Th74, Th75;

end;

theorem Th76: :: RLSUB_2:76

for b₁ being RealLinearSpace
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 Th77: :: RLSUB_2:77

for b₁, b₂ being set st b₁ c< b₂ holds
ex b₃ being set st
( b₃ in b₂ & not b₃ in b₁ ) by Lemma49;

theorem Th78: :: RLSUB_2:78

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ = b₃ + b₄ iff b₃ = b₂ - b₄ ) by Lemma37;

theorem Th79: :: RLSUB_2:79

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

theorem Th80: :: RLSUB_2:80

for b₁ being RealLinearSpace
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 Th81: :: RLSUB_2:81

canceled;

theorem Th82: :: RLSUB_2:82

canceled;

theorem Th83: :: RLSUB_2:83

canceled;

theorem Th84: :: RLSUB_2:84

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "/\" b₂ = b₂ ) holds
b₂ = Bottom b₁ by Lemma61;

theorem Th85: :: RLSUB_2:85

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "\/" b₂ = b₂ ) holds
b₂ = Top b₁ by Lemma62;