let F be Field; 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; 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; ( 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
; V is_the_direct_sum_of Lin A, Lin (B \ A)
A3:
(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:39;
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)));
v in W
A4:
B is
linearly-independent
by A2, VECTSP_7:def 3;
A5:
v in (Lin A) /\ (Lin (B \ A))
;
then
v in Lin A
by VECTSP_5:3;
then consider l being
Linear_Combination of
A such that A6:
v = Sum l
by VECTSP_7:7;
v in Lin (B \ A)
by A5, VECTSP_5:3;
then consider m being
Linear_Combination of
B \ A such that A7:
v = Sum m
by VECTSP_7:7;
A8:
0. V =
(Sum l) - (Sum m)
by A6, A7, VECTSP_1:19
.=
Sum (l - m)
by VECTSP_6:47
;
A9:
(
Carrier (l - m) c= (Carrier l) \/ (Carrier m) &
A \/ (B \ A) = B )
by A1, VECTSP_6:41, XBOOLE_1:45;
A10:
(
Carrier l c= A &
Carrier m c= B \ A )
by VECTSP_6:def 4;
then
(Carrier l) \/ (Carrier m) c= A \/ (B \ A)
by XBOOLE_1:13;
then
Carrier (l - m) c= B
by A9;
then reconsider n =
l - m as
Linear_Combination of
B by VECTSP_6:def 4;
A misses B \ A
by XBOOLE_1:79;
then
Carrier n = (Carrier l) \/ (Carrier m)
by A10, Th32, XBOOLE_1:64;
then
Carrier l = {}
by A8, A4, VECTSP_7:def 1;
then
l = ZeroLC V
by VECTSP_6:def 3;
then
Sum l = 0. V
by VECTSP_6:15;
hence
v in W
by A6, VECTSP_4:35;
verum
end;
hence
(Lin A) /\ (Lin (B \ A)) = (0). V
by VECTSP_4:32;
verum
end;
(Omega). V = (Lin A) + (Lin (B \ A))
hence
V is_the_direct_sum_of Lin A, Lin (B \ A)
by A3, VECTSP_5:def 4; verum