let K be Field; for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st W1 /\ W2 = (0). V holds
I1 \/ I2 is Basis of (W1 + W2)
let V be VectSp of K; for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st W1 /\ W2 = (0). V holds
I1 \/ I2 is Basis of (W1 + W2)
let W1, W2 be Subspace of V; for I1 being Basis of W1
for I2 being Basis of W2 st W1 /\ W2 = (0). V holds
I1 \/ I2 is Basis of (W1 + W2)
let I1 be Basis of W1; for I2 being Basis of W2 st W1 /\ W2 = (0). V holds
I1 \/ I2 is Basis of (W1 + W2)
let I2 be Basis of W2; ( W1 /\ W2 = (0). V implies I1 \/ I2 is Basis of (W1 + W2) )
assume P1:
W1 /\ W2 = (0). V
; I1 \/ I2 is Basis of (W1 + W2)
set I = I1 \/ I2;
reconsider W = W1 + W2 as strict Subspace of V ;
reconsider WW1 = W1, WW2 = W2 as Subspace of W by VECTSP_5:7;
( the carrier of WW1 c= the carrier of W & the carrier of WW2 c= the carrier of W )
by VECTSP_4:def 2;
then
( I1 c= the carrier of W & I2 c= the carrier of W )
;
then reconsider I0 = I1 \/ I2 as Subset of W by XBOOLE_1:8;
reconsider I10 = I1 as Basis of WW1 ;
reconsider I20 = I2 as Basis of WW2 ;
A2:
WW1 /\ WW2 is Subspace of V
by VECTSP_4:26;
A3:
WW1 + WW2 is Subspace of V
by VECTSP_4:26;
for x being object holds
( x in WW1 /\ WW2 iff x in (0). V )
then
for x being Vector of V holds
( x in WW1 /\ WW2 iff x in (0). V )
;
then A4: WW1 /\ WW2 =
(0). V
by A2, VECTSP_4:30
.=
(0). W
by VECTSP_4:36
;
for x being object holds
( x in W iff x in WW1 + WW2 )
proof
let x be
object ;
( x in W iff x in WW1 + WW2 )
hereby ( x in WW1 + WW2 implies x in W )
end;
assume
x in WW1 + WW2
;
x in W
then consider x1,
x2 being
Vector of
W such that B2:
(
x1 in WW1 &
x2 in WW2 &
x = x1 + x2 )
by VECTSP_5:1;
thus
x in W
by B2;
verum
end;
then
for x being Vector of V holds
( x in W iff x in WW1 + WW2 )
;
then
W = WW1 + WW2
by A3, VECTSP_4:30;
then
I0 is base
by A4, FRds2, FRds3, VECTSP_5:def 4;
hence
I1 \/ I2 is Basis of (W1 + W2)
; verum