let R be Ring; :: thesis: for V being RightMod of R
for W1, W2 being Submodule 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} )
let V be RightMod of R; :: thesis: for W1, W2 being Submodule 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} )
let W1, W2 be Submodule of V; :: thesis: ( 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} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1: W1 + W2 is Submodule of (Omega). V by Lm5;
thus ( V is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ) :: thesis: ( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ) implies V is_the_direct_sum_of W1,W2 )

proof

assume A2: V is_the_direct_sum_of W1,W2 ; :: thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v}
then A3: RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 ;
let C1 be Coset of W1; :: thesis: for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v}
let C2 be Coset of W2; :: thesis: ex v being Vector of V st C1 /\ C2 = {v}
consider v1 being Vector of V such that
A4: C1 = v1 + W1 by RMOD_2:def 6;
v1 in (Omega). V ;
then consider v11, v12 being Vector of V such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3, Th1;
consider v2 being Vector of V such that
A8: C2 = v2 + W2 by RMOD_2:def 6;
v2 in (Omega). V ;
then consider v21, v22 being Vector of V such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3, Th1;
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 object ; :: 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;
v21 = v2 - v22 by A11, Lm15;
then v21 in C2 by A8, A10, RMOD_2:59;
then C2 = v21 + W2 by RMOD_2:74;
then A14: x in C2 by A6, A13;
v12 = v1 - v11 by A7, Lm15;
then v12 in C1 by A4, A5, RMOD_2:59;
then C1 = v12 + W1 by RMOD_2:74;
then x in C1 by A9, A13;
hence x in C1 /\ C2 by A14, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: 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 ;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th40;
A16: v in {v} by TARSKI:def 1;
W1 /\ W2 = (0). V by A2;
then ex u being Vector of V st C = {u} by RMOD_2:69;
hence x in {v} by A12, A15, A16, TARSKI:def 1; :: 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 Vector of V st C1 /\ C2 = {v} ; :: thesis: V is_the_direct_sum_of W1,W2
A18: the carrier of W2 is Coset of W2 by RMOD_2:70;
A19: the carrier of V c= the carrier of (W1 + W2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of V or x in the carrier of (W1 + W2) )
assume x in the carrier of V ; :: thesis: x in the carrier of (W1 + W2)
then reconsider u = x as Vector of V ;
consider C1 being Coset of W1 such that
A20: u in C1 by RMOD_2:65;
consider v being Vector of V such that
A21: C1 /\ the carrier of W2 = {v} by A18, A17;
A22: v in {v} by TARSKI:def 1;
then v in C1 by A21, XBOOLE_0:def 4;
then consider v1 being Vector of V such that
A23: v1 in W1 and
A24: u - v1 = v by A20, RMOD_2:76;
v in the carrier of W2 by A21, A22, XBOOLE_0:def 4;
then A25: v in W2 ;
u = v1 + v by A24, Lm15;
then x in W1 + W2 by A25, A23, Th1;
hence x in the carrier of (W1 + W2) ; :: thesis: verum

end;

the carrier of W1 is Coset of W1 by RMOD_2:70;
then consider v being Vector of V such that
A26: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;
the carrier of (W1 + W2) c= the carrier of V by RMOD_2:def 2;
then the carrier of V = the carrier of (W1 + W2) by A19;
hence RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 by A1, RMOD_2:31; :: according to RMOD_3:def 4 :: thesis: W1 /\ W2 = (0). V
0. V in W2 by RMOD_2:17;
then A27: 0. V in the carrier of W2 ;
0. V in W1 by RMOD_2:17;
then 0. V in the carrier of W1 ;
then A28: 0. V in {v} by A26, A27, XBOOLE_0:def 4;
the carrier of ((0). V) = {(0. V)} by RMOD_2: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). V by RMOD_2:29; :: thesis: verum