:: Extensions of Orderings
:: by Christoph Schwarzweller
::
:: Received December 18, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users


scheme :: REALALG3:sch 1
3SeqDEx{ F1() -> non empty set , F2() -> Nat, P1[ object , object ], P2[ object , object ], P3[ object , object ] } :
ex p, q, r being FinSequence of F1() st
( dom p = Seg F2() & dom q = Seg F2() & dom r = Seg F2() & ( for k being Nat st k in Seg F2() holds
( P1[k,p . k] & ( for k being Nat st k in Seg F2() holds
( P2[k,q . k] & ( for k being Nat st k in Seg F2() holds
P3[k,r . k] ) ) ) ) ) )
provided
A1: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P1[k,x] and
A2: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P2[k,x] and
A3: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P3[k,x]
proof end;

theorem lempart0: :: REALALG3:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - {(0. L)} = {(0. L)}
proof end;

definition
let R be Ring;
func 2. R -> Element of R equals :: REALALG3:def 1
(1. R) + (1. R);
coherence
(1. R) + (1. R) is Element of R ;
end;

:: deftheorem defines 2. REALALG3:def 1 :
for R being Ring holds 2. R = (1. R) + (1. R);

registration
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible unital V99() V101() right-distributive left-distributive right_unital well-unital V114() left_unital Abelian add-associative right_zeroed V131() domRing-like V206() V240() V281() V282() V283() V284() PID K619() -homomorphic factorial 2 -characteristic for doubleLoopStr ;
existence
ex b1 being Field st b1 is 2 -characteristic
proof end;
end;

registration
let R be 2 -characteristic Ring;
cluster 2. R -> zero ;
coherence
2. R is zero
proof end;
end;

registration
let R be non degenerated non 2 -characteristic Ring;
cluster 2. R -> non zero ;
coherence
not 2. R is zero
proof end;
end;

registration
cluster 2. F_Rat -> non square ;
coherence
not 2. F_Rat is square
proof end;
cluster 2. F_Real -> square ;
coherence
2. F_Real is square
proof end;
end;

registration
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible unital V99() V101() right-distributive left-distributive right_unital well-unital V114() left_unital Abelian add-associative right_zeroed V131() domRing-like V206() V240() preordered V281() V282() V283() V284() PID K619() -homomorphic factorial polynomial_disjoint for doubleLoopStr ;
existence
ex b1 being Field st
( b1 is preordered & b1 is polynomial_disjoint )
proof end;
end;

registration
cluster non empty non degenerated right_complementable V99() well-unital V114() Abelian add-associative right_zeroed preordered -> non degenerated non 2 -characteristic for doubleLoopStr ;
coherence
for b1 being non degenerated Ring st b1 is preordered holds
not b1 is 2 -characteristic
proof end;
end;

theorem finex: :: REALALG3:2
for F being Field
for E being FieldExtension of F
for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in F ) holds
( f is FinSequence of F & Sum f in F )
proof end;

