let F be Field; for E being FieldExtension of F
for a being F -algebraic Element of E holds
( FAdj (F,{a}) is F -normal iff MinPoly (a,F) splits_in FAdj (F,{a}) )
let E be FieldExtension of F; for a being F -algebraic Element of E holds
( FAdj (F,{a}) is F -normal iff MinPoly (a,F) splits_in FAdj (F,{a}) )
let a be F -algebraic Element of E; ( FAdj (F,{a}) is F -normal iff MinPoly (a,F) splits_in FAdj (F,{a}) )
set K = FAdj (F,{a});
( {a} is Subset of (FAdj (F,{a})) & a in {a} )
by FIELD_6:35, TARSKI:def 1;
then reconsider a1 = a as Element of (FAdj (F,{a})) ;
E is FAdj (F,{a}) -extending
by FIELD_4:7;
then Ext_eval ((MinPoly (a,F)),a1) =
Ext_eval ((MinPoly (a,F)),a)
by FIELD_6:11
.=
0. E
by FIELD_6:52
.=
0. (FAdj (F,{a}))
by EC_PF_1:def 1
;
then H1:
a1 is_a_root_of MinPoly (a,F), FAdj (F,{a})
by FIELD_4:def 2;
Roots ((FAdj (F,{a})),(MinPoly (a,F))) = { b where b is Element of (FAdj (F,{a})) : b is_a_root_of MinPoly (a,F), FAdj (F,{a}) }
by FIELD_4:def 4;
then H2:
a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
by H1;
now ( MinPoly (a,F) splits_in FAdj (F,{a}) implies FAdj (F,{a}) is F -normal )assume AS:
MinPoly (
a,
F)
splits_in FAdj (
F,
{a})
;
FAdj (F,{a}) is F -normal now for U being FieldExtension of F st MinPoly (a,F) splits_in U & U is Subfield of FAdj (F,{a}) holds
U == FAdj (F,{a})let U be
FieldExtension of
F;
( MinPoly (a,F) splits_in U & U is Subfield of FAdj (F,{a}) implies U == FAdj (F,{a}) )assume B:
(
MinPoly (
a,
F)
splits_in U &
U is
Subfield of
FAdj (
F,
{a}) )
;
U == FAdj (F,{a})then
FAdj (
F,
{a}) is
U -extending
by FIELD_4:7;
then
Roots (
(FAdj (F,{a})),
(MinPoly (a,F)))
c= the
carrier of
U
by AS, B, FIELD_8:27;
then
a in the
carrier of
U
by H2;
then
{a} c= the
carrier of
U
by TARSKI:def 1;
then
(
{a} is
Subset of
U &
F is
Subfield of
U &
U is
Subfield of
E )
by FIELD_4:7, B, EC_PF_1:5;
then
FAdj (
F,
{a}) is
Subfield of
U
by FIELD_6:37;
hence
U == FAdj (
F,
{a})
by B, FIELD_7:def 2;
verum end; then
FAdj (
F,
{a}) is
SplittingField of
MinPoly (
a,
F)
by AS, FIELD_8:def 1;
hence
FAdj (
F,
{a}) is
F -normal
;
verum end;
hence
( FAdj (F,{a}) is F -normal iff MinPoly (a,F) splits_in FAdj (F,{a}) )
by H1, FIELD_4:def 3; verum