let R be Ring; for V being LeftMod of R
for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st
for v1, v2, u1, u2 being Vector of V st v1 + v2 = 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
let V be LeftMod of R; for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st
for v1, v2, u1, u2 being Vector of V st v1 + v2 = 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
let W1, W2 be Submodule of V; ( V = W1 + W2 & ex v being Vector of V st
for v1, v2, u1, u2 being Vector of V st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) implies V is_the_direct_sum_of W1,W2 )
assume A1:
V = W1 + W2
; ( for v being Vector of V ex v1, v2, u1, u2 being Vector of V st
( v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or V is_the_direct_sum_of W1,W2 )
( the carrier of ((0). V) = {(0. V)} & (0). V is Submodule of W1 /\ W2 )
by Th54, VECTSP_4:def 3;
then A2:
{(0. V)} c= the carrier of (W1 /\ W2)
by VECTSP_4:def 2;
given v being Vector of V such that A3:
for v1, v2, u1, u2 being Vector of V st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
; V is_the_direct_sum_of W1,W2
assume
not V is_the_direct_sum_of W1,W2
; contradiction
then
the carrier of (W1 /\ W2) <> {(0. V)}
by VECTSP_4:def 3, A1;
then
{(0. V)} c< the carrier of (W1 /\ W2)
by A2;
then consider x being object such that
A4:
x in the carrier of (W1 /\ W2)
and
A5:
not x in {(0. V)}
by XBOOLE_0:6;
A6:
x <> 0. V
by A5, TARSKI:def 1;
A7:
x in W1 /\ W2
by A4;
then
x in V
by Th24;
then reconsider u = x as Vector of V ;
consider v1, v2 being Vector of V such that
A8:
v1 in W1
and
A9:
v2 in W2
and
A10:
v = v1 + v2
by A1, Lm17;
A11: v =
(v1 + v2) + (0. V)
by A10, RLVECT_1:4
.=
(v1 + v2) + (u - u)
by RLVECT_1:15
.=
((v1 + v2) + u) - u
by RLVECT_1:def 3
.=
((v1 + u) + v2) - u
by RLVECT_1:def 3
.=
(v1 + u) + (v2 - u)
by RLVECT_1:def 3
;
x in W2
by A7, Th94;
then A12:
v2 - u in W2
by A9, Th39;
x in W1
by A7, Th94;
then
v1 + u in W1
by A8, Th36;
then v2 - u =
v2
by A3, A8, A9, A10, A11, A12
.=
v2 - (0. V)
by RLVECT_1:13
;
hence
contradiction
by A6, RLVECT_1:23; verum