let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 + W2) = rank W2 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; :: thesis: for I being Basis of W1 st rank (W1 + W2) = rank W2 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
let I be Basis of W1; :: thesis: ( rank (W1 + W2) = rank W2 implies for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V )
assume A1: rank (W1 + W2) = rank W2 ; :: thesis: for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
thus for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V :: thesis: verum

proof

let v be Vector of V; :: thesis: ( v in I implies (W1 /\ W2) /\ (Lin {v}) <> (0). V )
assume C1: v in I ; :: thesis: (W1 /\ W2) /\ (Lin {v}) <> (0). V
reconsider II = I as linearly-independent Subset of V by ZMODUL03:15, VECTSP_7:def 3;
v in II by C1;
then C2: v <> 0. V by ZMODUL02:57;
C3: W1 /\ (Lin {v}) <> (0). V

proof

D1: v in W1 by C1;
D2: v in Lin {v} by ZMODUL02:65, ZFMISC_1:31;
v in II by C1;
then v <> 0. V by ZMODUL02:57;
hence W1 /\ (Lin {v}) <> (0). V by D2, ZMODUL02:66, D1, ZMODUL01:94; :: thesis: verum

end;

W2 /\ (Lin {v}) <> (0). V

proof

Lin {v} is Subspace of Lin II by ZMODUL02:70, C1, ZFMISC_1:31;
then Lin {v} is Subspace of Lin I by ZMODUL03:20;
then Lin {v} is Subspace of W1 by ZMODUL01:42;
then D1: rank ((Lin {v}) + W2) = rank W2 by A1, ThRankS5;
assume W2 /\ (Lin {v}) = (0). V ; :: thesis: contradiction
then rank ((Lin {v}) + W2) = (rank (Lin {v})) + (rank W2) by ThRankDirectSum
.= (rank W2) + 1 by C2, LmRank0a ;
hence contradiction by D1; :: thesis: verum

end;

hence (W1 /\ W2) /\ (Lin {v}) <> (0). V by C3, LmISRank21; :: thesis: verum

end;