let F be Field; :: thesis: for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )
let E be FieldExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of E holds
( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )
let a be Element of E; :: thesis: ( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring E) ;
reconsider qa = q as Polynomial of E ;
reconsider ra = rpoly (1,a) as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
A: now :: thesis: ( Ext_eval (p,a) = 0. E implies Ext_eval ((NormPolynomial p),a) = 0. E )
assume Ext_eval (p,a) = 0. E ; :: thesis: Ext_eval ((NormPolynomial p),a) = 0. E
then eval (qa,a) = 0. E by FIELD_4:26;
then ra divides NormPolynomial qa by RING_4:26, RING_5:11;
then eval ((NormPolynomial q),a) = 0. E by RING_5:11;
hence Ext_eval ((NormPolynomial p),a) = 0. E by pr0, FIELD_4:26; :: thesis: verum
end;
now :: thesis: ( Ext_eval ((NormPolynomial p),a) = 0. E implies Ext_eval (p,a) = 0. E )
assume Ext_eval ((NormPolynomial p),a) = 0. E ; :: thesis: Ext_eval (p,a) = 0. E
then eval ((NormPolynomial q),a) = 0. E by pr0, FIELD_4:26;
then ra divides NormPolynomial qa by RING_5:11;
then eval (qa,a) = 0. E by RING_5:11, RING_4:26;
hence Ext_eval (p,a) = 0. E by FIELD_4:26; :: thesis: verum
end;
hence ( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E ) by A; :: thesis: verum