let F be Field; :: thesis: for E being F -algebraic FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of K st a is E -algebraic holds
a is F -algebraic
let E be F -algebraic FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for a being Element of K st a is E -algebraic holds
a is F -algebraic
let K be E -extending FieldExtension of F; :: thesis: for a being Element of K st a is E -algebraic holds
a is F -algebraic
let a be Element of K; :: thesis: ( a is E -algebraic implies a is F -algebraic )
assume a is E -algebraic ; :: thesis: a is F -algebraic
then consider p being non zero Polynomial of E such that
A: Ext_eval (p,a) = 0. K by FIELD_6:43;
reconsider T = Coeff p as finite Subset of E ;
for a being Element of E st a in T holds
a is F -algebraic ;
then reconsider T = T as finite F -algebraic Subset of E by FIELD_7:def 12;
set B = FAdj (F,T);
E is FieldExtension of FAdj (F,T) by FIELD_4:7;
then reconsider K1 = K as FieldExtension of FAdj (F,T) ;
E: ( K1 is FAdj (F,T) -extending & E is FAdj (F,T) -extending ) by FIELD_4:7;
reconsider a1 = a as Element of K1 ;
T is Subset of (FAdj (F,T)) by FIELD_6:35;
then reconsider p1 = p as non zero Polynomial of (FAdj (F,T)) by E, FIELD_7:12;
( p1 is Element of the carrier of (Polynom-Ring (FAdj (F,T))) & p is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then Ext_eval (p1,a) = 0. K by A, E, FIELD_7:15;
then reconsider a1 = a as FAdj (F,T) -algebraic Element of K1 by FIELD_6:43;
reconsider B1 = FAdj ((FAdj (F,T)),{a1}) as FieldExtension of F ;
F: {a} is Subset of (FAdj ((FAdj (F,T)),{a1})) by FIELD_6:35;
G: K is B1 -extending by FIELD_4:7;
a in {a} by TARSKI:def 1;
then a in FAdj ((FAdj (F,T)),{a1}) by F;
hence a is F -algebraic by G, FIELD_7:33; :: thesis: verum