registration
let F be Field;
let a be sum_of_squares Element of F;
let b be non zero sum_of_squares Element of F;
cluster a * (b ") -> sum_of_squares ;
coherence
a * (b ") is sum_of_squares
proof end;
end;

registration
let F be Field;
let f be non empty quadratic FinSequence of F;
cluster Sum f -> sum_of_squares ;
coherence
Sum f is sum_of_squares
proof end;
end;

ll: for R being ZeroStr holds <*> the carrier of R is trivial
proof end;

registration
let R be ZeroStr ;
cluster Relation-like NAT -defined the carrier of R -valued Function-like V34() FinSequence-like FinSubsequence-like trivial for FinSequence of the carrier of R;
existence
ex b1 being FinSequence of R st b1 is trivial
proof end;
end;

registration
let R be ZeroStr ;
cluster <*> the carrier of R -> trivial ;
coherence
<*> the carrier of R is trivial by ll;
cluster empty -> trivial for FinSequence of the carrier of R;
coherence
for b1 being FinSequence of R st b1 is empty holds
b1 is trivial
proof end;
end;

registration
let R be ZeroStr ;
let f, g be trivial FinSequence of R;
cluster f ^ g -> trivial ;
coherence
f ^ g is trivial
proof end;
end;

registration
let R be non degenerated Ring;
let f be non trivial FinSequence of R;
let g be FinSequence of R;
cluster f ^ g -> non trivial ;
coherence
not f ^ g is trivial
proof end;
cluster g ^ f -> non trivial ;
coherence
not g ^ f is trivial
proof end;
end;

registration
let R be Ring;
let f be trivial FinSequence of R;
cluster Sum f -> zero ;
coherence
Sum f is zero
proof end;
end;

definition
let E be Field;
let F be Subfield of E;
let a be Element of F;
func @ (a,E) -> Element of E equals :: REALALG3:def 2
a;
coherence
a is Element of E
proof end;
end;

:: deftheorem defines @ REALALG3:def 2 :
for E being Field
for F being Subfield of E
for a being Element of F holds @ (a,E) = a;

definition
let E be Field;
let F be Subfield of E;
let a be Element of E;
attr a is F -membered means :: REALALG3:def 3
a in the carrier of F;
end;

:: deftheorem defines -membered REALALG3:def 3 :
for E being Field
for F being Subfield of E
for a being Element of E holds
( a is F -membered iff a in the carrier of F );

registration
let E be Field;
let F be Subfield of E;
cluster non irreducible F -membered for Element of the carrier of E;
existence
ex b1 being Element of E st b1 is F -membered
proof end;
end;

definition
let E be Field;
let F be Subfield of E;
let a be Element of E;
assume AS: a is F -membered ;
func @ (F,a) -> Element of F equals :defred: :: REALALG3:def 4
a;
coherence
a is Element of F by AS;
end;

:: deftheorem defred defines @ REALALG3:def 4 :
for E being Field
for F being Subfield of E
for a being Element of E st a is F -membered holds
@ (F,a) = a;

registration
let E be Field;
let F be Subfield of E;
let a be F -membered Element of E;
reduce @ (F,a) to a;
reducibility
@ (F,a) = a by defred;
end;

registration
let R be non degenerated Ring;
cluster 1. R -> non zero ;
coherence
not 1. R is zero ;
cluster - (1. R) -> non zero ;
coherence
not - (1. R) is zero
proof end;
end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
let a, b be P -positive Element of R;
cluster a + b -> P -positive ;
coherence
a + b is P -positive
proof end;
end;

registration
let R be preordered domRing;
let P be Preordering of R;
let a, b be P -positive Element of R;
cluster a * b -> P -positive ;
coherence
a * b is P -positive
proof end;
end;

definition
let R be Ring;
let S be Subset of R;
func S ^+ -> Subset of R equals :: REALALG3:def 5
S \ {(0. R)};
coherence
S \ {(0. R)} is Subset of R ;
func S ^- -> Subset of R equals :: REALALG3:def 6
(- S) \ {(0. R)};
coherence
(- S) \ {(0. R)} is Subset of R ;
end;

:: deftheorem defines ^+ REALALG3:def 5 :
for R being Ring
for S being Subset of R holds S ^+ = S \ {(0. R)};

:: deftheorem defines ^- REALALG3:def 6 :
for R being Ring
for S being Subset of R holds S ^- = (- S) \ {(0. R)};

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster P ^+ -> non empty ;
coherence
not P ^+ is empty
proof end;
cluster P ^- -> non empty ;
coherence
not P ^- is empty
proof end;
end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster (P ^+) /\ (P ^-) -> empty ;
coherence
(P ^+) /\ (P ^-) is empty
proof end;
end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster P ^+ -> add-closed ;
coherence
P ^+ is add-closed
proof end;
end;

registration
let R be preordered domRing;
let P be Preordering of R;
cluster P ^+ -> mult-closed ;
coherence
P ^+ is mult-closed
proof end;
end;

theorem lemP: :: REALALG3:3
for R being non degenerated preordered Ring
for P being Preordering of R holds
( P + (P ^+) c= P ^+ & (P ^+) + P c= P ^+ )
proof end;

theorem :: REALALG3:4
for R being preordered domRing
for P being Preordering of R holds
( (P ^-) * (P ^-) c= P ^+ & (P ^+) * (P ^-) c= P ^- & (P ^-) * (P ^+) c= P ^- )
proof end;

bla: for R being non degenerated Ring
for S being Subset of R st 0. R in S & ( (S ^+) /\ (S ^-) = {} or S ^+ <> S ^- ) & {(S ^+),{(0. R)},(S ^-)} is a_partition of the carrier of R & S ^+ is add-closed & S ^+ is mult-closed holds
S is positive_cone
proof end;

theorem :: REALALG3:5
for R being domRing
for S being Subset of R st S is positive_cone holds
( {(S ^+),{(0. R)},(S ^-)} is a_partition of the carrier of R & S ^+ is add-closed & S ^+ is mult-closed )
proof end;

theorem :: REALALG3:6
for R being non degenerated Ring
for S being Subset of R st {S,{(0. R)},(- S)} is a_partition of the carrier of R & S is add-closed & S is mult-closed holds
S \/ {(0. R)} is positive_cone
proof end;

theorem finP: :: REALALG3:7
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P
proof end;

theorem lemPP: :: REALALG3:8
for F being ordered Field
for P being Ordering of F
for E being Field st E == F holds
( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) )
proof end;

registration
let F be ordered Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible unital V99() V101() right-distributive left-distributive right_unital well-unital V114() left_unital Abelian add-associative right_zeroed V131() domRing-like V206() V240() ordered V281() V282() V283() V284() PID K619() -homomorphic factorial F -extending for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st b1 is ordered
proof end;
end;

definition
let F be Field;
let g be non empty FinSequence of the carrier of (Polynom-Ring F);
let i be Element of dom g;
:: original: .
redefine func g . i -> Element of the carrier of (Polynom-Ring F);
coherence
g . i is Element of the carrier of (Polynom-Ring F)
proof end;
end;

theorem lem23a: :: REALALG3:9
for F being Field
for p, q being Polynomial of F st (LC p) + (LC q) <> 0. F holds
deg (p + q) = max ((deg p),(deg q))
proof end;

theorem lem23d: :: REALALG3:10
for F being Field
for p, q being Polynomial of F holds
( ( deg p > deg q implies LC (p + q) = LC p ) & ( deg p < deg q implies LC (p + q) = LC q ) & ( deg p = deg q & (LC p) + (LC q) <> 0. F implies LC (p + q) = (LC p) + (LC q) ) )
proof end;

theorem lemdeg: :: REALALG3:11
for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds deg (NormPolynomial p) = deg p
proof end;

theorem lem22: :: REALALG3:12
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible )
proof end;

