let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd ((a * c),(b * c),Amp) is_associated_to c * (gcd (a,b,Amp))
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd ((a * c),(b * c),Amp) is_associated_to c * (gcd (a,b,Amp))
let A, B, C be Element of R; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
now :: thesis: ( ( C <> 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) or ( C = 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) )
per cases ( C <> 0. R or C = 0. R ) ;
case A1: C <> 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
set D = gcd (A,B,Amp);
now :: thesis: ( ( gcd (A,B,Amp) <> 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) or ( gcd (A,B,Amp) = 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) )
per cases ( gcd (A,B,Amp) <> 0. R or gcd (A,B,Amp) = 0. R ) ;
case A2: gcd (A,B,Amp) <> 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
set E = gcd ((A * C),(B * C),Amp);
A3: gcd ((A * C),(B * C),Amp) divides B * C by Def12;
gcd (A,B,Amp) divides B by Def12;
then A4: C * (gcd (A,B,Amp)) divides B * C by Th5;
gcd (A,B,Amp) divides A by Def12;
then C * (gcd (A,B,Amp)) divides A * C by Th5;
then C * (gcd (A,B,Amp)) divides gcd ((A * C),(B * C),Amp) by A4, Def12;
then consider F being Element of R such that
A5: gcd ((A * C),(B * C),Amp) = (C * (gcd (A,B,Amp))) * F ;
A6: gcd ((A * C),(B * C),Amp) divides A * C by Def12;
( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B )
proof
consider G being Element of R such that
A7: ((C * (gcd (A,B,Amp))) * F) * G = A * C by A5, A6;
(C * ((gcd (A,B,Amp)) * F)) * G = C * A by A7, GROUP_1:def 3;
then A8: C * ((gcd (A,B,Amp)) * F) divides C * A ;
consider G being Element of R such that
A9: ((C * (gcd (A,B,Amp))) * F) * G = B * C by A5, A3;
(C * ((gcd (A,B,Amp)) * F)) * G = C * B by A9, GROUP_1:def 3;
then C * ((gcd (A,B,Amp)) * F) divides C * B ;
hence ( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B ) by A1, A8, Th15; :: thesis: verum
end;
then A10: (gcd (A,B,Amp)) * F divides gcd (A,B,Amp) by Def12;
gcd (A,B,Amp) = (gcd (A,B,Amp)) * (1. R) ;
then F divides 1. R by A2, A10, Th15;
then F is unital ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) by A5, Th18; :: thesis: verum
end;
case A11: gcd (A,B,Amp) = 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
then A12: C * (gcd (A,B,Amp)) = 0. R ;
( A = 0. R & B = 0. R ) by A11, Th33;
then gcd ((A * C),(B * C),Amp) = gcd ((0. R),((0. R) * C),Amp)
.= gcd ((0. R),(0. R),Amp)
.= C * (gcd (A,B,Amp)) by A12, Th31 ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum
end;
end;
end;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum
end;
case A13: C = 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
then ( A * C = 0. R & B * C = 0. R ) ;
then gcd ((A * C),(B * C),Amp) = 0. R by Th31
.= C * (gcd (A,B,Amp)) by A13 ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum
end;
end;
end;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum