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 )

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;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

now :: thesis: ( eval (p,x) = 0. L implies rpoly (1,x) divides p )

hence
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
by A1; :: thesis: verumassume
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;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