let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st W1 /\ (Lin {v}) <> (0). V & W2 /\ (Lin {v}) <> (0). V holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
let W1, W2 be free finite-rank Subspace of V; :: thesis: for v being Vector of V st W1 /\ (Lin {v}) <> (0). V & W2 /\ (Lin {v}) <> (0). V holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
let v be Vector of V; :: thesis: ( W1 /\ (Lin {v}) <> (0). V & W2 /\ (Lin {v}) <> (0). V implies (W1 /\ W2) /\ (Lin {v}) <> (0). V )
assume A1: ( W1 /\ (Lin {v}) <> (0). V & W2 /\ (Lin {v}) <> (0). V ) ; :: thesis: (W1 /\ W2) /\ (Lin {v}) <> (0). V
consider u1 being Vector of V such that
A2: ( u1 in W1 /\ (Lin {v}) & u1 <> 0. V ) by A1, ZMODUL04:24;
consider u2 being Vector of V such that
A3: ( u2 in W2 /\ (Lin {v}) & u2 <> 0. V ) by A1, ZMODUL04:24;
A6: u1 in Lin {v} by A2, ZMODUL01:94;
then consider iu1 being Element of INT.Ring such that
A4: u1 = iu1 * v by ThLin1;
u2 in Lin {v} by A3, ZMODUL01:94;
then consider iu2 being Element of INT.Ring such that
A5: u2 = iu2 * v by ThLin1;
A7: iu2 <> 0. INT.Ring by A3, A5, ZMODUL01:1;
A8: iu2 * u1 = (iu2 * iu1) * v by VECTSP_1:def 16, A4
.= iu1 * u2 by A5, VECTSP_1:def 16 ;
u1 in W1 by A2, ZMODUL01:94;
then A9: iu2 * u1 in W1 by ZMODUL01:37;
u2 in W2 by A3, ZMODUL01:94;
then iu2 * u1 in W2 by A8, ZMODUL01:37;
then A10: iu2 * u1 in W1 /\ W2 by A9, ZMODUL01:94;
iu2 * u1 in Lin {v} by A6, ZMODUL01:37;
then iu2 * u1 in (W1 /\ W2) /\ (Lin {v}) by A10, ZMODUL01:94;
hence (W1 /\ W2) /\ (Lin {v}) <> (0). V by ZMODUL02:66, A2, A7, ZMODUL01:def 7; :: thesis: verum