let F be Field; for E being F -algebraic FieldExtension of F holds
( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E )
let E be F -algebraic FieldExtension of F; ( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E )
now ( ( for a being Element of E holds MinPoly (a,F) splits_in E ) implies E is F -normal )assume AS:
for
a being
Element of
E holds
MinPoly (
a,
F)
splits_in E
;
E is F -normal now for p being irreducible Element of the carrier of (Polynom-Ring F) st p is_with_roots_in E holds
p splits_in Elet p be
irreducible Element of the
carrier of
(Polynom-Ring F);
( p is_with_roots_in E implies p splits_in E )assume
p is_with_roots_in E
;
p splits_in Ethen consider a being
Element of
E such that B:
a is_a_root_of p,
E
by FIELD_4:def 3;
Ext_eval (
p,
a)
= 0. E
by B, FIELD_4:def 2;
then consider q being
Polynomial of
F such that C:
p = (MinPoly (a,F)) *' q
by FIELD_6:53, RING_4:1;
reconsider q1 =
q as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
q <> 0_. F
by C;
then
deg p = (deg (MinPoly (a,F))) + (deg q)
by C, HURWITZ:23;
then
((deg p) - (deg q)) + (deg q) > 0 + (deg q)
by RING_4:def 4, XREAL_1:8;
then
deg q1 < 1
by C, RING_4:1, RING_4:40;
then
(deg q1) + 1
<= 1
by INT_1:7;
then
((deg q1) + 1) - 1
<= 1
- 1
by XREAL_1:9;
then consider b being
Element of
F such that G:
q1 = b | F
by RING_4:def 4, RING_4:20;
H:
F is
Subring of
E
by FIELD_4:def 1;
then
the
carrier of
F c= the
carrier of
E
by C0SP1:def 3;
then reconsider d =
b as
Element of
E ;
q <> (0. F) | F
by C;
then
d <> 0. E
by G, H, C0SP1:def 3;
then reconsider d =
d as non
zero Element of
E by STRUCT_0:def 12;
reconsider q2 =
d | E as
Element of the
carrier of
(Polynom-Ring E) by POLYNOM3:def 10;
H:
d | E = b | F
by FIELD_6:23;
consider c being non
zero Element of
E,
r being
Ppoly of
E such that I:
MinPoly (
a,
F)
= c * r
by AS, FIELD_4:def 5;
p =
(c * r) *' (d | E)
by C, I, G, H, FIELD_4:17
.=
(c * r) *' (d * (1_. E))
by RING_4:16
.=
d * ((c * r) *' (1_. E))
by RING_4:10
.=
(d * c) * r
by RING_4:11
;
hence
p splits_in E
by FIELD_4:def 5;
verum end; hence
E is
F -normal
;
verum end;
hence
( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E )
by A; verum