let F be ordered Field; :: thesis: for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
for P being Ordering of F holds
( P extends_to FAdj (F,{a}) iff a ^2 in P )
let E be FieldExtension of F; :: thesis: for a being Element of E st a ^2 in F holds
for P being Ordering of F holds
( P extends_to FAdj (F,{a}) iff a ^2 in P )
let a be Element of E; :: thesis: ( a ^2 in F implies for P being Ordering of F holds
( P extends_to FAdj (F,{a}) iff a ^2 in P ) )
assume AS: a ^2 in F ; :: thesis: for P being Ordering of F holds
( P extends_to FAdj (F,{a}) iff a ^2 in P )
let P be Ordering of F; :: thesis: ( P extends_to FAdj (F,{a}) iff a ^2 in P )

Z: now :: thesis: ( P extends_to FAdj (F,{a}) implies a ^2 in P )

assume P extends_to FAdj (F,{a}) ; :: thesis: a ^2 in P
then consider O being Subset of (FAdj (F,{a})) such that
A: ( P c= O & O is positive_cone ) ;
reconsider K = FAdj (F,{a}) as ordered FieldExtension of F by A, REALALG1:def 17;
reconsider O = O as Ordering of K by A;
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of K ;
H: [a1,a1] in [: the carrier of K, the carrier of K:] ;
B: a1 ^2 in O by REALALG1:23;
C: a1 ^2 = ( the multF of E || the carrier of K) . (a1,a1) by EC_PF_1:def 1
.= a ^2 by H, FUNCT_1:49 ;
O extends P by A, l13;
hence a ^2 in P by AS, C, B, XBOOLE_0:def 4; :: thesis: verum

end;

now :: thesis: ( a ^2 in P implies P extends_to FAdj (F,{a}) )

assume GG: a ^2 in P ; :: thesis: P extends_to FAdj (F,{a})

per cases ( a in F or not a in F ) ;

suppose a in F ; :: thesis: P extends_to FAdj (F,{a})

then {a} c= the carrier of F by TARSKI:def 1;
then A1: FAdj (F,{a}) == F by FIELD_7:3;
then reconsider K = FAdj (F,{a}) as ordered Field by lemPP;
consider Q being Subset of K such that
A2: ( Q = P & Q is positive_cone ) by A1, lemPP;
thus P extends_to FAdj (F,{a}) by A2; :: thesis: verum

end;

suppose AS1: not a in F ; :: thesis: P extends_to FAdj (F,{a})

set K = FAdj (F,{a});
Y0: ( F is Subfield of FAdj (F,{a}) & F is Subring of FAdj (F,{a}) & FAdj (F,{a}) is Subring of E ) by FIELD_4:7, FIELD_4:def 1, FIELD_5:12;
then Y1: ( 0. (FAdj (F,{a})) = 0. F & 1. (FAdj (F,{a})) = 1. F ) by EC_PF_1:def 1;
then Y2: - (1. (FAdj (F,{a}))) = - (1. F) by Y0, FIELD_6:17;

now :: thesis: not - (1. (FAdj (F,{a}))) in QS ((FAdj (F,{a})),P)

