let V be RealUnitarySpace; 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 RUSUB_1:11;
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:
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
U7 of
V, the
Mult of
V, the
scalar 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 RUSUB_1:def 5;
v1 in UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
U7 of
V, the
Mult of
V, the
scalar 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 RUSUB_1:def 5;
v2 in UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
U7 of
V, the
Mult of
V, the
scalar 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
proof
thus A12:
{v} c= C1 /\ C2
XBOOLE_0:def 10 C1 /\ C2 c= {v}proof
let x be
object ;
TARSKI:def 3 ( not x in {v} or x in C1 /\ C2 )
assume
x in {v}
;
x in C1 /\ C2
then A13:
x = v
by TARSKI:def 1;
v21 = v2 - v22
by A11, RLSUB_2:61;
then
v21 in C2
by A8, A10, RUSUB_1:58;
then
C2 = v21 + W2
by RUSUB_1:72;
then A14:
x in C2
by A6, A13, RUSUB_1:57;
v12 = v1 - v11
by A7, RLSUB_2:61;
then
v12 in C1
by A4, A5, RUSUB_1:58;
then
C1 = v12 + W1
by RUSUB_1:72;
then
x in C1
by A9, A13, RUSUB_1:57;
hence
x in C1 /\ C2
by A14, XBOOLE_0:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in C1 /\ C2 or x in {v} )
assume A15:
x in C1 /\ C2
;
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 RUSUB_1:67;
hence
x in {v}
by A12, A15, A16, TARSKI:def 1;
verum
end;
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 RUSUB_1:68;
hence
UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2
by Lm12; RUSUB_2:def 4 W1 /\ W2 = (0). V
the carrier of W1 is Coset of W1
by RUSUB_1:68;
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 RUSUB_1:11;
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 RUSUB_1:def 2
.=
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 RUSUB_1:24; verum