let L be domRing; :: thesis: for p being Polynomial of L
for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let p be Polynomial of L; :: thesis: for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let x be Element of L; :: thesis: ( eval (p,x) = 0. L iff rpoly (1,x) divides p )
A1: now :: thesis: ( rpoly (1,x) divides p implies eval (p,x) = 0. L )
assume rpoly (1,x) divides p ; :: thesis: eval (p,x) = 0. L
then consider u being Polynomial of L such that
A2: (rpoly (1,x)) *' u = p by RING_4:1;
A3: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
thus eval (p,x) = (eval ((rpoly (1,x)),x)) * (eval (u,x)) by A2, POLYNOM4:24
.= 0. L by A3 ; :: thesis: verum
end;
now :: thesis: ( eval (p,x) = 0. L implies rpoly (1,x) divides p )
assume eval (p,x) = 0. L ; :: thesis: rpoly (1,x) divides p
then consider s being Polynomial of L such that
A4: p = (rpoly (1,x)) *' s by HURWITZ:33, POLYNOM5:def 7;
thus rpoly (1,x) divides p by RING_4:1, A4; :: thesis: verum
end;
hence ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) by A1; :: thesis: verum