let V be torsion-free Z_Module; 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; ( 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 )
; 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})
A16:
Lin {(I1 * v1)} = (Lin {v1}) /\ (Lin {v2})
proof
assume
Lin {(I1 * v1)} <> (Lin {v1}) /\ (Lin {v2})
;
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
;
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; verum