let V be RealLinearSpace; 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; ( 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} )
( ( 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
;
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;
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v}let C2 be
Coset of
W2;
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;
C1 /\ C2 = {v}
{v} = C1 /\ C2
hence
C1 /\ C2 = {v}
;
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}
; V is_the_direct_sum_of W1,W2
A18:
the carrier of W2 is Coset of W2
by RLSUB_1:74;
hence
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2
by Lm12; RLSUB_2:def 4 W1 /\ W2 = (0). V
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; verum