let F be Field; for E being FieldExtension of F
for K being b1 -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds
K is F -algebraic
let E be FieldExtension of F; for K being E -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds
K is F -algebraic
let K be E -extending FieldExtension of F; ( K is E -algebraic & E is F -algebraic implies K is F -algebraic )
assume AS:
( K is E -algebraic & E is F -algebraic )
; K is F -algebraic
now for a being Element of K holds a is F -algebraic let a be
Element of
K;
a is F -algebraic consider p being non
zero Polynomial of
E such that A:
Ext_eval (
p,
a)
= 0. K
by AS, FIELD_6:43;
reconsider T =
Coeff p as
finite Subset of
E ;
T is
F -algebraic
by AS;
then reconsider T =
T as
finite F -algebraic Subset of
E ;
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, cof2;
(
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, lemma7b;
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, alg1;
verum end;
hence
K is F -algebraic
; verum