let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )
let E be FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )
let a be Element of E; :: thesis: ( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )
set g = hom_Ext_eval (a,F);
A: now :: thesis: ( a is F -algebraic implies ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )
assume a is F -algebraic ; :: thesis: ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E
then a is_integral_over F by alg1;
then consider p being Polynomial of F such that
A1: ( LC p = 1. F & Ext_eval (p,a) = 0. E ) ;
LC (0_. F) = (0_. F) . ((len (0_. F)) -' 1) by RATFUNC1:def 6
.= 0. F ;
then not p is zero by A1, UPROOTS:def 5;
hence ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E by A1; :: thesis: verum
end;
now :: thesis: ( ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E implies a is F -algebraic )
assume ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E ; :: thesis: a is F -algebraic
then consider p being non zero Polynomial of F such that
A1: Ext_eval (p,a) = 0. E ;
A2: (hom_Ext_eval (a,F)) . p = 0. E by A1, ALGNUM_1:def 11;
reconsider b = p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
p <> 0_. F ;
then not b is zero by POLYNOM3:def 10;
then reconsider b = b as non zero Element of (Polynom-Ring F) ;
b in { x where x is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . x = 0. E } by A2;
then b in ker (hom_Ext_eval (a,F)) by VECTSP10:def 9;
hence a is F -algebraic by TARSKI:def 1; :: thesis: verum
end;
hence ( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E ) by A; :: thesis: verum