let R be non degenerated Ring; :: thesis: for a being Element of R holds Roots (rpoly (1,a)) = {a}

let a be Element of R; :: thesis: Roots (rpoly (1,a)) = {a}

set p = rpoly (1,a);

let a be Element of R; :: thesis: Roots (rpoly (1,a)) = {a}

set p = rpoly (1,a);

A: now :: thesis: for u being object st u in {a} holds

u in Roots (rpoly (1,a))

u in Roots (rpoly (1,a))

let u be object ; :: thesis: ( u in {a} implies u in Roots (rpoly (1,a)) )

assume u in {a} ; :: thesis: u in Roots (rpoly (1,a))

then A: u = a by TARSKI:def 1;

eval ((rpoly (1,a)),a) = a - a by HURWITZ:29

.= 0. R by RLVECT_1:15 ;

then a is_a_root_of rpoly (1,a) by POLYNOM5:def 7;

hence u in Roots (rpoly (1,a)) by A, POLYNOM5:def 10; :: thesis: verum

end;assume u in {a} ; :: thesis: u in Roots (rpoly (1,a))

then A: u = a by TARSKI:def 1;

eval ((rpoly (1,a)),a) = a - a by HURWITZ:29

.= 0. R by RLVECT_1:15 ;

then a is_a_root_of rpoly (1,a) by POLYNOM5:def 7;

hence u in Roots (rpoly (1,a)) by A, POLYNOM5:def 10; :: thesis: verum

now :: thesis: for u being object st u in Roots (rpoly (1,a)) holds

u in {a}

hence
Roots (rpoly (1,a)) = {a}
by A, TARSKI:2; :: thesis: verumu in {a}

let u be object ; :: thesis: ( u in Roots (rpoly (1,a)) implies u in {a} )

assume B: u in Roots (rpoly (1,a)) ; :: thesis: u in {a}

then reconsider x = u as Element of R ;

x is_a_root_of rpoly (1,a) by B, POLYNOM5:def 10;

then 0. R = eval ((rpoly (1,a)),x) by POLYNOM5:def 7

.= x - a by HURWITZ:29 ;

then a = x by RLVECT_1:21;

hence u in {a} by TARSKI:def 1; :: thesis: verum

end;assume B: u in Roots (rpoly (1,a)) ; :: thesis: u in {a}

then reconsider x = u as Element of R ;

x is_a_root_of rpoly (1,a) by B, POLYNOM5:def 10;

then 0. R = eval ((rpoly (1,a)),x) by POLYNOM5:def 7

.= x - a by HURWITZ:29 ;

then a = x by RLVECT_1:21;

hence u in {a} by TARSKI:def 1; :: thesis: verum