let F be non 2 -characteristic Field; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( b ^2 = a implies ( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 ) )
assume AS2: b ^2 = a ; :: thesis: ( 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 :: thesis: 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; :: thesis: ( 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}) ) ; :: thesis: 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;

now :: thesis: for o being object st o in {b} holds
o in the carrier of U

let o be object ; :: thesis: ( o in {b} implies o in the carrier of U )
assume o in {b} ; :: thesis: o in the carrier of U
then o = b by TARSKI:def 1;
hence o in the carrier of U by H10; :: thesis: verum

end;

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; :: thesis: verum

end;

hence FAdj (F,{b}) is SplittingField of X^2- a by H, FIELD_8:def 1; :: thesis: 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; :: thesis: verum