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 <> 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 ; :: thesis: contradiction

per cases ( |.i1.| gcd |.i2.| = 0 or |.i1.| gcd |.i2.| <> 0 ) ;

suppose |.i1.| gcd |.i2.| = 0 ; :: thesis: contradiction

then ( |.i1.| = 0 & |.i2.| = 0 ) by INT_2:5;
hence contradiction by ABSVALUE:2, A2, A4, ZMODUL01:1; :: thesis: verum

end;

suppose |.i1.| gcd |.i2.| <> 0 ; :: thesis: contradiction

then |.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)
.= ((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; :: thesis: 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 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 a7 ;
(Lin {v1}) + (Lin {v2}) = Lin {u}

proof

B5: for vx being Vector of V st vx in Lin {v1} holds
vx in Lin {u}

proof

let vx be Vector of V; :: thesis: ( vx in Lin {v1} implies vx in Lin {u} )
assume C1: vx in Lin {v1} ; :: thesis: vx in Lin {u}
consider ivx1 being Element of INT.Ring such that
C2: vx = ivx1 * v1 by C1, ThLin1;
vx = (ivx1 * i2) * u by VECTSP_1:def 16, B3, C2;
hence vx in Lin {u} by A8, ZMODUL01:37; :: thesis: verum

end;

B6: for vx being Vector of V st vx in Lin {v2} holds
vx in Lin {u}

proof

let vx be Vector of V; :: thesis: ( vx in Lin {v2} implies vx in Lin {u} )
assume C1: vx in Lin {v2} ; :: thesis: vx in Lin {u}
consider ivx2 being Element of INT.Ring such that
C2: vx = ivx2 * v2 by C1, ThLin1;
vx = (ivx2 * i1) * u by VECTSP_1:def 16, B1, C2;
hence vx in Lin {u} by A8, ZMODUL01:37; :: thesis: verum

end;

for vx being Vector of V holds
( vx in (Lin {v1}) + (Lin {v2}) iff vx in Lin {u} )

proof

let vx be Vector of V; :: thesis: ( vx in (Lin {v1}) + (Lin {v2}) iff vx in Lin {u} )

hereby :: thesis: ( vx in Lin {u} implies vx in (Lin {v1}) + (Lin {v2}) )

assume vx in (Lin {v1}) + (Lin {v2}) ; :: thesis: vx in Lin {u}
then consider vx1, vx2 being Vector of V such that
C2: ( vx1 in Lin {v1} & vx2 in Lin {v2} & vx = vx1 + vx2 ) by ZMODUL01:92;
C3: vx1 in Lin {u} by B5, C2;
vx2 in Lin {u} by B6, C2;
hence vx in Lin {u} by C2, C3, ZMODUL01:36; :: thesis: verum

end;

assume vx in Lin {u} ; :: thesis: vx in (Lin {v1}) + (Lin {v2})
then consider ivx being Element of INT.Ring such that
C2: vx = ivx * u by ThLin1;
C3: vx = (ivx * (J1 * v2)) + (ivx * (J2 * v1)) by VECTSP_1:def 14, C2
.= ((ivx * J1) * v2) + (ivx * (J2 * v1)) by VECTSP_1:def 16
.= ((ivx * J1) * v2) + ((ivx * J2) * v1) by VECTSP_1:def 16 ;
v1 in Lin {v1} by ZMODUL02:65, ZFMISC_1:31;
then C4: (ivx * J2) * v1 in Lin {v1} by ZMODUL01:37;
v2 in Lin {v2} by ZMODUL02:65, ZFMISC_1:31;
then (ivx * J1) * v2 in Lin {v2} by ZMODUL01:37;
hence vx in (Lin {v1}) + (Lin {v2}) by C3, C4, ZMODUL01:92; :: thesis: verum

end;

hence (Lin {v1}) + (Lin {v2}) = Lin {u} by ZMODUL01:46; :: thesis: verum

end;

hence ex u being Vector of V st
( u <> 0. V & (Lin {v1}) + (Lin {v2}) = Lin {u} ) by A1, B3, ZMODUL01:1; :: thesis: verum