let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff a is_integral_over F )
let E be FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -algebraic iff a is_integral_over F )
let a be Element of E; :: thesis: ( a is F -algebraic iff a is_integral_over F )
set g = hom_Ext_eval (a,F);

A: now :: thesis: ( a is_integral_over F implies a is F -algebraic )

assume a is_integral_over F ; :: thesis: a is F -algebraic
then consider p being Polynomial of F such that
A1: ( LC p = 1. F & Ext_eval (p,a) = 0. E ) ;
(0_. F) . ((len (0_. F)) -' 1) = 0. F ;
then p <> 0_. F by A1, RATFUNC1:def 6;
then A3: p <> 0. (Polynom-Ring F) by POLYNOM3:def 10;
reconsider b = p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
(hom_Ext_eval (a,F)) . p = 0. E by A1, ALGNUM_1:def 11;
then b in { x where x is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . x = 0. E } ;
then b in ker (hom_Ext_eval (a,F)) by VECTSP10:def 9;
hence a is F -algebraic by A3, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: ( a is F -algebraic implies a is_integral_over F )

assume A0: a is F -algebraic ; :: thesis: a is_integral_over F

now :: thesis: ex p being Element of the carrier of (Polynom-Ring F) st
( p in ker (hom_Ext_eval (a,F)) & p <> 0. (Polynom-Ring F) )

assume AS: for p being Element of the carrier of (Polynom-Ring F) holds
( not p in ker (hom_Ext_eval (a,F)) or not p <> 0. (Polynom-Ring F) ) ; :: thesis: contradiction
for x being object holds
( x in ker (hom_Ext_eval (a,F)) iff x = 0. (Polynom-Ring F) )

proof

let x be object ; :: thesis: ( x in ker (hom_Ext_eval (a,F)) iff x = 0. (Polynom-Ring F) )

now :: thesis: ( x = 0. (Polynom-Ring F) implies x in ker (hom_Ext_eval (a,F)) )

assume A2: x = 0. (Polynom-Ring F) ; :: thesis: x in ker (hom_Ext_eval (a,F))
then (hom_Ext_eval (a,F)) . x = 0. E by RING_2:6;
then x in { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } by A2;
hence x in ker (hom_Ext_eval (a,F)) by VECTSP10:def 9; :: thesis: verum

end;

hence ( x in ker (hom_Ext_eval (a,F)) iff x = 0. (Polynom-Ring F) ) by AS; :: thesis: verum

end;

hence contradiction by A0, TARSKI:def 1; :: thesis: verum

end;

then consider p being Element of the carrier of (Polynom-Ring F) such that
A1: ( p in ker (hom_Ext_eval (a,F)) & p <> 0. (Polynom-Ring F) ) ;
p <> 0_. F by A1, POLYNOM3:def 10;
then reconsider p = p as non zero Element of the carrier of (Polynom-Ring F) by UPROOTS:def 5;
set q = NormPolynomial p;
A2: LC (NormPolynomial p) = 1. F by RATFUNC1:def 7;
ker (hom_Ext_eval (a,F)) = { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } by VECTSP10:def 9;
then consider v being Element of the carrier of (Polynom-Ring F) such that
A3: ( v = p & (hom_Ext_eval (a,F)) . v = 0. E ) by A1;
Ext_eval (p,a) = 0. E by A3, ALGNUM_1:def 11;
then Ext_eval ((NormPolynomial p),a) = 0. E by pr1;
hence a is_integral_over F by A2; :: thesis: verum

end;

hence ( a is F -algebraic iff a is_integral_over F ) by A; :: thesis: verum