:: Operations on Subspaces in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received September 20, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

::
:: Definitions of sum and intersection of subspaces.
::

definition

let V be RealLinearSpace;
let W1, W2 be Subspace of V;

func W1 + W2 -> strict Subspace of V means :Def1: :: RLSUB_2:def 1
the carrier of it = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;

existence
ex b₁ being strict Subspace of V st the carrier of b₁ = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V st the carrier of b₁ = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } & the carrier of b₂ = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } holds
b₁ = b₂ by RLSUB_1:30;

end;

:: deftheorem Def1 defines + RLSUB_2:def 1 :
for V being RealLinearSpace
for W1, W2 being Subspace of V
for b₄ being strict Subspace of V holds
( b₄ = W1 + W2 iff the carrier of b₄ = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } );

definition

let V be RealLinearSpace;
let W1, W2 be Subspace of V;

func W1 /\ W2 -> strict Subspace of V means :Def2: :: RLSUB_2:def 2
the carrier of it = the carrier of W1 /\ the carrier of W2;

existence
ex b₁ being strict Subspace of V st the carrier of b₁ = the carrier of W1 /\ the carrier of W2

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V st the carrier of b₁ = the carrier of W1 /\ the carrier of W2 & the carrier of b₂ = the carrier of W1 /\ the carrier of W2 holds
b₁ = b₂ by RLSUB_1:30;

end;

:: deftheorem Def2 defines /\ RLSUB_2:def 2 :
for V being RealLinearSpace
for W1, W2 being Subspace of V
for b₄ being strict Subspace of V holds
( b₄ = W1 /\ W2 iff the carrier of b₄ = the carrier of W1 /\ the carrier of W2 );

::
:: Definitional theorems of sum and intersection of subspaces.
::

theorem Th1: :: RLSUB_2:1

for V being RealLinearSpace
for W1, W2 being Subspace of V
for x being object holds
( x in W1 + W2 iff ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )

proof end;

theorem Th2: :: RLSUB_2:2

for V being RealLinearSpace
for W1, W2 being Subspace of V
for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2

proof end;

theorem Th3: :: RLSUB_2:3

for V being RealLinearSpace
for W1, W2 being Subspace of V
for x being object holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )

proof end;

Lm1: for V being RealLinearSpace
for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1

proof end;

Lm2: for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

Lm3: for V being RealLinearSpace
for W1 being Subspace of V
for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2

proof end;

theorem :: RLSUB_2:4

for V being RealLinearSpace
for W being strict Subspace of V holds W + W = W by Lm3;

theorem :: RLSUB_2:5

for V being RealLinearSpace
for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 by Lm1;

theorem Th6: :: RLSUB_2:6

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3

proof end;

theorem Th7: :: RLSUB_2:7

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )

proof end;

theorem Th8: :: RLSUB_2:8

for V being RealLinearSpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )

proof end;

theorem Th9: :: RLSUB_2:9

for V being RealLinearSpace
for W being strict Subspace of V holds
( ((0). V) + W = W & W + ((0). V) = W )

proof end;

theorem :: RLSUB_2:10

for V being RealLinearSpace holds
( ((0). V) + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & ((Omega). V) + ((0). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Th9;

theorem Th11: :: RLSUB_2:11

for V being RealLinearSpace
for W being Subspace of V holds
( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) )

proof end;

theorem :: RLSUB_2:12

for V being strict RealLinearSpace holds ((Omega). V) + ((Omega). V) = V by Th11;

theorem :: RLSUB_2:13

for V being RealLinearSpace
for W being strict Subspace of V holds W /\ W = W

proof end;

theorem Th14: :: RLSUB_2:14

for V being RealLinearSpace
for W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1

proof end;

theorem Th15: :: RLSUB_2:15

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3

proof end;

Lm4: for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1

proof end;

theorem Th16: :: RLSUB_2:16

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )

proof end;

theorem Th17: :: RLSUB_2:17

for V being RealLinearSpace
for W2 being Subspace of V
for W1 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 /\ W2 = W1 )

proof end;

theorem Th18: :: RLSUB_2:18

for V being RealLinearSpace
for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )

proof end;

theorem :: RLSUB_2:19

for V being RealLinearSpace holds
( ((0). V) /\ ((Omega). V) = (0). V & ((Omega). V) /\ ((0). V) = (0). V ) by Th18;

theorem Th20: :: RLSUB_2:20

for V being RealLinearSpace
for W being strict Subspace of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )

proof end;

theorem :: RLSUB_2:21

for V being strict RealLinearSpace holds ((Omega). V) /\ ((Omega). V) = V by Th20;

Lm5: for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

proof end;

theorem :: RLSUB_2:22

