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 st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
M is_the_direct_sum_of W1,W2
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 st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
M is_the_direct_sum_of W1,W2
let W1, W2 be Subspace of M; ( M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) implies M is_the_direct_sum_of W1,W2 )
assume A1:
M = W1 + W2
; ( for v being Element of M ex v1, v2, u1, u2 being Element of M st
( v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or M is_the_direct_sum_of W1,W2 )
( the carrier of ((0). M) = {(0. M)} & (0). M is Subspace of W1 /\ W2 )
by VECTSP_4:39, VECTSP_4:def 3;
then A2:
{(0. M)} c= the carrier of (W1 /\ W2)
by VECTSP_4:def 2;
given v being Element of M such that A3:
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
; M is_the_direct_sum_of W1,W2
assume
not M is_the_direct_sum_of W1,W2
; contradiction
then
W1 /\ W2 <> (0). M
by A1;
then
the carrier of (W1 /\ W2) <> {(0. M)}
by VECTSP_4:def 3;
then
{(0. M)} 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. M)}
by XBOOLE_0:6;
A6:
x in W1 /\ W2
by A4, STRUCT_0:def 5;
then
x in M
by VECTSP_4:9;
then reconsider u = x as Element of M by STRUCT_0:def 5;
consider v1, v2 being Element of M such that
A7:
v1 in W1
and
A8:
v2 in W2
and
A9:
v = v1 + v2
by A1, Lm16;
A10: v =
(v1 + v2) + (0. M)
by A9, RLVECT_1:4
.=
(v1 + v2) + (u - u)
by VECTSP_1:19
.=
((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 A6, Th3;
then A11:
v2 - u in W2
by A8, VECTSP_4:23;
x in W1
by A6, Th3;
then
v1 + u in W1
by A7, VECTSP_4:20;
then
v2 - u = v2
by A3, A7, A8, A9, A10, A11;
then
v2 + (- u) = v2 + (0. M)
by RLVECT_1:4;
then
- u = 0. M
by RLVECT_1:8;
then A12:
u = - (0. M)
by RLVECT_1:17;
x <> 0. M
by A5, TARSKI:def 1;
hence
contradiction
by A12, RLVECT_1:12; verum