let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of 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 VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: 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; :: thesis: ( 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: ( the carrier of W1 is Coset of W1 & the carrier of W2 is Coset of W2 ) by VECTSP_4:89;
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} ) :: thesis: ( ( 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 )

proof

assume A2: M is_the_direct_sum_of W1,W2 ; :: thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
let C1 be Coset of W1; :: thesis: for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
let C2 be Coset of W2; :: thesis: ex v being Element of M st C1 /\ C2 = {v}
consider v1 being Element of M such that
A3: C1 = v1 + W1 by VECTSP_4:def 6;
consider v2 being Element of M such that
A4: C2 = v2 + W2 by VECTSP_4:def 6;
A5: VectSpStr(# the carrier of M,the U7 of M,the U2 of M,the lmult of M #) = W1 + W2 by A2, Def4;
v1 in (Omega). M by RLVECT_1:3;
then consider v11, v12 being Element of M such that
A6: v11 in W1 and
A7: v12 in W2 and
A8: v1 = v11 + v12 by A5, Th5;
v2 in (Omega). M by RLVECT_1:3;
then consider v21, v22 being Element of M such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A5, Th5;
take v = v12 + v21; :: thesis: C1 /\ C2 = {v}
{v} = C1 /\ C2

proof

thus A12: {v} c= C1 /\ C2 :: according to XBOOLE_0:def 10 :: thesis: C1 /\ C2 c= {v}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in C1 /\ C2 )
assume x in {v} ; :: thesis: x in C1 /\ C2
then A13: x = v by TARSKI:def 1;
v12 = v1 - v11 by A8, VECTSP_2:22;
then v12 in C1 by A3, A6, VECTSP_4:78;
then C1 = v12 + W1 by VECTSP_4:93;
then A14: x in C1 by A9, A13;
v21 = v2 - v22 by A11, VECTSP_2:22;
then v21 in C2 by A4, A10, VECTSP_4:78;
then ( C2 = v21 + W2 & v = v21 + v12 ) by VECTSP_4:93;
then x in C2 by A7, A13;
hence x in C1 /\ C2 by A14, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C1 /\ C2 or x in {v} )
assume A15: x in C1 /\ C2 ; :: thesis: x in {v}
then C1 meets C2 by XBOOLE_0:4;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th55;
W1 /\ W2 = (0). M by A2, Def4;
then A16: ex u being Element of M st C = {u} by VECTSP_4:88;
v in {v} by TARSKI:def 1;
hence x in {v} by A12, A15, A16, TARSKI:def 1; :: thesis: verum
thus verum ; :: thesis: verum

end;

hence C1 /\ C2 = {v} ; :: thesis: verum

end;

assume A17: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ; :: thesis: M is_the_direct_sum_of W1,W2
A18: ( W1 + W2 is Subspace of (Omega). M & VectSpStr(# the carrier of M,the U7 of M,the U2 of M,the lmult of M #) = (Omega). M ) by Lm6;
the carrier of M = the carrier of (W1 + W2)

proof

thus the carrier of M c= the carrier of (W1 + W2) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (W1 + W2) c= the carrier of M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in the carrier of (W1 + W2) )
assume x in the carrier of M ; :: thesis: x in the carrier of (W1 + W2)
then reconsider u = x as Element of M ;
consider C1 being Coset of W1 such that
A19: u in C1 by VECTSP_4:84;
consider v being Element of M such that
A20: C1 /\ the carrier of W2 = {v} by A1, A17;
A21: v in {v} by TARSKI:def 1;
then v in the carrier of W2 by A20, XBOOLE_0:def 4;
then A22: v in W2 by STRUCT_0:def 5;
v in C1 by A20, A21, XBOOLE_0:def 4;
then consider v1 being Element of M such that
A23: v1 in W1 and
A24: u - v1 = v by A19, VECTSP_4:95;
u = v1 + v by A24, VECTSP_2:22;
then x in W1 + W2 by A22, A23, Th5;
hence x in the carrier of (W1 + W2) by STRUCT_0:def 5; :: thesis: verum

end;

thus the carrier of (W1 + W2) c= the carrier of M by VECTSP_4:def 2; :: thesis: verum

end;

hence VectSpStr(# the carrier of M,the U7 of M,the U2 of M,the lmult of M #) = W1 + W2 by A18, VECTSP_4:39; :: according to VECTSP_5:def 4 :: thesis: W1 /\ W2 = (0). M
consider v being Element of M such that
A25: the carrier of W1 /\ the carrier of W2 = {v} by A1, A17;
( 0. M in W1 & 0. M in W2 ) by VECTSP_4:25;
then ( 0. M in the carrier of W1 & 0. M in the carrier of W2 ) by STRUCT_0:def 5;
then A26: 0. M in {v} by A25, 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 A25, A26, TARSKI:def 1
.= the carrier of (W1 /\ W2) by Def2 ;
hence W1 /\ W2 = (0). M by VECTSP_4:37; :: thesis: verum