let V be LeftMod of INT.Ring ; for W1, W2 being free 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 free 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 I1 be 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 I2 be 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 I be Subset of V; ( 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
; I is linearly-independent
assume
I is linearly-dependent
; contradiction
then consider l being Linear_Combination of I such that
A3:
Sum l = 0. V
and
A4:
Carrier l <> {}
by VECTSP_7:def 1;
A5A:
I1 /\ I2 = {}
by A1, FRds1;
then A5B:
I1 misses I2
;
( 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, ThCarrier2;
reconsider ll1 = l1 as Linear_Combination of I by A2, XBOOLE_1:7, ZMODUL02:10;
reconsider ll2 = l2 as Linear_Combination of I by A2, XBOOLE_1:7, ZMODUL02:10;
A7:
Sum l = (Sum ll1) + (Sum ll2)
by A6, ZMODUL02:52;
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
assume B1:
Sum ll1 = 0. V
;
contradiction
II1 is
linearly-independent
by VECTSP_7:def 3, ZMODUL03:15;
then B3:
Carrier l1 = {}
by B1, VECTSP_7:def 1;
II2 is
linearly-independent
by VECTSP_7:def 3, ZMODUL03:15;
then
(Carrier ll1) \/ (Carrier ll2) = {}
by A3, A7, B1, B3, VECTSP_7:def 1;
hence
contradiction
by A4, A6, A8, ThCarrier1;
verum
end;
A13:
Sum ll1 = - (Sum ll2)
by A3, A7, RLVECT_1:6;
Sum ll1 in Lin II1
by ZMODUL02:64;
then
Sum ll1 in Lin I1
by ZMODUL03:20;
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 ZMODUL02:64;
then
Sum ll2 in Lin I2
by ZMODUL03:20;
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, ZMODUL01:38;
W1 /\ W2 = (0). V
by A1, VECTSP_5:def 4;
hence
contradiction
by A10, A14, A15, VECTSP_5:3, ZMODUL02:66; verum