let L be Field; :: thesis: for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
let p be Polynomial of L; :: thesis: ( len p <> 0 implies for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p ) )
assume A1: len p <> 0 ; :: thesis: for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
then len p >= 0 + 1 by NAT_1:13;
then len p = ((len p) -' 1) + 1 by XREAL_1:235;
then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
then A2: (p . ((len p) -' 1)) " <> 0. L by VECTSP_1:25;
let x be Element of L; :: thesis: ( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
thus ( x is_a_root_of p implies x is_a_root_of NormPolynomial p ) :: thesis: ( x is_a_root_of NormPolynomial p implies x is_a_root_of p )
proof
assume x is_a_root_of p ; :: thesis: x is_a_root_of NormPolynomial p
then eval (p,x) = 0. L ;
then eval ((NormPolynomial p),x) = (0. L) / (p . ((len p) -' 1)) by A1, Th58
.= (0. L) * ((p . ((len p) -' 1)) ")
.= 0. L ;
hence x is_a_root_of NormPolynomial p ; :: thesis: verum
end;
assume x is_a_root_of NormPolynomial p ; :: thesis: x is_a_root_of p
then 0. L = eval ((NormPolynomial p),x)
.= (eval (p,x)) / (p . ((len p) -' 1)) by A1, Th58
.= (eval (p,x)) * ((p . ((len p) -' 1)) ") ;
then eval (p,x) = 0. L by A2, VECTSP_1:12;
hence x is_a_root_of p ; :: thesis: verum