theorem lem21: :: REALALG3:13
for F being Field
for p being Element of the carrier of (Polynom-Ring F) st deg p is odd holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd )
proof end;

theorem lem24: :: REALALG3:14
for F being Field
for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
proof end;

theorem lem23: :: REALALG3:15
for F being ordered Field
for P being Ordering of F
for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
deg p is even
proof end;

theorem lem20: :: REALALG3:16
for F being Field
for E being FieldExtension of F
for p being Polynomial of F
for a being Element of F
for x, b being Element of E st b = a holds
Ext_eval ((a * p),x) = b * (Ext_eval (p,x))
proof end;

theorem lem: :: REALALG3:17
for F being Field
for E being FieldExtension of F
for f being FinSequence of the carrier of (Polynom-Ring F)
for p being Polynomial of F st p = Sum f holds
for a being Element of E
for g being FinSequence of E st len g = len f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
g . i = Ext_eval (q,a) ) holds
Ext_eval (p,a) = Sum g
proof end;

theorem lemBas00: :: REALALG3:18
for F being Field
for E being FieldExtension of F
for a being Element of E
for b being Element of F st b = a ^2 holds
Ext_eval ((X^2- b),a) = 0. E
proof end;

theorem lemBas0: :: REALALG3:19
for F being Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
a is F -algebraic
proof end;

