let K be Field; :: thesis: 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

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let V be VectSp of K; :: thesis: for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let W1, W2 be Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I2 be Basis of W2; :: thesis: for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I be Subset of V; :: thesis: ( V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 implies I is linearly-independent )

assume that

A1: V is_the_direct_sum_of W1,W2 and

A2: I = I1 \/ I2 ; :: thesis: I is linearly-independent

assume I is linearly-dependent ; :: thesis: contradiction

then consider l being Linear_Combination of I such that

A3: Sum l = 0. V and

A4: Carrier l <> {} ;

A5A: I1 /\ I2 = {} by A1, FRds1;

A5B: I1 misses I2 by A1, FRds1;

( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by VECTSP_4:def 2;

then reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1:1;

consider l1 being Linear_Combination of II1, l2 being Linear_Combination of II2 such that

A6: l = l1 + l2 by A2, A5A, ZMODUL04:26;

reconsider ll1 = l1 as Linear_Combination of I by A2, XBOOLE_1:7, VECTSP_6:4;

reconsider ll2 = l2 as Linear_Combination of I by A2, XBOOLE_1:7, VECTSP_6:4;

A7: Sum l = (Sum ll1) + (Sum ll2) by A6, VECTSP_6:44;

set v1 = Sum ll1;

set v2 = Sum ll2;

( Carrier ll1 c= I1 & Carrier ll2 c= I2 ) by VECTSP_6:def 4;

then A8: (Carrier ll1) /\ (Carrier ll2) = {} by A5B, XBOOLE_0:def 7, XBOOLE_1:64;

A10: Sum ll1 <> 0. V

Sum ll1 in Lin II1 by VECTSP_7:7;

then Sum ll1 in Lin I1 by VECTSP_9:17;

then Sum ll1 in ModuleStr(# the carrier of W1, the addF of W1, the ZeroF of W1, the lmult of W1 #) by VECTSP_7:def 3;

then A14: Sum ll1 in W1 ;

Sum ll2 in Lin II2 by VECTSP_7:7;

then Sum ll2 in Lin I2 by VECTSP_9:17;

then Sum ll2 in ModuleStr(# the carrier of W2, the addF of W2, the ZeroF of W2, the lmult of W2 #) by VECTSP_7:def 3;

then Sum ll2 in W2 ;

then A15: Sum ll1 in W2 by A13, VECTSP_4:22;

W1 /\ W2 = (0). V by A1, VECTSP_5:def 4;

hence contradiction by A10, A14, A15, VECTSP_5:3, VECTSP_4:35; :: thesis: verum

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let V be VectSp of K; :: thesis: for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let W1, W2 be Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I2 be Basis of W2; :: thesis: for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

let I be Subset of V; :: thesis: ( V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 implies I is linearly-independent )

assume that

A1: V is_the_direct_sum_of W1,W2 and

A2: I = I1 \/ I2 ; :: thesis: I is linearly-independent

assume I is linearly-dependent ; :: thesis: contradiction

then consider l being Linear_Combination of I such that

A3: Sum l = 0. V and

A4: Carrier l <> {} ;

A5A: I1 /\ I2 = {} by A1, FRds1;

A5B: I1 misses I2 by A1, FRds1;

( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by VECTSP_4:def 2;

then reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1:1;

consider l1 being Linear_Combination of II1, l2 being Linear_Combination of II2 such that

A6: l = l1 + l2 by A2, A5A, ZMODUL04:26;

reconsider ll1 = l1 as Linear_Combination of I by A2, XBOOLE_1:7, VECTSP_6:4;

reconsider ll2 = l2 as Linear_Combination of I by A2, XBOOLE_1:7, VECTSP_6:4;

A7: Sum l = (Sum ll1) + (Sum ll2) by A6, VECTSP_6:44;

set v1 = Sum ll1;

set v2 = Sum ll2;

( Carrier ll1 c= I1 & Carrier ll2 c= I2 ) by VECTSP_6:def 4;

then A8: (Carrier ll1) /\ (Carrier ll2) = {} by A5B, XBOOLE_0:def 7, XBOOLE_1:64;

A10: Sum ll1 <> 0. V

proof

A13:
Sum ll1 = - (Sum ll2)
by A3, A7, RLVECT_1:6;
assume B1:
Sum ll1 = 0. V
; :: thesis: contradiction

II1 is linearly-independent by VECTSP_7:def 3, VECTSP_9:11;

then B3: Carrier l1 = {} by B1;

II2 is linearly-independent by VECTSP_7:def 3, VECTSP_9:11;

then (Carrier ll1) \/ (Carrier ll2) = {} by A3, A7, B1, B3;

hence contradiction by A4, A6, A8, ZMODUL04:25; :: thesis: verum

end;II1 is linearly-independent by VECTSP_7:def 3, VECTSP_9:11;

then B3: Carrier l1 = {} by B1;

II2 is linearly-independent by VECTSP_7:def 3, VECTSP_9:11;

then (Carrier ll1) \/ (Carrier ll2) = {} by A3, A7, B1, B3;

hence contradiction by A4, A6, A8, ZMODUL04:25; :: thesis: verum

Sum ll1 in Lin II1 by VECTSP_7:7;

then Sum ll1 in Lin I1 by VECTSP_9:17;

then Sum ll1 in ModuleStr(# the carrier of W1, the addF of W1, the ZeroF of W1, the lmult of W1 #) by VECTSP_7:def 3;

then A14: Sum ll1 in W1 ;

Sum ll2 in Lin II2 by VECTSP_7:7;

then Sum ll2 in Lin I2 by VECTSP_9:17;

then Sum ll2 in ModuleStr(# the carrier of W2, the addF of W2, the ZeroF of W2, the lmult of W2 #) by VECTSP_7:def 3;

then Sum ll2 in W2 ;

then A15: Sum ll1 in W2 by A13, VECTSP_4:22;

W1 /\ W2 = (0). V by A1, VECTSP_5:def 4;

hence contradiction by A10, A14, A15, VECTSP_5:3, VECTSP_4:35; :: thesis: verum