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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum