let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p, q being Element of the carrier of (Polynom-Ring F1) holds
( p divides q iff (PolyHom h) . p divides (PolyHom h) . q )
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for p, q being Element of the carrier of (Polynom-Ring F1) holds
( p divides q iff (PolyHom h) . p divides (PolyHom h) . q )
let h be Isomorphism of F1,F2; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F1) holds
( p divides q iff (PolyHom h) . p divides (PolyHom h) . q )
let p, q be Element of the carrier of (Polynom-Ring F1); :: thesis: ( p divides q iff (PolyHom h) . p divides (PolyHom h) . q )
A: now :: 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
end;
reconsider f = (PolyHom h) " as Isomorphism of (Polynom-Ring F2),(Polynom-Ring F1) by RING_3:73;
now :: thesis: ( (PolyHom h) . p divides (PolyHom h) . q implies p divides q )
assume AS: (PolyHom h) . p divides (PolyHom h) . q ; :: thesis: p divides q
reconsider pp = (PolyHom h) . p, qq = (PolyHom h) . q as Polynomial of F2 ;
consider rr being Polynomial of F2 such that
B: pp *' rr = qq by AS, RING_4:1;
reconsider r = rr as Element of the carrier of (Polynom-Ring F2) by POLYNOM3:def 10;
((PolyHom h) . p) * r = (PolyHom h) . q by B, POLYNOM3:def 10;
then C: (f . ((PolyHom h) . p)) * (f . r) = f . ((PolyHom h) . q) by GROUP_6:def 6;
D: ( f . ((PolyHom h) . p) = p & f . ((PolyHom h) . q) = q ) by FUNCT_2:26;
reconsider pe = p, qe = q, re = f . r as Polynomial of F1 ;
qe = pe *' re by C, D, POLYNOM3:def 10;
hence p divides q by RING_4:1; :: thesis: verum
end;
hence ( p divides q iff (PolyHom h) . p divides (PolyHom h) . q ) by A; :: thesis: verum