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 <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {x} )
by A1, LmSumMod1;
A3:
x in Lin {x}
by ZMODUL02:65, ZFMISC_1:31;
then
x in Lin {v1}
by A2, ZMODUL01:94;
then consider i1 being Element of INT.Ring such that
A4:
x = i1 * v1
by ThLin1;
x in Lin {v2}
by A2, A3, ZMODUL01:94;
then consider i2 being Element of INT.Ring such that
A5:
x = i2 * v2
by ThLin1;
|.i1.| gcd |.i2.| = 1
proof
set n1 =
|.i1.|;
set n2 =
|.i2.|;
assume ASB:
|.i1.| gcd |.i2.| <> 1
;
contradiction
per cases
( |.i1.| gcd |.i2.| = 0 or |.i1.| gcd |.i2.| <> 0 )
;
suppose
|.i1.| gcd |.i2.| <> 0
;
contradictionthen
|.i1.| gcd |.i2.| > 1
by ASB, NAT_1:25;
then C1:
i1 gcd i2 > 1
by INT_2:34;
i1 gcd i2 divides i1
by INT_2:def 2;
then consider k1 being
Integer such that C2:
i1 = (i1 gcd i2) * k1
by INT_1:def 3;
i1 gcd i2 divides i2
by INT_2:def 2;
then consider k2 being
Integer such that C3:
i2 = (i1 gcd i2) * k2
by INT_1:def 3;
reconsider K1 =
k1,
K2 =
k2 as
Element of
INT.Ring by INT_1:def 2;
reconsider igi =
i1 gcd i2 as
Element of
INT.Ring by INT_1:def 2;
c2:
(
i1 = igi * K1 &
i2 = igi * K2 )
by C2, C3;
then C4:
igi * (K1 * v1) =
(igi * K2) * v2
by VECTSP_1:def 16, A4, A5
.=
igi * (K2 * v2)
by VECTSP_1:def 16
;
C5:
K1 * v1 = K2 * v2
by ZMODUL01:10, C1, C4;
C6:
K1 * v1 in Lin {v1}
by ZMODUL01:37, ThLin2;
K2 * v2 in Lin {v2}
by ZMODUL01:37, ThLin2;
then consider ikv being
Element of
INT.Ring such that C8:
K1 * v1 = ikv * x
by ThLin1, A2, C5, C6, ZMODUL01:94;
x =
igi * (K1 * v1)
by VECTSP_1:def 16, A4, c2
.=
(igi * ikv) * x
by VECTSP_1:def 16, C8
;
then C9:
0. V =
((igi * ikv) * x) - x
by RLVECT_1:15
.=
((igi * ikv) * x) - ((1. INT.Ring) * x)
by VECTSP_1:def 17
.=
((igi * ikv) - (1. INT.Ring)) * x
by ZMODUL01:9
;
(igi * ikv) - (1. INT.Ring) <> 0. INT.Ring
by C1, INT_1:9;
hence
contradiction
by A2, C9, ZMODUL01:def 7;
verum end; end;
end;
then
i1 gcd i2 = 1
by INT_2:34;
then consider j1, j2 being Element of INT.Ring such that
A7:
(i1 * j1) + (i2 * j2) = 1
by LmGCD, INT_2:def 3;
reconsider J1 = j1, J2 = j2 as Element of INT.Ring ;
a7:
(i1 * J1) + (i2 * J2) = 1. INT.Ring
by A7;
reconsider u = (J1 * v2) + (J2 * v1) as Vector of V ;
A8:
u in Lin {u}
by ZMODUL02:65, ZFMISC_1:31;
B1: i1 * u =
(i1 * (J1 * v2)) + (i1 * (J2 * v1))
by VECTSP_1:def 14
.=
(i1 * (J1 * v2)) + ((i1 * J2) * v1)
by VECTSP_1:def 16
.=
(i1 * (J1 * v2)) + (J2 * (i1 * v1))
by VECTSP_1:def 16
.=
((i1 * J1) * v2) + (J2 * (i2 * v2))
by VECTSP_1:def 16, A4, A5
.=
((i1 * J1) * v2) + ((i2 * J2) * v2)
by VECTSP_1:def 16
.=
((i1 * J1) + (i2 * J2)) * v2
by VECTSP_1:def 15
.=
v2
by VECTSP_1:def 17, a7
;
B3: i2 * u =
(i2 * (J1 * v2)) + (i2 * (J2 * v1))
by VECTSP_1:def 14
.=
((i2 * J1) * v2) + (i2 * (J2 * v1))
by VECTSP_1:def 16
.=
(J1 * (i2 * v2)) + (i2 * (J2 * v1))
by VECTSP_1:def 16
.=
(J1 * (i2 * v2)) + ((i2 * J2) * v1)
by VECTSP_1:def 16
.=
((i1 * J1) * v1) + ((i2 * J2) * v1)
by VECTSP_1:def 16, A4, A5
.=
((i1 * J1) + (i2 * J2)) * v1
by VECTSP_1:def 15
.=
v1
by VECTSP_1:def 17, a7
;
(Lin {v1}) + (Lin {v2}) = Lin {u}
hence
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) + (Lin {v2}) = Lin {u} )
by A1, B3, ZMODUL01:1; verum