let E be FieldExtension of F; ( E is F -quadratic implies E is F -normal )
assume AS:
E is F -quadratic
; E is F -normal
then reconsider E = E as F -finite FieldExtension of F ;
now for a being Element of E holds MinPoly (a,F) splits_in Elet a be
Element of
E;
MinPoly (b1,F) splits_in E
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider p =
MinPoly (
a,
F) as
Element of the
carrier of
(Polynom-Ring E) ;
reconsider p1 =
p as
Polynomial of
E ;
H:
(
deg (MinPoly (a,F)) <= deg (
E,
F) &
deg (MinPoly (a,F)) = deg p )
by FIELD_10:11, INT_2:27, FIELD_4:20;
0. E =
Ext_eval (
(MinPoly (a,F)),
a)
by FIELD_6:52
.=
eval (
p,
a)
by FIELD_4:26
;
then consider r being
Polynomial of
E such that B:
(rpoly (1,a)) *' r = p1
by RING_5:11, RING_4:1;
MinPoly (
a,
F)
<> 0_. F
;
then C:
r <> 0_. E
by B, FIELD_4:12;
reconsider r1 =
r as
Element of the
carrier of
(Polynom-Ring E) by POLYNOM3:def 10;
(
deg p <= 2 implies not not
deg p = 0 & ... & not
deg p = 2 )
by H;
per cases then
( deg p = 0 or deg p = 1 or deg p = 2 )
by H, AS, FIELD_9:def 26;
suppose
deg p = 1
;
MinPoly (b1,F) splits_in Ethen H: 1 =
(deg (rpoly (1,a))) + (deg r)
by B, C, HURWITZ:23
.=
1
+ (deg r)
by HURWITZ:27
;
then consider b being
Element of
E such that D:
r1 = b | E
by RING_4:def 4, RING_4:20;
r1 = b * (1_. E)
by D, RING_4:16;
then F:
p = b * ((1_. E) *' (rpoly (1,a)))
by B, RING_4:10;
G:
not
b is
zero
by H, D, RING_4:21;
rpoly (1,
a) is
Ppoly of
E
by RING_5:51;
hence
MinPoly (
a,
F)
splits_in E
by G, F, FIELD_4:def 5;
verum end; suppose
deg p = 2
;
MinPoly (b1,F) splits_in Ethen 2 =
(deg (rpoly (1,a))) + (deg r)
by B, C, HURWITZ:23
.=
1
+ (deg r)
by HURWITZ:27
;
then consider c,
b being
Element of
E such that D:
(
c <> 0. E &
r = c * (rpoly (1,b)) )
by HURWITZ:28;
E:
not
c is
zero
by D;
F:
p = c * ((rpoly (1,b)) *' (rpoly (1,a)))
by B, D, RING_4:10;
(
rpoly (1,
a) is
Ppoly of
E &
rpoly (1,
b) is
Ppoly of
E )
by RING_5:51;
then
(rpoly (1,b)) *' (rpoly (1,a)) is
Ppoly of
E
by RING_5:52;
hence
MinPoly (
a,
F)
splits_in E
by E, F, FIELD_4:def 5;
verum end; end;
hence
E is F -normal
by lemmin; verum