let V be torsion-free Z_Module; :: thesis: for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} )
let v1, v2 be Vector of V; :: thesis: ( v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V implies ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} ) )
assume A1: ( v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V ) ; :: thesis: ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} )
consider x being Vector of V such that
A2: ( x in (Lin {v1}) /\ (Lin {v2}) & x <> 0. V ) by A1, ZMODUL04:24;
x in Lin {v1} by A2, ZMODUL01:94;
then consider ii1 being Element of INT.Ring such that
A4: x = ii1 * v1 by ThLin1;
x in Lin {v2} by A2, ZMODUL01:94;
then consider ii2 being Element of INT.Ring such that
A6: x = ii2 * v2 by ThLin1;
A8: ii1 <> 0 by A2, A4, ZMODUL01:1;
consider i1, i2 being Integer such that
A10: ( ii1 = (ii1 gcd ii2) * i1 & ii2 = (ii1 gcd ii2) * i2 & i1,i2 are_coprime ) by A8, INT_2:23;
reconsider I1 = i1, I2 = i2 as Element of INT.Ring by INT_1:def 2;
AX1: ii1 gcd ii2 <> 0 by A8, INT_2:5;
reconsider igi = ii1 gcd ii2 as Element of INT.Ring by INT_1:def 2;
a10: ( ii1 = igi * I1 & ii2 = igi * I2 ) by A10;
then A11: x = igi * (I1 * v1) by VECTSP_1:def 16, A4;
x = igi * (I2 * v2) by VECTSP_1:def 16, A6, a10;
then A12: I1 * v1 = I2 * v2 by A11, AX1, ZMODUL01:10;
( I1 * v1 in Lin {v1} & I2 * v2 in Lin {v2} ) by ZMODUL01:37, ThLin2;
then A13: I1 * v1 in (Lin {v1}) /\ (Lin {v2}) by A12, ZMODUL01:94;
A14: for y being Vector of V st y in Lin {(I1 * v1)} holds
y in (Lin {v1}) /\ (Lin {v2})

proof

let y be Vector of V; :: thesis: ( y in Lin {(I1 * v1)} implies y in (Lin {v1}) /\ (Lin {v2}) )
assume B1: y in Lin {(I1 * v1)} ; :: thesis: y in (Lin {v1}) /\ (Lin {v2})
consider iy being Element of INT.Ring such that
B2: y = iy * (I1 * v1) by B1, ThLin1;
thus y in (Lin {v1}) /\ (Lin {v2}) by A13, B2, ZMODUL01:37; :: thesis: verum

end;

A16: Lin {(I1 * v1)} = (Lin {v1}) /\ (Lin {v2})

proof

assume Lin {(I1 * v1)} <> (Lin {v1}) /\ (Lin {v2}) ; :: thesis: contradiction
then consider y being Vector of V such that
B2: ( y in (Lin {v1}) /\ (Lin {v2}) & not y in Lin {(I1 * v1)} ) by A14, ZMODUL01:46;
y in Lin {v1} by B2, ZMODUL01:94;
then consider iy1 being Element of INT.Ring such that
B4: y = iy1 * v1 by ThLin1;
consider J1, Jy1 being Integer such that
B5: i1 gcd iy1 = (J1 * i1) + (Jy1 * iy1) by NAT_D:68;
reconsider j1 = J1, jy1 = Jy1 as Element of INT.Ring by INT_1:def 2;
reconsider iyi = i1 gcd iy1 as Element of INT.Ring by INT_1:def 2;
iyi = (j1 * I1) + (jy1 * iy1) by B5;
then B6: iyi * v1 = ((j1 * I1) * v1) + ((jy1 * iy1) * v1) by VECTSP_1:def 15
.= (j1 * (I1 * v1)) + ((jy1 * iy1) * v1) by VECTSP_1:def 16
.= (j1 * (I1 * v1)) + (jy1 * y) by B4, VECTSP_1:def 16 ;
B7: j1 * (I1 * v1) in (Lin {v1}) /\ (Lin {v2}) by A13, ZMODUL01:37;
jy1 * y in (Lin {v1}) /\ (Lin {v2}) by B2, ZMODUL01:37;
then B8: iyi * v1 in (Lin {v1}) /\ (Lin {v2}) by B6, B7, ZMODUL01:36;
iyi * v1 in Lin {v2} by B8, ZMODUL01:94;
then consider iiy2 being Element of INT.Ring such that
B10: iyi * v1 = iiy2 * v2 by ThLin1;
i1 gcd iy1 divides i1 by INT_2:def 2;
then consider I3 being Integer such that
B11: i1 = (i1 gcd iy1) * I3 by INT_1:def 3;
reconsider i3 = I3 as Element of INT.Ring by INT_1:def 2;
i1 = iyi * i3 by B11;
then B12: I1 * v1 = i3 * (iyi * v1) by VECTSP_1:def 16
.= (i3 * iiy2) * v2 by VECTSP_1:def 16, B10 ;

per cases ( i3 * iiy2 = i2 or i3 * iiy2 <> i2 ) ;

suppose i3 * iiy2 = i2 ; :: thesis: contradiction

then C3: i3 divides i2 by INT_1:def 3;
C2: i3 divides i1 by B11, INT_1:def 3;

per cases ( i1 gcd i2 = 1 or i1 gcd i2 <> 1 ) ;

suppose i1 gcd i2 = 1 ; :: thesis: contradiction

then ( i3 = 1 or i3 = - 1 ) by INT_2:13, C3, C2, INT_2:22;
then ( i1 divides iy1 or - i1 divides iy1 ) by INT_2:def 2, B11;
then consider iy3 being Integer such that
D2: iy1 = i1 * iy3 by INT_1:def 3, INT_2:10;
reconsider Iy3 = iy3 as Element of INT.Ring by INT_1:def 2;
iy1 = I1 * Iy3 by D2;
then y = Iy3 * (I1 * v1) by VECTSP_1:def 16, B4;
hence contradiction by B2, ZMODUL01:37, ThLin2; :: thesis: verum

end;

suppose i1 gcd i2 <> 1 ; :: thesis: contradiction

hence contradiction by A10, INT_2:def 3; :: thesis: verum

end;

end;

end;

suppose i3 * iiy2 <> i2 ; :: thesis: contradiction

then C2: i2 - (i3 * iiy2) <> 0 ;
0. V = (I2 * v2) - ((i3 * iiy2) * v2) by RLVECT_1:15, A12, B12
.= (I2 - (i3 * iiy2)) * v2 by ZMODUL01:9 ;
then v2 is torsion by C2;
hence contradiction by A1, defTorsionFree; :: thesis: verum

end;

end;

end;

i1 <> 0. INT.Ring by A10, A2, A4, ZMODUL01:1;
hence ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} ) by A16, A1, ZMODUL01:def 7; :: thesis: verum