let F be Field; :: thesis: for V being VectSp of F
for A, B being Subset of V st A c= B & B is Basis of V holds
V is_the_direct_sum_of Lin A, Lin (B \ A)
let V be VectSp of F; :: thesis: for A, B being Subset of V st A c= B & B is Basis of V holds
V is_the_direct_sum_of Lin A, Lin (B \ A)
let A, B be Subset of V; :: thesis: ( A c= B & B is Basis of V implies V is_the_direct_sum_of Lin A, Lin (B \ A) )
assume that
A1:
A c= B
and
A2:
B is Basis of V
; :: thesis: V is_the_direct_sum_of Lin A, Lin (B \ A)
A3:
(Omega). V = (Lin A) + (Lin (B \ A))
(Lin A) /\ (Lin (B \ A)) = (0). V
proof
set U =
(Lin A) /\ (Lin (B \ A));
reconsider W =
(0). V as
strict Subspace of
(Lin A) /\ (Lin (B \ A)) by VECTSP_4:50;
for
v being
Element of
((Lin A) /\ (Lin (B \ A))) holds
v in W
proof
let v be
Element of
((Lin A) /\ (Lin (B \ A)));
:: thesis: v in W
A7:
v in (Lin A) /\ (Lin (B \ A))
by STRUCT_0:def 5;
then A8:
v in Lin A
by VECTSP_5:7;
A9:
v in Lin (B \ A)
by A7, VECTSP_5:7;
consider l being
Linear_Combination of
A such that A10:
v = Sum l
by A8, VECTSP_7:12;
consider m being
Linear_Combination of
B \ A such that A11:
v = Sum m
by A9, VECTSP_7:12;
A12:
0. V =
(Sum l) - (Sum m)
by A10, A11, VECTSP_1:66
.=
Sum (l - m)
by VECTSP_6:80
;
A13:
Carrier (l - m) c= (Carrier l) \/ (Carrier m)
by VECTSP_6:74;
A14:
Carrier l c= A
by VECTSP_6:def 7;
A15:
Carrier m c= B \ A
by VECTSP_6:def 7;
A16:
A \/ (B \ A) = B
by A1, XBOOLE_1:45;
(Carrier l) \/ (Carrier m) c= A \/ (B \ A)
by A14, A15, XBOOLE_1:13;
then
Carrier (l - m) c= B
by A13, A16, XBOOLE_1:1;
then reconsider n =
l - m as
Linear_Combination of
B by VECTSP_6:def 7;
B is
linearly-independent
by A2, VECTSP_7:def 3;
then A17:
Carrier n = {}
by A12, VECTSP_7:def 1;
A misses B \ A
by XBOOLE_1:79;
then
Carrier n = (Carrier l) \/ (Carrier m)
by A14, A15, Th32, XBOOLE_1:64;
then
Carrier l = {}
by A17;
then
l = ZeroLC V
by VECTSP_6:def 6;
then
Sum l = 0. V
by VECTSP_6:41;
hence
v in W
by A10, VECTSP_4:46;
:: thesis: verum
end;
hence
(Lin A) /\ (Lin (B \ A)) = (0). V
by VECTSP_4:40;
:: thesis: verum
end;
hence
V is_the_direct_sum_of Lin A, Lin (B \ A)
by A3, VECTSP_5:def 4; :: thesis: verum