let F be non 2 -characteristic Field; for E being FieldExtension of F
for a being Element of F st ( for b being Element of F holds not a = b ^2 ) holds
for b being Element of E st b ^2 = a holds
( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 )
let E be FieldExtension of F; for a being Element of F st ( for b being Element of F holds not a = b ^2 ) holds
for b being Element of E st b ^2 = a holds
( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 )
let a be Element of F; ( ( for b being Element of F holds not a = b ^2 ) implies for b being Element of E st b ^2 = a holds
( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 ) )
assume AS1:
for b being Element of F holds not a = b ^2
; for b being Element of E st b ^2 = a holds
( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 )
let b be Element of E; ( b ^2 = a implies ( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 ) )
assume AS2:
b ^2 = a
; ( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 )
reconsider a1 = a as square Element of E by AS2;
F is Subring of E
by FIELD_4:def 1;
then H1:
( 0. E = 0. F & 1. E = 1. F & - a1 = - a )
by FIELD_6:17, C0SP1:def 3;
H0: b * (- b) =
- (b * b)
by VECTSP_1:8
.=
- a1
by AS2, O_RING_1:def 1
;
H2: X^2- a =
<%(- a1),(- (0. E)),(1. E)%>
by H1
.=
<%(b * (- b)),(- (b + (- b))),(1. E)%>
by H0, RLVECT_1:5
.=
(rpoly (1,b)) *' (rpoly (1,(- b)))
by lemred3z
;
( rpoly (1,b) is Ppoly of E & rpoly (1,(- b)) is Ppoly of E )
by RING_5:51;
then reconsider p = X^2- a as Ppoly of E by H2, RING_5:52;
H3:
(1. E) * p = X^2- a
;
then H11:
X^2- a splits_in E
by FIELD_4:def 5;
H5:
( Roots (rpoly (1,b)) = {b} & Roots (rpoly (1,(- b))) = {(- b)} )
by RING_5:18;
H9: Roots (E,(X^2- a)) =
Roots (X^2- a1)
by H1, FIELD_7:13
.=
{b} \/ {(- b)}
by H2, H1, H5, UPROOTS:23
.=
{b,(- b)}
by ENUMSET1:1
;
then
X^2- a splits_in FAdj (F,{b,(- b)})
by H3, FIELD_8:30, FIELD_4:def 5;
then H:
X^2- a splits_in FAdj (F,{b})
by ext1;
now for U being FieldExtension of F st X^2- a splits_in U & U is Subfield of FAdj (F,{b}) holds
U == FAdj (F,{b})let U be
FieldExtension of
F;
( X^2- a splits_in U & U is Subfield of FAdj (F,{b}) implies U == FAdj (F,{b}) )assume AS:
(
X^2- a splits_in U &
U is
Subfield of
FAdj (
F,
{b}) )
;
U == FAdj (F,{b})then H8:
(
FAdj (
F,
{b}) is
FieldExtension of
U &
E is
FieldExtension of
FAdj (
F,
{b}) )
by FIELD_4:7;
then H6:
U is
Subfield of
E
by FIELD_4:7;
H7:
F is
Subfield of
U
by FIELD_4:7;
Roots (
E,
(X^2- a))
= Roots (
U,
(X^2- a))
by H11, AS, H8, FIELD_8:29;
then H10:
b in Roots (
U,
(X^2- a))
by H9, TARSKI:def 2;
then
{b} c= the
carrier of
U
;
then
FAdj (
F,
{b}) is
Subfield of
U
by H6, H7, FIELD_6:37;
hence
U == FAdj (
F,
{b})
by AS, FIELD_7:def 2;
verum end;
hence
FAdj (F,{b}) is SplittingField of X^2- a
by H, FIELD_8:def 1; deg ((FAdj (F,{b})),F) = 2
eval ((X^2- a1),b) = 0. E
by AS2, m105;
then H12:
Ext_eval ((X^2- a),b) = 0. E
by H1, FIELD_4:26;
then reconsider b1 = b as F -algebraic Element of E by FIELD_6:43;
X^2- a is irreducible
by naH2, AS1, O_RING_1:def 2;
then H11: MinPoly (b1,F) =
NormPolynomial (X^2- a)
by H12, FIELD_8:15
.=
X^2- a
by RING_4:24
;
deg (X^2- a) = 2
by defquadr;
hence
deg ((FAdj (F,{b})),F) = 2
by H11, FIELD_6:67; verum