let K be Field; for V being VectSp of
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
let V be VectSp of ; for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
let W1, W2 be Subspace of V; ( W1 /\ W2 = (0). V implies for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2 )
assume A1:
W1 /\ W2 = (0). V
; for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
let B1 be Basis of W1; for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
let B2 be Basis of W2; B1 \/ B2 is Basis of W1 + W2
A2:
W2 is Subspace of W1 + W2
by VECTSP_5:11;
then
the carrier of W2 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then A3:
B2 c= the carrier of (W1 + W2)
by XBOOLE_1:1;
A4:
W1 is Subspace of W1 + W2
by VECTSP_5:11;
then
the carrier of W1 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
B1 c= the carrier of (W1 + W2)
by XBOOLE_1:1;
then reconsider B12 = B1 \/ B2, B1' = B1, B2' = B2 as Subset of by A3, XBOOLE_1:8;
A5: (Omega). W2 =
Lin B2
by VECTSP_7:def 3
.=
Lin B2'
by A2, VECTSP_9:21
;
A6:
Lin B12 = (Lin B1') + (Lin B2')
by VECTSP_7:20;
A7: (Omega). W1 =
Lin B1
by VECTSP_7:def 3
.=
Lin B1'
by A4, VECTSP_9:21
;
A8:
the carrier of (W1 + W2) c= the carrier of (Lin B12)
proof
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (W1 + W2) or x in the carrier of (Lin B12) )
assume A9:
x in the
carrier of
(W1 + W2)
;
x in the carrier of (Lin B12)
reconsider v =
x as
Vector of
by A9;
x in W1 + W2
by A9, STRUCT_0:def 5;
then consider v1,
v2 being
Vector of
such that A10:
v1 in W1
and A11:
v2 in W2
and A12:
x = v1 + v2
by VECTSP_5:5;
(
v1 is
Vector of &
v2 is
Vector of )
by A10, A11, STRUCT_0:def 5;
then reconsider w1 =
v1,
w2 =
v2 as
Vector of
by A4, A2, VECTSP_4:18;
A13:
v1 + v2 = w1 + w2
by VECTSP_4:21;
v2 in the
carrier of
(Lin B2')
by A5, A11, STRUCT_0:def 5;
then A14:
v2 in Lin B2'
by STRUCT_0:def 5;
v1 in the
carrier of
(Lin B1')
by A7, A10, STRUCT_0:def 5;
then
v1 in Lin B1'
by STRUCT_0:def 5;
then
w1 + w2 in Lin B12
by A6, A14, VECTSP_5:5;
hence
x in the
carrier of
(Lin B12)
by A12, A13, STRUCT_0:def 5;
verum
end;
the carrier of (Lin B12) c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
the carrier of (Lin B12) = the carrier of (W1 + W2)
by A8, XBOOLE_0:def 10;
then A15:
Lin B12 = VectSpStr(# the carrier of (W1 + W2),the addF of (W1 + W2),the U2 of (W1 + W2),the lmult of (W1 + W2) #)
by VECTSP_4:39;
( B2 is linearly-independent & B1 is linearly-independent )
by VECTSP_7:def 3;
then
B1 \/ B2 is linearly-independent Subset of
by A1, Th2;
hence
B1 \/ B2 is Basis of W1 + W2
by A15, VECTSP_7:def 3; verum
reconsider W1' = W1, W2' = W2 as Subspace of W1 + W2 by VECTSP_5:11;