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

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 v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } & the carrier of b2 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } holds
b1 = b2
by RLSUB_1:38;
end;

:: deftheorem Def1 defines + RLSUB_2:def 1 :
for V being RealLinearSpace
for W1, W2 being Subspace of V
for b4 being strict Subspace of V holds
( b4 = W1 + W2 iff the carrier of b4 = { (v + u) where v, u 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 b1 being strict Subspace of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds
b1 = b2
by RLSUB_1:38;
end;

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

theorem :: RLSUB_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: RLSUB_2:5  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 W1, W2 being Subspace of V
for x being set 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 Th6: :: RLSUB_2:6  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 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 Th7: :: RLSUB_2:7  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 W1, W2 being Subspace of V
for x being set 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:8  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 + W = W by Lm3;

theorem :: RLSUB_2:9  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 W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 by Lm1;

theorem Th10: :: RLSUB_2:10  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 W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3
proof end;

theorem Th11: :: RLSUB_2:11  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 W1, W2 being Subspace of V holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
proof end;

theorem Th12: :: RLSUB_2:12  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 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 Th13: :: RLSUB_2:13  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
( ((0). V) + W = W & W + ((0). V) = W )
proof end;

theorem Th14: :: RLSUB_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds
( ((0). V) + ((Omega). V) = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) & ((Omega). V) + ((0). V) = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) ) by Th13;

theorem Th15: :: RLSUB_2:15  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
( ((Omega). V) + W = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) )
proof end;

theorem :: RLSUB_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict RealLinearSpace holds ((Omega). V) + ((Omega). V) = V by Th15;

theorem :: RLSUB_2:17  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 /\ W = W
proof end;

theorem Th18: :: RLSUB_2:18  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 W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1
proof end;

theorem Th19: :: RLSUB_2:19  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 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 Th20: :: RLSUB_2:20  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 W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
proof end;

theorem Th21: :: RLSUB_2:21  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 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 Th22: :: RLSUB_2:22  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
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
proof end;

theorem :: RLSUB_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds
( ((0). V) /\ ((Omega). V) = (0). V & ((Omega). V) /\ ((0). V) = (0). V ) by Th22;

theorem Th24: :: RLSUB_2: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 strict Subspace of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
proof end;

theorem :: RLSUB_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict RealLinearSpace holds ((Omega). V) /\ ((Omega). V) = V by Th24;

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: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 W1, W2 being Subspace of V holds W1 /\ W2 is Subspace of W1 + W2
proof end;

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 Th27: :: RLSUB_2: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 W1 being Subspace of V
for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2
proof end;

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 Th28: :: RLSUB_2: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 W2 being Subspace of V
for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1
proof end;

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:29  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 W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3)
proof end;

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 Th30: :: RLSUB_2:30  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 W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
proof end;

Lm10: for V being RealLinearSpace
for W2, W1, 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:31  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 W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3)
proof end;

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: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 W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
proof end;

theorem Th33: :: RLSUB_2:33  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 W1, W3, W2 being Subspace of V st W1 is strict Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof end;

theorem :: RLSUB_2:34  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 W1, W2 being strict Subspace of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proof end;

theorem :: RLSUB_2:35  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 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:36  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 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;

