let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V st W1 /\ W2 = (0). V holds
rank (W1 + W2) = (rank W1) + (rank W2)
let W1, W2 be free finite-rank Subspace of V; ( W1 /\ W2 = (0). V implies rank (W1 + W2) = (rank W1) + (rank W2) )
assume A1:
W1 /\ W2 = (0). V
; rank (W1 + W2) = (rank W1) + (rank W2)
set W = W1 + W2;
reconsider WW1 = W1, WW2 = W2 as Subspace of W1 + W2 by ZMODUL01:97;
WW1 /\ WW2 =
(0). V
by A1, ZMODUL04:2
.=
(0). (W1 + W2)
by ZMODUL01:51
;
then A3:
W1 + W2 is_the_direct_sum_of WW1,WW2
by ZMODUL04:1;
reconsider WW1 = WW1, WW2 = WW2 as free finite-rank Subspace of W1 + W2 ;
set I1 = the Basis of WW1;
set I2 = the Basis of WW2;
A4:
card the Basis of WW1 = rank WW1
by ZMODUL03:def 5;
the Basis of WW1 /\ the Basis of WW2 = {}
by A3, ZMODUL04:27;
then A7: card ( the Basis of WW1 \/ the Basis of WW2) =
(card the Basis of WW1) + (card the Basis of WW2)
by CARD_2:40, XBOOLE_0:def 7
.=
(rank WW1) + (rank WW2)
by ZMODUL03:def 5, A4
;
set I = the Basis of WW1 \/ the Basis of WW2;
the carrier of WW1 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then A11:
the Basis of WW1 is Subset of (W1 + W2)
by XBOOLE_1:1;
the carrier of WW2 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
the Basis of WW2 is Subset of (W1 + W2)
by XBOOLE_1:1;
then reconsider I = the Basis of WW1 \/ the Basis of WW2 as Subset of (W1 + W2) by A11, XBOOLE_1:8;
Lin I = (Omega). (W1 + W2)
by A3, ZMODUL04:28;
then
the Basis of WW1 \/ the Basis of WW2 is Basis of (W1 + W2)
by VECTSP_7:def 3, A3, ZMODUL04:29;
hence
rank (W1 + W2) = (rank W1) + (rank W2)
by A7, ZMODUL03:def 5; verum