let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 /\ W2) = rank W1 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
let W1, W2 be free finite-rank Subspace of V; for I being Basis of W1 st rank (W1 /\ W2) = rank W1 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
let I be Basis of W1; ( rank (W1 /\ W2) = rank W1 implies for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V )
assume A1:
rank (W1 /\ W2) = rank W1
; for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
assume
ex v being Vector of V st
( v in I & (W1 /\ W2) /\ (Lin {v}) = (0). V )
; contradiction
then consider v being Vector of V such that
A2:
( v in I & (W1 /\ W2) /\ (Lin {v}) = (0). V )
;
reconsider II = I as linearly-independent Subset of V by ZMODUL03:15, VECTSP_7:def 3;
A4X: (Omega). W1 =
Lin I
by VECTSP_7:def 3
.=
Lin II
by ZMODUL03:20
;
then A4:
( (Omega). W1 = (Lin (II \ {v})) + (Lin {v}) & (Lin (II \ {v})) /\ (Lin {v}) = (0). V & Lin (II \ {v}) is free & Lin {v} is free & v <> 0. V )
by A2, ThLin8;
reconsider LIv = Lin (II \ {v}) as free finite-rank Subspace of V ;
reconsider W1s = (Omega). W1, W2s = (Omega). W2 as strict free finite-rank Subspace of V by ZMODUL01:42;
rank W1s =
rank ((W1s /\ W2s) + W1s)
by ZMODUL01:112
.=
rank ((W1 /\ W2) + W1s)
by ZMODUL04:23
;
then A6:
rank W1 = rank ((W1 /\ W2) + W1s)
by ZMODUL05:4;
(W1 /\ W2) + W1s =
(W1 /\ W2) + (LIv + (Lin {v}))
by A4X, A2, ThLin8
.=
((W1 /\ W2) + (Lin {v})) + LIv
by ZMODUL01:96
;
then
(W1 /\ W2) + (Lin {v}) is Subspace of (W1 /\ W2) + W1s
by ZMODUL01:97;
then A8:
rank ((W1 /\ W2) + (Lin {v})) <= rank W1
by A6, ZMODUL05:2;
rank ((W1 /\ W2) + (Lin {v})) =
(rank (W1 /\ W2)) + (rank (Lin {v}))
by A2, ThRankDirectSum
.=
(rank W1) + 1
by A1, A4, LmRank0a
;
hence
contradiction
by A8, NAT_1:13; verum