let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace 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 Subspace 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;

0. V in W2 by RLSUB_1:17;

then A1: 0. V in the carrier of W2 by STRUCT_0:def 5;

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 )

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 RLSUB_1:74;

the carrier of W1 is Coset of W1 by RLSUB_1:74;

then consider v being VECTOR of V such that

A25: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;

0. V in W1 by RLSUB_1:17;

then 0. V in the carrier of W1 by STRUCT_0:def 5;

then A26: 0. V in {v} by A25, A1, XBOOLE_0:def 4;

the carrier of ((0). V) = {(0. V)} by RLSUB_1: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). V by RLSUB_1:30; :: thesis: verum

( 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 Subspace 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;

0. V in W2 by RLSUB_1:17;

then A1: 0. V in the carrier of W2 by STRUCT_0:def 5;

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 A17:
for C1 being Coset of W1
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: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 RLSUB_1:def 6;

v1 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1;

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 RLSUB_1:def 6;

v2 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1;

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

end;for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v}

then A3: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 RLSUB_1:def 6;

v1 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1;

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 RLSUB_1:def 6;

v2 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1;

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

hence
C1 /\ C2 = {v}
; :: thesis: verum
thus A12:
{v} c= C1 /\ C2
:: according to XBOOLE_0:def 10 :: thesis: C1 /\ C2 c= {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 Th42;

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 RLSUB_1:73;

hence x in {v} by A12, A15, A16, TARSKI:def 1; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C1 /\ C2 or x in {v} )
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, Lm14;

then v21 in C2 by A8, A10, RLSUB_1:64;

then C2 = v21 + W2 by RLSUB_1:78;

then A14: x in C2 by A6, A13;

v12 = v1 - v11 by A7, Lm14;

then v12 in C1 by A4, A5, RLSUB_1:64;

then C1 = v12 + W1 by RLSUB_1:78;

then x in C1 by A9, A13;

hence x in C1 /\ C2 by A14, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {v} ; :: thesis: x in C1 /\ C2

then A13: x = v by TARSKI:def 1;

v21 = v2 - v22 by A11, Lm14;

then v21 in C2 by A8, A10, RLSUB_1:64;

then C2 = v21 + W2 by RLSUB_1:78;

then A14: x in C2 by A6, A13;

v12 = v1 - v11 by A7, Lm14;

then v12 in C1 by A4, A5, RLSUB_1:64;

then C1 = v12 + W1 by RLSUB_1:78;

then x in C1 by A9, A13;

hence x in C1 /\ C2 by A14, XBOOLE_0:def 4; :: thesis: verum

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 Th42;

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 RLSUB_1:73;

hence x in {v} by A12, A15, A16, TARSKI:def 1; :: thesis: verum

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 RLSUB_1:74;

now :: thesis: for u being VECTOR of V holds u in W1 + W2

hence
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2
by Lm12; :: according to RLSUB_2:def 4 :: thesis: W1 /\ W2 = (0). Vlet u be VECTOR of V; :: thesis: u in W1 + W2

consider C1 being Coset of W1 such that

A19: u in C1 by Lm17;

consider v being VECTOR of V such that

A20: C1 /\ the carrier of W2 = {v} by A18, A17;

A21: v in {v} by TARSKI:def 1;

then v in C1 by A20, XBOOLE_0:def 4;

then consider v1 being VECTOR of V such that

A22: v1 in W1 and

A23: u - v1 = v by A19, RLSUB_1:80;

v in the carrier of W2 by A20, A21, XBOOLE_0:def 4;

then A24: v in W2 by STRUCT_0:def 5;

u = v1 + v by A23, Lm14;

hence u in W1 + W2 by A24, A22, Th1; :: thesis: verum

end;consider C1 being Coset of W1 such that

A19: u in C1 by Lm17;

consider v being VECTOR of V such that

A20: C1 /\ the carrier of W2 = {v} by A18, A17;

A21: v in {v} by TARSKI:def 1;

then v in C1 by A20, XBOOLE_0:def 4;

then consider v1 being VECTOR of V such that

A22: v1 in W1 and

A23: u - v1 = v by A19, RLSUB_1:80;

v in the carrier of W2 by A20, A21, XBOOLE_0:def 4;

then A24: v in W2 by STRUCT_0:def 5;

u = v1 + v by A23, Lm14;

hence u in W1 + W2 by A24, A22, Th1; :: thesis: verum

the carrier of W1 is Coset of W1 by RLSUB_1:74;

then consider v being VECTOR of V such that

A25: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;

0. V in W1 by RLSUB_1:17;

then 0. V in the carrier of W1 by STRUCT_0:def 5;

then A26: 0. V in {v} by A25, A1, XBOOLE_0:def 4;

the carrier of ((0). V) = {(0. V)} by RLSUB_1: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). V by RLSUB_1:30; :: thesis: verum