let E be EuclidianRing; :: thesis: E is gcdDomain
set d = the DegreeFunction of E;
now :: thesis: for x, y being Element of E 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 ) )
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 :: thesis: ( ( x = 0. E & 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 ) ) ) or ( x <> 0. E & 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 ) ) ) )
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 ;
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) } ;
defpred S1[ 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 = the DegreeFunction of E . z );
((1. E) * x) + ((0. E) * y) = (1. E) * x by RLVECT_1:def 4
.= x ;
then A4: x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;
ex k being Element of NAT st k = the DegreeFunction of E . x ;
then A5: ex k being Nat st S1[k] by A3, A4;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A5);
then consider k being Nat such that
A6: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) ;
consider g being Element of E such that
A7: g in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } and
A8: g <> 0. E and
A9: ( k = the DegreeFunction of E . 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 = the DegreeFunction of E . z ) holds
k <= n ) ) by A6;
set G = { z where z is Element of E : ex r being Element of E st z = r * g } ;
A10: for z being object 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 object ; :: 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 and
A12: ex s, t being Element of E st z2 = (s * x) + (t * y) ;
consider u, v being Element of E such that
A13: z2 = (u * x) + (v * y) by A12;
reconsider z = z as Element of E by A11;
consider q, r being Element of E such that
A14: z = (q * g) + r and
A15: ( r = 0. E or the DegreeFunction of E . r < the DegreeFunction of E . g ) by A8, Def9;
r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }
proof
consider z1 being Element of E such that
A16: g = z1 and
A17: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;
consider s, t being Element of E such that
A18: z1 = (s * x) + (t * y) by A17;
z + (- (q * g)) = r + ((q * g) + (- (q * g))) by A14, RLVECT_1:def 3
.= r + (0. E) by RLVECT_1:def 10
.= r by RLVECT_1:def 4 ;
then r = z + (- ((q * (s * x)) + (q * (t * y)))) by A16, A18, VECTSP_1:def 7
.= z + ((- (q * (s * x))) + (- (q * (t * y)))) by RLVECT_1:31
.= (((u * x) + (v * y)) + (- (q * (s * x)))) + (- (q * (t * y))) by A11, A13, RLVECT_1:def 3
.= (((u * x) + (- (q * (s * x)))) + (v * y)) + (- (q * (t * y))) by RLVECT_1:def 3
.= ((u * x) + (- (q * (s * x)))) + ((v * y) + (- (q * (t * y)))) by RLVECT_1:def 3
.= ((u * x) + ((- q) * (s * x))) + ((v * y) + (- (q * (t * y)))) by GCD_1:48
.= ((u * x) + ((- q) * (s * x))) + ((v * y) + ((- q) * (t * y))) by GCD_1:48
.= ((u * x) + (((- q) * s) * x)) + ((v * y) + ((- q) * (t * y))) by GROUP_1:def 3
.= ((u * x) + (((- q) * s) * x)) + ((v * y) + (((- q) * t) * y)) by GROUP_1:def 3
.= ((u + ((- q) * s)) * x) + ((v * y) + (((- q) * t) * y)) by VECTSP_1:def 7
.= ((u + ((- q) * s)) * x) + ((v + ((- q) * t)) * y) by VECTSP_1:def 7 ;
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 A9, A15;
then z = q * g by A14, RLVECT_1:def 4;
hence z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: verum
end;
A19: 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 that
A20: z divides x and
A21: z divides y ; :: thesis: z divides g
consider u being Element of E such that
A22: x = z * u by A20, GCD_1:def 1;
consider zz being Element of E such that
A23: g = zz and
A24: ex s, t being Element of E st zz = (s * x) + (t * y) by A7;
consider s, t being Element of E such that
A25: zz = (s * x) + (t * y) by A24;
consider v being Element of E such that
A26: y = z * v by A21, GCD_1:def 1;
g = ((s * u) * z) + (t * (v * z)) by A22, A26, A23, A25, GROUP_1:def 3
.= ((s * u) * z) + ((t * v) * z) by GROUP_1:def 3
.= ((s * u) + (t * v)) * z by VECTSP_1:def 7 ;
hence z divides g by GCD_1:def 1; :: thesis: verum
end;
((0. E) * x) + ((1. E) * y) = (1. E) * y by RLVECT_1:4
.= y ;
then A27: y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;
for z being object 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 object ; :: 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
A28: z = z2 and
A29: ex s being Element of E st z2 = s * g ;
reconsider z = z as Element of E by A28;
consider u being Element of E such that
A30: z2 = u * g by A29;
consider z1 being Element of E such that
A31: g = z1 and
A32: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;
consider s, t being Element of E such that
A33: z1 = (s * x) + (t * y) by A32;
z = (u * (s * x)) + (u * (t * y)) by A28, A30, A31, A33, VECTSP_1:def 2
.= ((u * s) * x) + (u * (t * y)) by GROUP_1:def 3
.= ((u * s) * x) + ((u * t) * y) by GROUP_1:def 3 ;
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;
then A34: { 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;
( g divides x & g divides y )
proof
( ex zz being Element of E st
( x = zz & ex r being Element of E st zz = r * g ) & ex zzz being Element of E st
( y = zzz & ex r being Element of E st zzz = r * g ) ) by A4, A27, A34;
hence ( g divides x & g divides y ) 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 A19; :: 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 gcdDomain by GCD_1:def 11; :: thesis: verum