let E be EuclidianRing; :: thesis: E is gcdDomain
consider d being DegreeFunction of E;
E is gcd-like

proof

now

let x, y be Element of E; :: thesis: ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) )

now

per cases ( x = 0. E or x <> 0. E ) ;

case A1: x = 0. E ; :: thesis: ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) )

y * (0. E) = 0. E by VECTSP_1:36;
then A2: y divides 0. E by GCD_1:def 1;
for zz being Element of E st zz divides x & zz divides y holds
zz divides y ;
hence ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) ) by A1, A2; :: thesis: verum

end;

case A3: x <> 0. E ; :: thesis: ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) )

set M = { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;
A4: ( x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } )

proof

A5: ((1. E) * x) + ((0. E) * y) = ((1. E) * x) + (0. E) by VECTSP_1:39
.= (1. E) * x by RLVECT_1:def 7
.= x by VECTSP_1:def 16 ;
((0. E) * x) + ((1. E) * y) = (0. E) + ((1. E) * y) by VECTSP_1:39
.= (1. E) * y by RLVECT_1:10
.= y by VECTSP_1:def 16 ;
hence ( x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ) by A5; :: thesis: verum

end;

defpred S₁[ Nat] means ex z being Element of E st
( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & $1 = d . z );
A6: ex k being Nat st S₁[k]

proof

ex k being Element of NAT st k = d . x ;
hence ex k being Nat st S₁[k] by A3, A4; :: thesis: verum

end;

ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A6);
then consider k being Nat such that
A7: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) ;
consider g being Element of E such that
A8: ( g in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & g <> 0. E & k = d . g & ( for n being Nat st ex z being Element of E st
( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & n = d . z ) holds
k <= n ) ) by A7;
set G = { z where z is Element of E : ex r being Element of E st z = r * g } ;
A9: { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } = { z where z is Element of E : ex r being Element of E st z = r * g }

proof

A10: for z being set st z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } holds
z in { z where z is Element of E : ex r being Element of E st z = r * g }

proof

let z be set ; :: thesis: ( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } implies z in { z where z is Element of E : ex r being Element of E st z = r * g } )
assume z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: z in { z where z is Element of E : ex r being Element of E st z = r * g }
then consider z2 being Element of E such that
A11: ( z = z2 & ex s, t being Element of E st z2 = (s * x) + (t * y) ) ;
reconsider z = z as Element of E by A11;
consider u, v being Element of E such that
A12: z2 = (u * x) + (v * y) by A11;
consider q, r being Element of E such that
A13: ( z = (q * g) + r & ( r = 0. E or d . r < d . g ) ) by A8, Def10;
r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

proof

A14: z + (- (q * g)) = r + ((q * g) + (- (q * g))) by A13, RLVECT_1:def 6
.= r + (0. E) by RLVECT_1:def 11
.= r by RLVECT_1:def 7 ;
consider z1 being Element of E such that
A15: ( g = z1 & ex s, t being Element of E st z1 = (s * x) + (t * y) ) by A8;
consider s, t being Element of E such that
A16: z1 = (s * x) + (t * y) by A15;
r = z + (- ((q * (s * x)) + (q * (t * y)))) by A14, A15, A16, VECTSP_1:def 18
.= z + ((- (q * (s * x))) + (- (q * (t * y)))) by RLVECT_1:45
.= (((u * x) + (v * y)) + (- (q * (s * x)))) + (- (q * (t * y))) by A11, A12, RLVECT_1:def 6
.= (((u * x) + (- (q * (s * x)))) + (v * y)) + (- (q * (t * y))) by RLVECT_1:def 6
.= ((u * x) + (- (q * (s * x)))) + ((v * y) + (- (q * (t * y)))) by RLVECT_1:def 6
.= ((u * x) + ((- q) * (s * x))) + ((v * y) + (- (q * (t * y)))) by GCD_1:51
.= ((u * x) + ((- q) * (s * x))) + ((v * y) + ((- q) * (t * y))) by GCD_1:51
.= ((u * x) + (((- q) * s) * x)) + ((v * y) + ((- q) * (t * y))) by GROUP_1:def 4
.= ((u * x) + (((- q) * s) * x)) + ((v * y) + (((- q) * t) * y)) by GROUP_1:def 4
.= ((u + ((- q) * s)) * x) + ((v * y) + (((- q) * t) * y)) by VECTSP_1:def 18
.= ((u + ((- q) * s)) * x) + ((v + ((- q) * t)) * y) by VECTSP_1:def 18 ;
hence r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

end;

then r = 0. E by A8, A13;
then z = q * g by A13, RLVECT_1:def 7;
hence z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: verum

end;

for z being set st z in { z where z is Element of E : ex r being Element of E st z = r * g } holds
z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

proof

let z be set ; :: thesis: ( z in { z where z is Element of E : ex r being Element of E st z = r * g } implies z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } )
assume z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }
then consider z2 being Element of E such that
A17: ( z = z2 & ex s being Element of E st z2 = s * g ) ;
reconsider z = z as Element of E by A17;
consider u being Element of E such that
A18: z2 = u * g by A17;
consider z1 being Element of E such that
A19: ( g = z1 & ex s, t being Element of E st z1 = (s * x) + (t * y) ) by A8;
consider s, t being Element of E such that
A20: z1 = (s * x) + (t * y) by A19;
z = (u * (s * x)) + (u * (t * y)) by A17, A18, A19, A20, VECTSP_1:def 11
.= ((u * s) * x) + (u * (t * y)) by GROUP_1:def 4
.= ((u * s) * x) + ((u * t) * y) by GROUP_1:def 4 ;
hence z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

end;

hence { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } = { z where z is Element of E : ex r being Element of E st z = r * g } by A10, TARSKI:2; :: thesis: verum

end;

A21: ( g divides x & g divides y )

proof

consider zz being Element of E such that
A22: ( x = zz & ex r being Element of E st zz = r * g ) by A4, A9;
consider zzz being Element of E such that
A23: ( y = zzz & ex r being Element of E st zzz = r * g ) by A4, A9;
thus ( g divides x & g divides y ) by A22, A23, GCD_1:def 1; :: thesis: verum

end;

for z being Element of E st z divides x & z divides y holds
z divides g

proof

let z be Element of E; :: thesis: ( z divides x & z divides y implies z divides g )
assume A24: ( z divides x & z divides y ) ; :: thesis: z divides g
then consider u being Element of E such that
A25: x = z * u by GCD_1:def 1;
consider v being Element of E such that
A26: y = z * v by A24, GCD_1:def 1;
consider zz being Element of E such that
A27: ( g = zz & ex s, t being Element of E st zz = (s * x) + (t * y) ) by A8;
consider s, t being Element of E such that
A28: zz = (s * x) + (t * y) by A27;
g = ((s * u) * z) + (t * (v * z)) by A25, A26, A27, A28, GROUP_1:def 4
.= ((s * u) * z) + ((t * v) * z) by GROUP_1:def 4
.= ((s * u) + (t * v)) * z by VECTSP_1:def 18 ;
hence z divides g by GCD_1:def 1; :: thesis: verum

end;

hence ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) ) by A21; :: thesis: verum

end;

end;

end;

hence ex z being Element of E st
( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds
zz divides z ) ) ; :: thesis: verum

end;

hence E is gcd-like by GCD_1:def 11; :: thesis: verum

end;

hence E is gcdDomain ; :: thesis: verum