let K be Field; 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; 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:7;
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)
;
A4:
W1 is Subspace of W1 + W2
by VECTSP_5:7;
then
the carrier of W1 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
B1 c= the carrier of (W1 + W2)
;
then reconsider B12 = B1 \/ B2, B19 = B1, B29 = B2 as Subset of (W1 + W2) by A3, XBOOLE_1:8;
A5: (Omega). W2 =
Lin B2
by VECTSP_7:def 3
.=
Lin B29
by A2, VECTSP_9:17
;
A6:
Lin B12 = (Lin B19) + (Lin B29)
by VECTSP_7:15;
A7: (Omega). W1 =
Lin B1
by VECTSP_7:def 3
.=
Lin B19
by A4, VECTSP_9:17
;
A8:
the carrier of (W1 + W2) c= the carrier of (Lin B12)
proof
let x be
object ;
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 x =
x as
Vector of
(W1 + W2) by A9;
x in W1 + W2
;
then consider v1,
v2 being
Vector of
V such that A10:
v1 in W1
and A11:
v2 in W2
and A12:
x = v1 + v2
by VECTSP_5:1;
(
v1 is
Vector of
W1 &
v2 is
Vector of
W2 )
by A10, A11;
then reconsider w1 =
v1,
w2 =
v2 as
Vector of
(W1 + W2) by A4, A2, VECTSP_4:10;
A13:
v1 + v2 = w1 + w2
by VECTSP_4:13;
v2 in the
carrier of
(Lin B29)
by A5, A11;
then A14:
v2 in Lin B29
;
v1 in the
carrier of
(Lin B19)
by A7, A10;
then
v1 in Lin B19
;
then
w1 + w2 in Lin B12
by A6, A14, VECTSP_5:1;
hence
x in the
carrier of
(Lin B12)
by A12, A13;
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 = ModuleStr(# the carrier of (W1 + W2), the addF of (W1 + W2), the ZeroF of (W1 + W2), the lmult of (W1 + W2) #)
by VECTSP_4:31;
( B2 is linearly-independent & B1 is linearly-independent )
by VECTSP_7:def 3;
then
B1 \/ B2 is linearly-independent Subset of (W1 + W2)
by A1, Th2;
hence
B1 \/ B2 is Basis of (W1 + W2)
by A15, VECTSP_7:def 3; verum