assume - (1. (FAdj (F,{a}))) in QS ((FAdj (F,{a})),P) ; :: thesis: contradiction
then consider f being P -quadratic FinSequence of (FAdj (F,{a})) such that
A: - (1. (FAdj (F,{a}))) = Sum f ;
Z: not f is empty by A;
consider g1, g2 being non empty FinSequence of (FAdj (F,{a})) such that
D: ( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) by Z, AS, XYZbS3;
F: - (1. (FAdj (F,{a}))) = (- (1. (FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (0. (FAdj (F,{a})))) ;
G: ( - (1. (FAdj (F,{a}))) in F & 0. (FAdj (F,{a})) in F ) by Y1, Y2;

now :: thesis: for i being Nat st i in dom g1 holds
g1 . i in F

let i be Nat; :: thesis: ( i in dom g1 implies g1 . i in F )
assume i in dom g1 ; :: thesis: g1 . i in F
then consider b being non zero Element of (FAdj (F,{a})), c1, c2 being Element of (FAdj (F,{a})) such that
K3: ( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by D;
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then a is FAdj (F,{a}) -membered ;
then K6: (@ ((FAdj (F,{a})),a)) * (@ ((FAdj (F,{a})),a)) = a ^2 by Y0, FIELD_6:16;
reconsider a3 = a ^2 , b3 = b, c3 = c1, c4 = c2 as Element of F by AS, K3;
b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) = b3 * ((c3 ^2) + ((c4 ^2) * a3))

proof

c1 * c1 = c3 ^2 by Y0, FIELD_6:16;
then K4: b * (c1 ^2) = b3 * (c3 ^2) by Y0, FIELD_6:16;
c2 * c2 = c4 ^2 by Y0, FIELD_6:16;
then b * (c2 ^2) = b3 * (c4 ^2) by Y0, FIELD_6:16;
then K5: (b * (c2 ^2)) * ((@ ((FAdj (F,{a})),a)) ^2) = (b3 * (c4 ^2)) * a3 by Y0, K6, FIELD_6:16;
thus b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) = (b * (c1 ^2)) + (b * ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) by VECTSP_1:def 2
.= (b * (c1 ^2)) + ((b * (c2 ^2)) * ((@ ((FAdj (F,{a})),a)) ^2)) by GROUP_1:def 3
.= ( the addF of (FAdj (F,{a})) || the carrier of F) . [(b3 * (c3 ^2)),((b3 * (c4 ^2)) * a3)] by K4, K5, FUNCT_1:49
.= (b3 * (c3 ^2)) + ((b3 * (c4 ^2)) * a3) by Y0, C0SP1:def 3
.= (b3 * (c3 ^2)) + (b3 * ((c4 ^2) * a3)) by GROUP_1:def 3
.= b3 * ((c3 ^2) + ((c4 ^2) * a3)) by VECTSP_1:def 2 ; :: thesis: verum

end;

hence g1 . i in F by K3; :: thesis: verum

end;

then H: Sum g1 in F by finex;

now :: thesis: for i being Nat st i in dom g2 holds
g2 . i in F

let i be Nat; :: thesis: ( i in dom g2 implies g2 . i in F )
assume i in dom g2 ; :: thesis: g2 . i in F
then consider b being non zero Element of (FAdj (F,{a})), c1, c2 being Element of (FAdj (F,{a})) such that
K3: ( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) by D;
reconsider b3 = b, c3 = c1, c4 = c2 as Element of F by K3;
b * c1 = b3 * c3 by Y0, FIELD_6:16;
then (b * c1) * c2 = (b3 * c3) * c4 by Y0, FIELD_6:16;
hence g2 . i in F by K3; :: thesis: verum

end;

then ( g2 is FinSequence of F & Sum g2 in F ) by finex;
then reconsider Sg2 = Sum g2 as Element of the carrier of F ;
2 '*' (Sum g2) = 2 '*' Sg2 by FIELD_9:7;
then 2 '*' (Sum g2) in F ;
then I: - (1. F) = Sum g1 by Y2, AS, AS1, D, A, F, G, H, XYZc;
for i being Nat st i in dom g1 holds
g1 . i in P

proof

let i be Nat; :: thesis: ( i in dom g1 implies g1 . i in P )
assume i in dom g1 ; :: thesis: g1 . i in P
then consider b being non zero Element of (FAdj (F,{a})), c1, c2 being Element of (FAdj (F,{a})) such that
K3: ( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by D;
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then a is FAdj (F,{a}) -membered ;
then K6: (@ ((FAdj (F,{a})),a)) * (@ ((FAdj (F,{a})),a)) = a ^2 by Y0, FIELD_6:16;
reconsider a3 = a ^2 , b3 = b, c3 = c1, c4 = c2 as Element of F by AS, K3;
K7: b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) = b3 * ((c3 ^2) + ((c4 ^2) * a3))

proof

K7: c1 * c1 = c3 ^2 by Y0, FIELD_6:16;
c2 * c2 = c4 ^2 by Y0, FIELD_6:16;
then K5: (c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2) = (c4 ^2) * a3 by Y0, K6, FIELD_6:16;
(c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2)) = ( the addF of (FAdj (F,{a})) || the carrier of F) . [(c3 ^2),((c4 ^2) * a3)] by K5, K7, FUNCT_1:49
.= (c3 ^2) + ((c4 ^2) * a3) by Y0, C0SP1:def 3 ;
hence b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) = ( the multF of (FAdj (F,{a})) || the carrier of F) . [b3,((c3 ^2) + ((c4 ^2) * a3))] by FUNCT_1:49
.= b3 * ((c3 ^2) + ((c4 ^2) * a3)) by Y0, C0SP1:def 3 ;
:: thesis: verum

end;

K8: ( P is add-closed & P is mult-closed ) ;
KK: c3 ^2 in P by REALALG1:23;
c4 ^2 in P by REALALG1:23;
then (c4 ^2) * a3 in P by GG, K8;
then (c3 ^2) + ((c4 ^2) * a3) in P by KK, K8;
hence g1 . i in P by K8, K7, K3; :: thesis: verum

end;

hence contradiction by I, finP, REALALG1:26; :: thesis: verum

end;

hence P extends_to FAdj (F,{a}) by lemoe2, lemoe4; :: thesis: verum

end;

end;

end;

hence ( P extends_to FAdj (F,{a}) iff a ^2 in P ) by Z; :: thesis: verum