theorem lemBas01: :: REALALG3:20
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )
proof end;

theorem lemBas1: :: REALALG3:21
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E st not a in F holds
for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b
proof end;

theorem ThBas: :: REALALG3:22
for F being Field
for E being FieldExtension of F
for a being Element of E st not a in F & a ^2 in F holds
( {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) & deg ((FAdj (F,{a})),F) = 2 )
proof end;

theorem lemma: :: REALALG3:23
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for b being Element of E holds
( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )
proof end;

theorem XYZb: :: REALALG3:24
for F being Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )
proof end;

theorem XYZc: :: REALALG3:25
for F being Field
for E being FieldExtension of F
for a being Element of E st not a in F & a ^2 in F holds
for c1, c2, d1, d2 being Element of (FAdj (F,{a})) st c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) holds
( c1 = d1 & c2 = d2 )
proof end;

mainX: for F being Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F & not a in F holds
for f being non empty quadratic FinSequence of (FAdj (F,{a})) ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
proof end;

theorem mainY: :: REALALG3:26
for F being Field
for E being FieldExtension of F
for a being Element of E
for b being Element of F
for f being non empty quadratic FinSequence of (FAdj (F,{a})) st not a in F & a ^2 = b holds
ex g1, g2 being non empty quadratic FinSequence of F ex g3 being non empty FinSequence of F st Sum f = (@ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum g3),(FAdj (F,{a})))))
proof end;

theorem maina: :: REALALG3:27
for F being Field
for E being FieldExtension of F
for a being Element of E
for b being Element of F
for f being non empty quadratic FinSequence of (FAdj (F,{a})) st not a in F & a ^2 = b & Sum f in F holds
ex g1, g2 being non empty quadratic FinSequence of F st Sum f = (Sum g1) + (b * (Sum g2))
proof end;

definition
let F be ordered Field;
let E be Field;
let P be Ordering of F;
pred P extends_to E means :: REALALG3:def 7
 ex O being Subset of E st
( P c= O & O is positive_cone );
end;

:: deftheorem defines extends_to REALALG3:def 7 :
for F being ordered Field
for E being Field
for P being Ordering of F holds
( P extends_to E iff ex O being Subset of E st
( P c= O & O is positive_cone ) );

notation
let F be ordered Field;
let E be Field;
let P be Ordering of F;
antonym P not_extends_to E for P extends_to E;
end;

definition
let F be ordered Field;
let E be ordered FieldExtension of F;
let P be Ordering of F;
let O be Ordering of E;
pred O extends P means :: REALALG3:def 8
O /\ the carrier of F = P;
end;

:: deftheorem defines extends REALALG3:def 8 :
for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff O /\ the carrier of F = P );

l12: for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E st ( for a being Element of F holds
( a in P iff a in O ) ) holds
O extends P
proof end;

theorem :: REALALG3:28
for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff for a being Element of F holds
( a in P iff a in O ) ) by XBOOLE_0:def 4, l12;

theorem l13: :: REALALG3:29
for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff P c= O )
proof end;

definition
let R be ordered Ring;
let P be Ordering of R;
let a be Element of R;
func signum (P,a) -> Integer equals :defsgn: :: REALALG3:def 9
1 if a in P \ {(0. R)}
0 if a = 0. R
otherwise - 1;
coherence
( ( a in P \ {(0. R)} implies 1 is Integer ) & ( a = 0. R implies 0 is Integer ) & ( not a in P \ {(0. R)} & not a = 0. R implies - 1 is Integer ) ) ;
consistency
for b1 being Integer st a in P \ {(0. R)} & a = 0. R holds
( b1 = 1 iff b1 = 0 )
proof end;
end;

