let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -monomorphic Field
for h being Monomorphism of F1,F2
for p, q being Element of the carrier of (Polynom-Ring F1) st p divides q holds
(PolyHom h) . p divides (PolyHom h) . q
let F2 be F1 -homomorphic F1 -monomorphic Field; :: thesis: for h being Monomorphism of F1,F2
for p, q being Element of the carrier of (Polynom-Ring F1) st p divides q holds
(PolyHom h) . p divides (PolyHom h) . q
let h be Monomorphism of F1,F2; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F1) st p divides q holds
(PolyHom h) . p divides (PolyHom h) . q
let p, q be Element of the carrier of (Polynom-Ring F1); :: thesis: ( p divides q implies (PolyHom h) . p divides (PolyHom h) . q )
assume AS: p divides q ; :: thesis: (PolyHom h) . p divides (PolyHom h) . q
reconsider pp = p, qq = q as Polynomial of F1 ;
consider rr being Polynomial of F1 such that
B: pp *' rr = qq by AS, RING_4:1;
reconsider r = rr as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
p * r = q by B, POLYNOM3:def 10;
then C: (PolyHom h) . q = ((PolyHom h) . p) * ((PolyHom h) . r) by FIELD_1:25;
reconsider pe = (PolyHom h) . p, qe = (PolyHom h) . q, re = (PolyHom h) . r as Polynomial of F2 ;
qe = pe *' re by C, POLYNOM3:def 10;
hence (PolyHom h) . p divides (PolyHom h) . q by RING_4:1; :: thesis: verum