let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p
let p be non constant Element of the carrier of (Polynom-Ring F); for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p
let E be FieldExtension of F; ( p splits_in E implies FAdj (F,(Roots (E,p))) is SplittingField of p )
assume AS:
p splits_in E
; FAdj (F,(Roots (E,p))) is SplittingField of p
set K = FAdj (F,(Roots (E,p)));
thus
p splits_in FAdj (F,(Roots (E,p)))
by AS, lemma5; FIELD_8:def 1 for E being FieldExtension of F st p splits_in E & E is Subfield of FAdj (F,(Roots (E,p))) holds
E == FAdj (F,(Roots (E,p)))
now for U being FieldExtension of F st U is Subfield of FAdj (F,(Roots (E,p))) & p splits_in U holds
FAdj (F,(Roots (E,p))) is Subfield of Ulet U be
FieldExtension of
F;
( U is Subfield of FAdj (F,(Roots (E,p))) & p splits_in U implies FAdj (F,(Roots (E,p))) is Subfield of U )assume B:
(
U is
Subfield of
FAdj (
F,
(Roots (E,p))) &
p splits_in U )
;
FAdj (F,(Roots (E,p))) is Subfield of UC:
U is
Subfield of
E
by B, EC_PF_1:5;
then C1:
E is
FieldExtension of
U
by FIELD_4:7;
D:
F is
Subfield of
U
by FIELD_4:7;
E:
Roots (
U,
p)
c= Roots (
E,
p)
by C1, lemma7;
Roots (
E,
p)
c= Roots (
U,
p)
by C1, AS, B, lemma3;
then
Roots (
E,
p) is
Subset of
U
by E, XBOOLE_0:def 10;
hence
FAdj (
F,
(Roots (E,p))) is
Subfield of
U
by D, C, FIELD_6:37;
verum end;
hence
for E being FieldExtension of F st p splits_in E & E is Subfield of FAdj (F,(Roots (E,p))) holds
E == FAdj (F,(Roots (E,p)))
; verum