let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
let W1, W2 be Subspace of M; ( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1:
W1 + W2 is Subspace of (Omega). M
by Lm6;
thus
( M is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ) implies M is_the_direct_sum_of W1,W2 )
assume A17:
for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
; M is_the_direct_sum_of W1,W2
A18:
the carrier of W2 is Coset of W2
by VECTSP_4:73;
A19:
the carrier of M c= the carrier of (W1 + W2)
the carrier of W1 is Coset of W1
by VECTSP_4:73;
then consider v being Element of M such that
A26:
the carrier of W1 /\ the carrier of W2 = {v}
by A18, A17;
the carrier of (W1 + W2) c= the carrier of M
by VECTSP_4:def 2;
then
the carrier of M = the carrier of (W1 + W2)
by A19;
hence
ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2
by A1, VECTSP_4:31; VECTSP_5:def 4 W1 /\ W2 = (0). M
0. M in W2
by VECTSP_4:17;
then A27:
0. M in the carrier of W2
by STRUCT_0:def 5;
0. M in W1
by VECTSP_4:17;
then
0. M in the carrier of W1
by STRUCT_0:def 5;
then A28:
0. M in {v}
by A26, A27, XBOOLE_0:def 4;
the carrier of ((0). M) =
{(0. M)}
by VECTSP_4:def 3
.=
the carrier of W1 /\ the carrier of W2
by A26, A28, TARSKI:def 1
.=
the carrier of (W1 /\ W2)
by Def2
;
hence
W1 /\ W2 = (0). M
by VECTSP_4:29; verum