let F be Field; :: thesis: for p, q being Polynomial of F
for r being monic Polynomial of F holds (r *' p) gcd (r *' q) = r *' (p gcd q)
let p, q be Polynomial of F; :: thesis: for r being monic Polynomial of F holds (r *' p) gcd (r *' q) = r *' (p gcd q)
let r be monic Polynomial of F; :: thesis: (r *' p) gcd (r *' q) = r *' (p gcd q)
consider a, b being Element of (Polynom-Ring F) such that
H: ( a = p & b = q & p gcd q = a gcd b ) by RING_4:def 12;

per cases ( ( p = 0_. F & q = 0_. F ) or p <> 0_. F or q <> 0_. F ) ;

suppose A: ( p = 0_. F & q = 0_. F ) ; :: thesis: (r *' p) gcd (r *' q) = r *' (p gcd q)

then a gcd b = 0_. F by H, RING_4:def 11;
hence (r *' p) gcd (r *' q) = r *' (p gcd q) by H, A; :: thesis: verum

end;

suppose AS: ( p <> 0_. F or q <> 0_. F ) ; :: thesis: (r *' p) gcd (r *' q) = r *' (p gcd q)

then K: a gcd b is monic by H, RING_4:def 11;
consider p1 being Polynomial of F such that
E1: p = (p gcd q) *' p1 by RING_4:1, RING_4:52;
(r *' (p gcd q)) *' p1 = r *' p by E1, POLYNOM3:33;
then A: r *' (p gcd q) divides r *' p by RING_4:1;
consider q1 being Polynomial of F such that
E2: q = (p gcd q) *' q1 by RING_4:1, RING_4:52;
(r *' (p gcd q)) *' q1 = r *' q by E2, POLYNOM3:33;
then r *' (p gcd q) divides r *' q by RING_4:1;
then consider u being Polynomial of F such that
C: (r *' p) gcd (r *' q) = (r *' (p gcd q)) *' u by A, RING_4:52, RING_4:1;
C1: u is monic

proof

consider a, b being Element of (Polynom-Ring F) such that
C0: ( a = r *' p & b = r *' q & (r *' p) gcd (r *' q) = a gcd b ) by RING_4:def 12;
( r *' q <> 0_. F or r *' p <> 0_. F )

proof

assume r *' q = 0_. F ; :: thesis: r *' p <> 0_. F
then q is zero ;
then not p is zero by AS, UPROOTS:def 5;
hence r *' p <> 0_. F ; :: thesis: verum

end;

then C2: (r *' p) gcd (r *' q) is monic by C0, RING_4:def 11;
p gcd q is monic by AS, H, RING_4:def 11;
hence u is monic by C, C2, ZZ3y; :: thesis: verum

end;

( (p gcd q) *' u divides p & (p gcd q) *' u divides q )

proof

consider v being Polynomial of F such that
D1: ((r *' (p gcd q)) *' u) *' v = r *' p by C, RING_4:52, RING_4:1;
(r *' (p gcd q)) *' u divides r *' p by D1, RING_4:1;
then r *' ((p gcd q) *' u) divides r *' p by POLYNOM3:33;
hence (p gcd q) *' u divides p by ZZ3z; :: thesis: (p gcd q) *' u divides q
consider w being Polynomial of F such that
D1: ((r *' (p gcd q)) *' u) *' w = r *' q by C, RING_4:52, RING_4:1;
(r *' (p gcd q)) *' u divides r *' q by D1, RING_4:1;
then r *' ((p gcd q) *' u) divides r *' q by POLYNOM3:33;
hence (p gcd q) *' u divides q by ZZ3z; :: thesis: verum

end;

then E: (p gcd q) *' u divides p gcd q by RING_4:52;
(p gcd q) *' (1_. F) = p gcd q ;
then u = 1_. F by C1, ZZ3x, K, H, E, ZZ3z;
hence (r *' p) gcd (r *' q) = r *' (p gcd q) by C; :: thesis: verum

end;

end;