let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st gcd (a,b,Amp) = 1. R holds
gcd (a,(b * c),Amp) = gcd (a,c,Amp)
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st gcd (a,b,Amp) = 1. R holds
gcd (a,(b * c),Amp) = gcd (a,c,Amp)
let A, B, C be Element of R; :: thesis: ( gcd (A,B,Amp) = 1. R implies gcd (A,(B * C),Amp) = gcd (A,C,Amp) )
assume gcd (A,B,Amp) = 1. R ; :: thesis: gcd (A,(B * C),Amp) = gcd (A,C,Amp)
then A1: C * (gcd (A,B,Amp)) = C ;
gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) by Th36;
then gcd (A,C,Amp) is_associated_to gcd (A,(gcd ((A * C),(B * C),Amp)),Amp) by A1, Th34;
then A2: gcd (A,C,Amp) is_associated_to gcd ((gcd (A,(A * C),Amp)),(B * C),Amp) by Th35;
A3: A * (gcd ((1. R),C,Amp)) = A * (1. R) by Th32
.= A ;
gcd ((A * (1. R)),(A * C),Amp) is_associated_to A * (gcd ((1. R),C,Amp)) by Th36;
then gcd (A,(A * C),Amp) is_associated_to A by A3;
then A4: gcd ((gcd (A,(A * C),Amp)),(B * C),Amp) is_associated_to gcd (A,(B * C),Amp) by Th34;
( gcd (A,(B * C),Amp) is Element of Amp & gcd (A,C,Amp) is Element of Amp ) by Def12;
hence gcd (A,(B * C),Amp) = gcd (A,C,Amp) by A2, A4, Th4, Th22; :: thesis: verum