for V being RealLinearSpace
for W1, W2 being Subspace of V holds W1 /\ W2 is Subspace of W1 + W2 by Lm5, RLSUB_1:28;

Lm6: for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

proof end;

theorem :: RLSUB_2:23

for V being RealLinearSpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2 by Lm6, RLSUB_1:30;

Lm7: for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

proof end;

theorem :: RLSUB_2:24

for V being RealLinearSpace
for W2 being Subspace of V
for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1 by Lm7, RLSUB_1:30;

Lm8: for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

proof end;

theorem :: RLSUB_2:25

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm8, RLSUB_1:28;

Lm9: for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

proof end;

theorem :: RLSUB_2:26

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm9, RLSUB_1:30;

Lm10: for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: RLSUB_2:27

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm10, RLSUB_1:28;

Lm11: for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: RLSUB_2:28

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm11, RLSUB_1:30;

theorem Th29: :: RLSUB_2:29

for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is strict Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3

proof end;

theorem :: RLSUB_2:30

for V being RealLinearSpace
for W1, W2 being strict Subspace of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )

proof end;

theorem :: RLSUB_2:31

for V being RealLinearSpace
for W1 being Subspace of V
for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3

proof end;

theorem :: RLSUB_2:32

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

proof end;

::
:: Introduction of a set of subspaces of real linear space.
::

definition

let V be RealLinearSpace;

func Subspaces V -> set means :Def3: :: RLSUB_2:def 3
for x being object holds
( x in it iff x is strict Subspace of V );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff x is strict Subspace of V )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is strict Subspace of V ) ) & ( for x being object holds
( x in b₂ iff x is strict Subspace of V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Subspaces RLSUB_2:def 3 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = Subspaces V iff for x being object holds
( x in b₂ iff x is strict Subspace of V ) );

registration

let V be RealLinearSpace;

cluster Subspaces V -> non empty ;

coherence
not Subspaces V is empty

proof end;

end;

theorem :: RLSUB_2:33

for V being strict RealLinearSpace holds V in Subspaces V

proof end;

::
:: Introduction of the direct sum of subspaces and
:: linear complement of subspace.
::

definition

let V be RealLinearSpace;
let W1, W2 be Subspace of V;

pred V is_the_direct_sum_of W1,W2 means :: RLSUB_2:def 4
( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V );

end;

:: deftheorem defines is_the_direct_sum_of RLSUB_2:def 4 :
for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( V is_the_direct_sum_of W1,W2 iff ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );

Lm12: for V being RealLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)

proof end;

Lm13: for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )

proof end;

Lm14: for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, v1, v2 being Element of V holds
( v = v1 + v2 iff v1 = v - v2 )

proof end;

Lm15: for V being RealLinearSpace
for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W

proof end;

definition

let V be RealLinearSpace;
let W be Subspace of V;

mode Linear_Compl of W -> Subspace of V means :Def5: :: RLSUB_2:def 5
V is_the_direct_sum_of it,W;

existence
ex b₁ being Subspace of V st V is_the_direct_sum_of b₁,W

proof end;

end;

:: deftheorem Def5 defines Linear_Compl RLSUB_2:def 5 :
for V being RealLinearSpace
for W, b₃ being Subspace of V holds
( b₃ is Linear_Compl of W iff V is_the_direct_sum_of b₃,W );

registration

let V be RealLinearSpace;
let W be Subspace of V;

cluster non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V136() for Linear_Compl of W;

existence
ex b₁ being Linear_Compl of W st b₁ is strict

proof end;

end;

Lm16: for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1
by Th14, Lm1;

theorem :: RLSUB_2:34

for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1 by Lm16, Def5;

theorem Th35: :: RLSUB_2:35

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) by Def5, Lm16;

::
:: Theorems concerning the direct sum of a subspaces,
:: linear complement of a subspace and coset of a subspace.
::

theorem Th36: :: RLSUB_2:36

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) )

proof end;

theorem Th37: :: RLSUB_2:37

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )

proof end;

theorem :: RLSUB_2:38

for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1 by Lm16;

theorem Th39: :: RLSUB_2:39

for V being RealLinearSpace holds
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th9, Th18;

theorem :: RLSUB_2:40

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L

proof end;

theorem :: RLSUB_2:41

for V being RealLinearSpace holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Th39, Def5;

theorem Th42: :: RLSUB_2:42

for V being RealLinearSpace
for W1, W2 being Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2

proof end;

Lm17: for V being RealLinearSpace
for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C

proof end;

theorem Th43: :: RLSUB_2:43

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} )

proof end;

::
:: Decomposition of a vector.
::

theorem :: RLSUB_2:44

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm13;

theorem Th45: :: RLSUB_2:45

for V being RealLinearSpace
for W1, W2 being Subspace of V
for u1, u2, v, v1, v2 being VECTOR of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )

