let R be domRing; :: thesis: for a, b being Element of R holds

( rpoly (1,a) divides rpoly (1,b) iff a = b )

let a, b be Element of R; :: thesis: ( rpoly (1,a) divides rpoly (1,b) iff a = b )

( rpoly (1,a) divides rpoly (1,b) iff a = b )

let a, b be Element of R; :: thesis: ( rpoly (1,a) divides rpoly (1,b) iff a = b )

X: now :: thesis: ( rpoly (1,a) divides rpoly (1,b) implies a = b )

assume
rpoly (1,a) divides rpoly (1,b)
; :: thesis: a = b

then consider p being Polynomial of R such that

A: (rpoly (1,a)) *' p = rpoly (1,b) by RING_4:1;

B: {b} = Roots (rpoly (1,b)) by ro4

.= (Roots (rpoly (1,a))) \/ (Roots p) by A, UPROOTS:23 ;

a in {a} by TARSKI:def 1;

then a in Roots (rpoly (1,a)) by ro4;

then a in {b} by B, XBOOLE_0:def 3;

hence a = b by TARSKI:def 1; :: thesis: verum

end;then consider p being Polynomial of R such that

A: (rpoly (1,a)) *' p = rpoly (1,b) by RING_4:1;

B: {b} = Roots (rpoly (1,b)) by ro4

.= (Roots (rpoly (1,a))) \/ (Roots p) by A, UPROOTS:23 ;

a in {a} by TARSKI:def 1;

then a in Roots (rpoly (1,a)) by ro4;

then a in {b} by B, XBOOLE_0:def 3;

hence a = b by TARSKI:def 1; :: thesis: verum

now :: thesis: ( a = b implies rpoly (1,a) divides rpoly (1,b) )

hence
( rpoly (1,a) divides rpoly (1,b) iff a = b )
by X; :: thesis: verumassume
a = b
; :: thesis: rpoly (1,a) divides rpoly (1,b)

then (rpoly (1,a)) *' (1_. R) = rpoly (1,b) ;

hence rpoly (1,a) divides rpoly (1,b) by RING_4:1; :: thesis: verum

end;then (rpoly (1,a)) *' (1_. R) = rpoly (1,b) ;

hence rpoly (1,a) divides rpoly (1,b) by RING_4:1; :: thesis: verum