let K be Field; :: thesis: for V being VectSp of K
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 K; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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; :: thesis: for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
let B2 be Basis of W2; :: thesis: B1 \/ B2 is Basis of W1 + W2
A2:
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
by VECTSP_5:11;
then
( the carrier of W1 c= the carrier of (W1 + W2) & the carrier of W2 c= the carrier of (W1 + W2) )
by VECTSP_4:def 2;
then
( B1 c= the carrier of (W1 + W2) & B2 c= the carrier of (W1 + W2) )
by XBOOLE_1:1;
then reconsider B12 = B1 \/ B2, B1' = B1, B2' = B2 as Subset of (W1 + W2) by XBOOLE_1:8;
reconsider W1' = W1, W2' = W2 as Subspace of W1 + W2 by VECTSP_5:11;
A3: (Omega). W1 =
Lin B1
by VECTSP_7:def 3
.=
Lin B1'
by A2, VECTSP_9:21
;
A4: (Omega). W2 =
Lin B2
by VECTSP_7:def 3
.=
Lin B2'
by A2, VECTSP_9:21
;
A5:
Lin B12 = (Lin B1') + (Lin B2')
by VECTSP_7:20;
A6:
the carrier of (Lin B12) c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
the carrier of (W1 + W2) c= the carrier of (Lin B12)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of (Lin B12) )
assume A7:
x in the
carrier of
(W1 + W2)
;
:: thesis: x in the carrier of (Lin B12)
reconsider v =
x as
Vector of
(W1 + W2) by A7;
x in W1 + W2
by A7, STRUCT_0:def 5;
then consider v1,
v2 being
Vector of
V such that A8:
(
v1 in W1 &
v2 in W2 &
x = v1 + v2 )
by VECTSP_5:5;
(
v1 is
Vector of
W1 &
v2 is
Vector of
W2 )
by A8, STRUCT_0:def 5;
then reconsider w1 =
v1,
w2 =
v2 as
Vector of
(W1 + W2) by A2, VECTSP_4:18;
(
v1 in the
carrier of
(Lin B1') &
v2 in the
carrier of
(Lin B2') )
by A3, A4, A8, STRUCT_0:def 5;
then
(
v1 in Lin B1' &
v2 in Lin B2' )
by STRUCT_0:def 5;
then
(
w1 + w2 in Lin B12 &
v1 + v2 = w1 + w2 )
by A5, VECTSP_4:21, VECTSP_5:5;
hence
x in the
carrier of
(Lin B12)
by A8, STRUCT_0:def 5;
:: thesis: verum
end;
then
the carrier of (Lin B12) = the carrier of (W1 + W2)
by A6, XBOOLE_0:def 10;
then A9:
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 (W1 + W2)
by Th2, A1;
hence
B1 \/ B2 is Basis of W1 + W2
by A9, VECTSP_7:def 3; :: thesis: verum