let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V holds
rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
let W1, W2 be free finite-rank Subspace of V; for v being Vector of V st v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V holds
rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
let v be Vector of V; ( v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V implies rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2) )
assume A1:
( v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V )
; rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
for u being Vector of V st u in W1 /\ W2 holds
u in (W1 + (Lin {v})) /\ W2
then
W1 /\ W2 is Subspace of (W1 + (Lin {v})) /\ W2
by ZMODUL01:44;
then A2:
rank ((W1 + (Lin {v})) /\ W2) >= rank (W1 /\ W2)
by ZMODUL05:2;
assume AS:
rank ((W1 + (Lin {v})) /\ W2) <> rank (W1 /\ W2)
; contradiction
ex u being Vector of V st
( u in (W1 + (Lin {v})) /\ W2 & not u in W1 /\ W2 )
then consider u being Vector of V such that
A4:
( u in (W1 + (Lin {v})) /\ W2 & not u in W1 /\ W2 )
;
u in W1 + (Lin {v})
by A4, ZMODUL01:94;
then consider u1, u2 being Vector of V such that
A5:
( u1 in W1 & u2 in Lin {v} & u = u1 + u2 )
by ZMODUL01:92;
A6:
u in W2
by A4, ZMODUL01:94;
A7:
u2 <> 0. V
by A4, A5, A6, ZMODUL01:94;
A8:
- u1 in W1
by A5, ZMODUL01:38;
u - u1 =
u2 + (u1 - u1)
by RLVECT_1:28, A5
.=
u2 + (0. V)
by RLVECT_1:15
.=
u2
;
then
u2 in W1 + W2
by A6, A8, ZMODUL01:92;
hence
contradiction
by A1, A7, ZMODUL02:66, A5, ZMODUL01:94; verum