let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd ((a + (b * c)),c,Amp) = gcd (a,c,Amp)
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd ((a + (b * c)),c,Amp) = gcd (a,c,Amp)
let A, B, C be Element of R; :: thesis: gcd ((A + (B * C)),C,Amp) = gcd (A,C,Amp)
set D = gcd (A,C,Amp);
gcd (A,C,Amp) divides A by Def12;
then consider E being Element of R such that
A1: (gcd (A,C,Amp)) * E = A ;
A2: gcd (A,C,Amp) divides C by Def12;
then consider F being Element of R such that
A3: (gcd (A,C,Amp)) * F = C ;
A4: for z being Element of R st z divides A + (B * C) & z divides C holds
z divides gcd (A,C,Amp)
proof
let Z be Element of R; :: thesis: ( Z divides A + (B * C) & Z divides C implies Z divides gcd (A,C,Amp) )
assume that
A5: Z divides A + (B * C) and
A6: Z divides C ; :: thesis: Z divides gcd (A,C,Amp)
consider X being Element of R such that
A7: Z * X = C by A6;
consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A5;
Z * (Y + (- (B * X))) = (Z * Y) + (Z * (- (B * X))) by VECTSP_1:def 2
.= (Z * Y) + (- (Z * (X * B))) by VECTSP_1:8
.= (A + (B * C)) + (- (C * B)) by A7, A8, GROUP_1:def 3
.= A + ((B * C) + (- (C * B))) by RLVECT_1:def 3
.= A + (0. R) by RLVECT_1:def 10
.= A by RLVECT_1:4 ;
then Z divides A ;
hence Z divides gcd (A,C,Amp) by A6, Def12; :: thesis: verum
end;
(gcd (A,C,Amp)) * (E + (F * B)) = ((gcd (A,C,Amp)) * E) + ((gcd (A,C,Amp)) * (F * B)) by VECTSP_1:def 2
.= A + (B * C) by A1, A3, GROUP_1:def 3 ;
then A9: gcd (A,C,Amp) divides A + (B * C) ;
gcd (A,C,Amp) is Element of Amp by Def12;
hence gcd ((A + (B * C)),C,Amp) = gcd (A,C,Amp) by A2, A9, A4, Def12; :: thesis: verum