let V be torsion-free Z_Module; :: thesis: for W being free finite-rank Subspace of V
for u, v being Vector of V st W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V holds
W /\ (Lin {u}) = (0). V
let W be free finite-rank Subspace of V; :: thesis: for u, v being Vector of V st W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V holds
W /\ (Lin {u}) = (0). V
let u, v be Vector of V; :: thesis: ( W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V implies W /\ (Lin {u}) = (0). V )
assume A1: ( W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V ) ; :: thesis: W /\ (Lin {u}) = (0). V
consider x being Vector of V such that
A2: ( x in (W + (Lin {u})) /\ (Lin {v}) & x <> 0. V ) by A1, ZMODUL04:24;
x in W + (Lin {u}) by A2, ZMODUL01:94;
then consider x1, x2 being Vector of V such that
A3: ( x1 in W & x2 in Lin {u} & x = x1 + x2 ) by ZMODUL01:92;
consider i being Element of INT.Ring such that
A5: x2 = i * u by A3, ThLin1;
assume W /\ (Lin {u}) <> (0). V ; :: thesis: contradiction
then consider y being Vector of V such that
A7: ( y in W /\ (Lin {u}) & y <> 0. V ) by ZMODUL04:24;
y in Lin {u} by A7, ZMODUL01:94;
then consider j being Element of INT.Ring such that
A8: y = j * u by ThLin1;
A9: j * x1 in W by A3, ZMODUL01:37;
A10: j * x2 = (j * i) * u by VECTSP_1:def 16, A5
.= i * y by A8, VECTSP_1:def 16 ;
y in W by A7, ZMODUL01:94;
then j * x2 in W by A10, ZMODUL01:37;
then (j * x1) + (j * x2) in W by A9, ZMODUL01:36;
then A11: j * x in W by A3, VECTSP_1:def 14;
x in Lin {v} by A2, ZMODUL01:94;
then j * x in Lin {v} by ZMODUL01:37;
then A12: j * x in W /\ (Lin {v}) by A11, ZMODUL01:94;
j <> 0. INT.Ring by A7, A8, ZMODUL01:1;
hence contradiction by A1, A12, ZMODUL02:66, A2, ZMODUL01:def 7; :: thesis: verum