begin
Lm1:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
Lm2:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
Lm3:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
Lm4:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
Lm5:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
Lm6:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
Lm7:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
Lm8:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
Lm9:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
Lm10:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
Lm11:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
Lm12:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
Lm13:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
Lm14:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
Lm15:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
Lm16:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
Lm17:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
M is_the_direct_sum_of W2,W1
definition
let GF be non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over
GF;
existence
ex b1 being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
uniqueness
for b1, b2 being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
end;
definition
let GF be non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over
GF;
existence
ex b1 being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
uniqueness
for b1, b2 being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
end;