definition
let V be RealLinearSpace;
func Subspaces V -> set means :Def3: :: RLSUB_2:def 3
for x being set holds
( x in it iff x is strict Subspace of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subspace of V )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Subspace of V ) ) & ( for x being set holds
( x in b2 iff x is strict Subspace of V ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Subspaces RLSUB_2:def 3 :
for V being RealLinearSpace
for b2 being set holds
( b2 = Subspaces V iff for x being set holds
( x in b2 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:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict RealLinearSpace holds V in Subspaces V
proof end;

definition
let V be RealLinearSpace;
let W1, W2 be Subspace of V;
pred V is_the_direct_sum_of W1,W2 means :Def4: :: RLSUB_2:def 4
( RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V );
end;

:: deftheorem Def4 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 Zero of V,the add 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 Zero of V,the add 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 Zero of V,the add 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 add-associative right_zeroed right_complementable LoopStr
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 b1 being Subspace of V st V is_the_direct_sum_of b1,W
proof end;
end;

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

registration
let V be RealLinearSpace;
let W be Subspace of V;
cluster strict Linear_Compl of W;
existence
ex b1 being Linear_Compl of W st b1 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
proof end;

theorem :: RLSUB_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:42  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 W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
proof end;

theorem Th43: :: RLSUB_2:43  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
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
proof end;

theorem Th44: :: RLSUB_2:44  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
for L being Linear_Compl of W holds
( W + L = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) & L + W = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) )
proof end;

theorem Th45: :: RLSUB_2:45  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
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
proof end;

theorem :: RLSUB_2:46  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 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 Th47: :: RLSUB_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RLSUB_2:48  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
for L being Linear_Compl of W holds W is Linear_Compl of L
proof end;

theorem :: RLSUB_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
proof end;

theorem Th50: :: RLSUB_2:50  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 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 Th51: :: RLSUB_2:51  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 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;

theorem :: RLSUB_2:52  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 W1, W2 being Subspace of V holds
( W1 + W2 = RLSStruct(# the carrier of V,the Zero of V,the add 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 Th53: :: RLSUB_2:53  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 W1, W2 being Subspace of V
for v, v1, v2, u1, u2 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;

Lm18: for X, Y being set st X c< Y holds
ex x being set st
( x in Y & not x in X )
proof end;

theorem :: RLSUB_2:54  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 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 b1 being Element of [:the carrier of V,the carrier of V:] st
( v = (b1 `1 ) + (b1 `2 ) & b1 `1 in W1 & b1 `2 in W2 )
proof end;
uniqueness
for b1, b2 being Element of [:the carrier of V,the carrier of V:] st v = (b1 `1 ) + (b1 `2 ) & b1 `1 in W1 & b1 `2 in W2 & v = (b2 `1 ) + (b2 `2 ) & b2 `1 in W1 & b2 `2 in W2 holds
b1 = b2
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 b5 being Element of [:the carrier of V,the carrier of V:] holds
( b5 = v |-- W1,W2 iff ( v = (b5 `1 ) + (b5 `2 ) & b5 `1 in W1 & b5 `2 in W2 ) );

theorem :: RLSUB_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th59: :: RLSUB_2:59  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 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 Th60: :: RLSUB_2:60  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 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:61  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
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:62  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
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:63  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
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:64  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
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- W,L) `1 = (v |-- L,W) `2
proof end;

theorem :: RLSUB_2:65  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
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- W,L) `2 = (v |-- L,W) `1
proof end;

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 b1 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
b1 . A1,A2 = W1 + W2
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . A1,A2 = W1 + W2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines SubJoin RLSUB_2:def 7 :
for V being RealLinearSpace
for b2 being BinOp of Subspaces V holds
( b2 = SubJoin V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b2 . 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 b1 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
b1 . A1,A2 = W1 /\ W2
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . A1,A2 = W1 /\ W2 ) holds
b1 = b2
proof end;
end;

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

theorem :: RLSUB_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

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

theorem Th71: :: RLSUB_2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded
proof end;

theorem Th72: :: RLSUB_2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded
proof end;

theorem Th73: :: RLSUB_2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice
proof end;

theorem Th74: :: RLSUB_2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
proof end;

Lm19: 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 ) )
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 = Bottom l
proof end;

Lm21: 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 Th75: :: RLSUB_2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) #) -> Lattice-like 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 Th71, Th72, Th74, Th75;
end;

theorem :: RLSUB_2:76  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 W1, 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:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c< Y holds
ex x being set st
( x in Y & not x in X ) by Lm18;

theorem :: RLSUB_2:78  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 add-associative right_zeroed right_complementable LoopStr
for v, v1, v2 being Element of V holds
( v = v1 + v2 iff v1 = v - v2 ) by Lm14;

theorem :: RLSUB_2:79  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 st ( for v being VECTOR of V holds v in W ) holds
W = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) by Lm12;

theorem :: RLSUB_2:80  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
for v being VECTOR of V ex C being Coset of W st v in C by Lm17;

theorem :: RLSUB_2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLSUB_2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

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

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