let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st b is_associated_to c holds
( gcd a,b,Amp is_associated_to gcd a,c,Amp & gcd b,a,Amp is_associated_to gcd c,a,Amp )
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st b is_associated_to c holds
( gcd a,b,Amp is_associated_to gcd a,c,Amp & gcd b,a,Amp is_associated_to gcd c,a,Amp )
let A, B, C be Element of R; :: thesis: ( B is_associated_to C implies ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp ) )
A1: gcd A,B,Amp divides B by Def12;
A2: gcd A,B,Amp divides A by Def12;
A3: gcd A,C,Amp divides A by Def12;
A4: gcd A,C,Amp divides C by Def12;
A5: gcd A,B,Amp = gcd B,A,Amp by Th30;
assume A6: B is_associated_to C ; :: thesis: ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp )
then C divides B by Def3;
then gcd A,C,Amp divides B by A4, Th2;
then A7: gcd A,C,Amp divides gcd A,B,Amp by A3, Def12;
B divides C by A6, Def3;
then gcd A,B,Amp divides C by A1, Th2;
then gcd A,B,Amp divides gcd A,C,Amp by A2, Def12;
then gcd A,B,Amp is_associated_to gcd A,C,Amp by A7, Def3;
hence ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp ) by A5, Th30; :: thesis: verum