let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )
let a be Element of E; :: thesis: ( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )
set f = hom_Ext_eval (a,F);

A: now :: thesis: ( a is F -algebraic implies FAdj (F,{a}) = RAdj (F,{a}) )

assume a is F -algebraic ; :: thesis: FAdj (F,{a}) = RAdj (F,{a})
then reconsider b = a as F -algebraic Element of E ;
(Polynom-Ring F) / ({(MinPoly (b,F))} -Ideal) is Field ;
then A1: (Polynom-Ring F) / (ker (hom_Ext_eval (a,F))) is Field by mpol1;
(Polynom-Ring F) / (ker (hom_Ext_eval (a,F))), Image (hom_Ext_eval (a,F)) are_isomorphic by RING_2:15;
then reconsider K = Image (hom_Ext_eval (a,F)) as (Polynom-Ring F) / (ker (hom_Ext_eval (a,F))) -isomorphic Ring by RING_3:def 4;
K is Field by A1;
then RAdj (F,{a}) is Field by lemphi4;
hence FAdj (F,{a}) = RAdj (F,{a}) by RF2; :: thesis: verum

end;

now :: thesis: ( FAdj (F,{a}) = RAdj (F,{a}) implies a is F -algebraic )

assume FAdj (F,{a}) = RAdj (F,{a}) ; :: thesis: a is F -algebraic
then B1: Image (hom_Ext_eval (a,F)) is Field by lemphi4;
Image (hom_Ext_eval (a,F)),(Polynom-Ring F) / (ker (hom_Ext_eval (a,F))) are_isomorphic by RING_2:15;
then reconsider K = (Polynom-Ring F) / (ker (hom_Ext_eval (a,F))) as Image (hom_Ext_eval (a,F)) -isomorphic Ring by RING_3:def 4;
B2: K is Field by B1;
{(0. (Polynom-Ring F))} -Ideal = {(0. (Polynom-Ring F))} by IDEAL_1:47;
hence a is F -algebraic by B2, RING_1:21; :: thesis: verum

end;

hence ( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) ) by A; :: thesis: verum