proof end;

theorem :: RLSUB_2:46

for V being RealLinearSpace
for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st
for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
V is_the_direct_sum_of W1,W2

proof end;

definition

let V be RealLinearSpace;
let v be VECTOR of V;
let W1, W2 be Subspace of V;
assume A1: V is_the_direct_sum_of W1,W2 ;

func v |-- (W1,W2) -> Element of [: the carrier of V, the carrier of V:] means :Def6: :: RLSUB_2:def 6
( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

existence
ex b₁ being Element of [: the carrier of V, the carrier of V:] st
( v = (b₁ `1) + (b<sub>1</sub> `2) & b₁ `1 in W1 & b<sub>1</sub> `2 in W2 )

proof end;

uniqueness
for b₁, b₂ being Element of [: the carrier of V, the carrier of V:] st v = (b₁ `1) + (b<sub>1</sub> `2) & b₁ `1 in W1 & b<sub>1</sub> `2 in W2 & v = (b₂ `1) + (b<sub>2</sub> `2) & b₂ `1 in W1 & b<sub>2</sub> `2 in W2 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines |-- RLSUB_2:def 6 :
for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for b₅ being Element of [: the carrier of V, the carrier of V:] holds
( b₅ = v |-- (W1,W2) iff ( v = (b₅ `1) + (b<sub>5</sub> `2) & b₅ `1 in W1 & b<sub>5</sub> `2 in W2 ) );

theorem Th47: :: RLSUB_2:47

for V being RealLinearSpace
for W1, W2 being Subspace of V
for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2

proof end;

theorem Th48: :: RLSUB_2:48

for V being RealLinearSpace
for W1, W2 being Subspace of V
for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1

proof end;

theorem :: RLSUB_2:49

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)

proof end;

theorem :: RLSUB_2:50

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v

proof end;

theorem :: RLSUB_2:51

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )

proof end;

theorem :: RLSUB_2:52

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th35, Th47;

theorem :: RLSUB_2:53

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th35, Th48;

definition

let V be RealLinearSpace;

func SubJoin V -> BinOp of (Subspaces V) means :Def7: :: RLSUB_2:def 7
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 + W2;

existence
ex b₁ being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₁ . (A1,A2) = W1 + W2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₁ . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 + W2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines SubJoin RLSUB_2:def 7 :
for V being RealLinearSpace
for b₂ being BinOp of (Subspaces V) holds
( b₂ = SubJoin V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 + W2 );

definition

let V be RealLinearSpace;

func SubMeet V -> BinOp of (Subspaces V) means :Def8: :: RLSUB_2:def 8
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 /\ W2;

existence
ex b₁ being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₁ . (A1,A2) = W1 /\ W2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₁ . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 /\ W2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines SubMeet RLSUB_2:def 8 :
for V being RealLinearSpace
for b₂ being BinOp of (Subspaces V) holds
( b₂ = SubMeet V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 /\ W2 );

::
:: Definitional theorems of functions SubJoin, SubMeet.
::

theorem Th54: :: RLSUB_2:54

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

proof end;

registration

let V be RealLinearSpace;

cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> Lattice-like ;

coherence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th54;

end;

theorem Th55: :: RLSUB_2:55

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

proof end;

theorem Th56: :: RLSUB_2:56

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

proof end;

theorem Th57: :: RLSUB_2:57

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

proof end;

theorem Th58: :: RLSUB_2:58

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

proof end;

Lm18: for l being Lattice
for a, b being Element of l holds
( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) )
;

Lm19: for l being Lattice
for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds
b = Bottom l

proof end;

Lm20: for l being Lattice
for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds
b = Top l

proof end;

theorem Th59: :: RLSUB_2:59

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

proof end;

registration

let V be RealLinearSpace;

cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> modular lower-bounded upper-bounded complemented ;

coherence
( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented ) by Th55, Th56, Th58, Th59;

end;

::
:: Theorems concerning operations on subspaces (continuation). Proven
:: on the basis that set of subspaces with operations is a lattice.
::

theorem :: RLSUB_2:60

for V being RealLinearSpace
for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3

proof end;

::
:: Auxiliary theorems.
::

theorem :: RLSUB_2:61

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, v1, v2 being Element of V holds
( v = v1 + v2 iff v1 = v - v2 ) by Lm14;

theorem :: RLSUB_2:62

for V being RealLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm12;

theorem :: RLSUB_2:63

for V being RealLinearSpace
for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C by Lm17;

theorem :: RLSUB_2:64

for l being Lattice
for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds
b = Bottom l by Lm19;

theorem :: RLSUB_2:65

for l being Lattice
for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds
b = Top l by Lm20;