:: deftheorem defsgn defines signum REALALG3:def 9 :
for R being ordered Ring
for P being Ordering of R
for a being Element of R holds
( ( a in P \ {(0. R)} implies signum (P,a) = 1 ) & ( a = 0. R implies signum (P,a) = 0 ) & ( not a in P \ {(0. R)} & not a = 0. R implies signum (P,a) = - 1 ) );

definition
let R be ordered Ring;
let P be Ordering of R;
func signum P -> Function of the carrier of R,INT means :sgnF: :: REALALG3:def 10
 for a being Element of R holds it . a = signum (P,a);
existence
ex b1 being Function of the carrier of R,INT st
for a being Element of R holds b1 . a = signum (P,a)
proof end;
uniqueness
for b1, b2 being Function of the carrier of R,INT st ( for a being Element of R holds b1 . a = signum (P,a) ) & ( for a being Element of R holds b2 . a = signum (P,a) ) holds
b1 = b2
proof end;
end;

:: deftheorem sgnF defines signum REALALG3:def 10 :
for R being ordered Ring
for P being Ordering of R
for b3 being Function of the carrier of R,INT holds
( b3 = signum P iff for a being Element of R holds b3 . a = signum (P,a) );

theorem :: REALALG3:30
for R being ordered domRing
for P being Ordering of R
for a being Element of R holds a = (signum (P,a)) '*' (abs (P,a))
proof end;

theorem :: REALALG3:31
for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff (signum O) | the carrier of F = signum P )
proof end;

definition
let F be ordered Field;
let E be FieldExtension of F;
let P be Ordering of F;
let f be FinSequence of E;
attr f is P -quadratic means :dq: :: REALALG3:def 11
 for i being Element of NAT st i in dom f holds
ex a being non zero Element of E ex b being Element of E st
( a in P & f . i = a * (b ^2) );
end;

:: deftheorem dq defines -quadratic REALALG3:def 11 :
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for f being FinSequence of E holds
( f is P -quadratic iff for i being Element of NAT st i in dom f holds
ex a being non zero Element of E ex b being Element of E st
( a in P & f . i = a * (b ^2) ) );

registration
let F be ordered Field;
let E be FieldExtension of F;
let P be Ordering of F;
cluster Relation-like NAT -defined the carrier of E -valued Function-like non empty V34() FinSequence-like FinSubsequence-like P -quadratic for FinSequence of the carrier of E;
existence
ex b1 being FinSequence of E st
( b1 is P -quadratic & not b1 is empty )
proof end;
end;

registration
let F be ordered Field;
let P be Ordering of F;
let E be FieldExtension of F;
let f, g be P -quadratic FinSequence of E;
cluster f ^ g -> P -quadratic for FinSequence of E;
coherence
for b1 being FinSequence of E st b1 = f ^ g holds
b1 is P -quadratic
proof end;
end;

theorem XYZbS3a: :: REALALG3:32
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for f being b3 -quadratic FinSequence of E
for g1, g2 being FinSequence of E st f = g1 ^ g2 holds
( g1 is P -quadratic & g2 is P -quadratic )
proof end;

definition
let F be ordered Field;
let E be FieldExtension of F;
let P be Ordering of F;
func P -Quadratic_Sums E -> non empty Subset of E equals :: REALALG3:def 12
 { (Sum f) where f is P -quadratic FinSequence of E : verum } ;
coherence
{ (Sum f) where f is P -quadratic FinSequence of E : verum } is non empty Subset of E
proof end;
end;

:: deftheorem defines -Quadratic_Sums REALALG3:def 12 :
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds P -Quadratic_Sums E = { (Sum f) where f is b3 -quadratic FinSequence of E : verum } ;

notation
let F be ordered Field;
let E be FieldExtension of F;
let P be Ordering of F;
synonym QS (E,P) for P -Quadratic_Sums E;
end;

S1: for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for f, g being b2 -quadratic FinSequence of E st len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)
proof end;

S0: for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for f, g being b2 -quadratic FinSequence of E st Sum f in QS (E,P) & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)
proof end;

registration
let F be ordered Field;
let E be FieldExtension of F;
let P be Ordering of F;
cluster P -Quadratic_Sums E -> non empty mult-closed with_sums_of_squares add-closed ;
coherence
( QS (E,P) is add-closed & QS (E,P) is mult-closed & QS (E,P) is with_sums_of_squares )
proof end;
end;

theorem lemmaA: :: REALALG3:33
for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for a being non zero Element of E holds
( a in QS (E,P) iff ex f being non empty b2 -quadratic FinSequence of E st
( Sum f = a & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) )
proof end;

theorem lemoe1: :: REALALG3:34
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds P c= QS (E,P)
proof end;

theorem lemoe3: :: REALALG3:35
for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E st O extends P holds
QS (E,P) c= O
proof end;

theorem lemoe2: :: REALALG3:36
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds
( QS (E,P) is prepositive_cone iff not - (1. E) in QS (E,P) )
proof end;

theorem lemoe4: :: REALALG3:37
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds
( P extends_to E iff QS (E,P) is prepositive_cone )
proof end;

lemB3: for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E st O extends P holds
for f being non empty b3 -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)}
proof end;

theorem :: REALALG3:38
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds
( P extends_to E iff for f being non empty b3 -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial )
proof end;

theorem XYZbS3: :: REALALG3:39
for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for a being Element of E st a ^2 in F holds
for f being non empty b3 -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( 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 ) ) )
proof end;

theorem oext1: :: REALALG3:40
for F being ordered Field
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 )
proof end;

theorem oext2: :: REALALG3:41
for F being ordered polynomial_disjoint Field
for P being Ordering of F
for a being non square Element of F holds
( P extends_to FAdj (F,{(sqrt a)}) iff a in P )
proof end;

theorem :: REALALG3:42
Positives(F_Rat) extends_to FAdj (F_Rat,{(sqrt (2. F_Rat))})
proof end;

theorem :: REALALG3:43
Positives(F_Rat) not_extends_to FAdj (F_Rat,{(sqrt (- (1. F_Rat)))}) by REALALG1:26, oext2;

theorem :: REALALG3:44
for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for a being Element of F
for b, c being Element of E st b ^2 = a & c ^2 = - a & not P extends_to FAdj (F,{b}) holds
P extends_to FAdj (F,{c})
proof end;

theorem :: REALALG3:45
for F being ordered polynomial_disjoint Field
for P being Ordering of F
for a, b being non square Element of F holds
( not b = - a or P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )
proof end;

theorem FF1: :: REALALG3:46
for F being formally_real Field
for E being FieldExtension of F
for a being Element of F
for b being Element of E st b ^2 = a & a in QS F holds
FAdj (F,{b}) is formally_real
proof end;

theorem FF2: :: REALALG3:47
for F being formally_real Field
for E being FieldExtension of F
for a being Element of F
for b being Element of E st b ^2 = a & not FAdj (F,{b}) is formally_real holds
- a in QS F
proof end;

theorem :: REALALG3:48
for F being ordered polynomial_disjoint Field
for a being non square Element of F st a in QS F holds
FAdj (F,{(sqrt a)}) is formally_real
proof end;

theorem :: REALALG3:49
for F being ordered polynomial_disjoint Field
for a being non square Element of F st not FAdj (F,{(sqrt a)}) is formally_real holds
- a in QS F
proof end;

theorem main: :: REALALG3:50
for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F st deg (E,F) is odd Nat holds
P extends_to E
proof end;

theorem :: REALALG3:51
for F being ordered Field
for P being Ordering of F
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st deg p is odd & a is_a_root_of p,E holds
P extends_to FAdj (F,{a})
proof end;