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

scheme :: REALALG3:sch 1
3SeqDEx{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ], P₂[ object , object ], P₃[ object , object ] } :

ex p, q, r being FinSequence of F₁() st
( dom p = Seg F₂() & dom q = Seg F₂() & dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
( P₁[k,p . k] & ( for k being Nat st k in Seg F₂() holds
( P₂[k,q . k] & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) ) ) ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x] and
A2: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₂[k,x] and
A3: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₃[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 associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed domRing-like gcd-like Euclidian left_zeroed add-left-invertible add-right-invertible Loop-like PID K619() -homomorphic factorial 2 -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ 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 associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed domRing-like gcd-like Euclidian preordered left_zeroed add-left-invertible add-right-invertible Loop-like PID K619() -homomorphic factorial polynomial_disjoint for doubleLoopStr ;

existence
ex b₁ being Field st
( b₁ is preordered & b₁ is polynomial_disjoint )

proof end;

end;

registration

cluster non empty non degenerated right_complementable associative well-unital distributive Abelian add-associative right_zeroed preordered -> non degenerated non 2 -characteristic for doubleLoopStr ;

coherence
for b₁ being non degenerated Ring st b₁ is preordered holds
not b₁ 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 finite FinSequence-like FinSubsequence-like trivial for FinSequence of the carrier of R;

existence
ex b₁ being FinSequence of R st b₁ 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 b₁ being FinSequence of R st b₁ is empty holds
b₁ 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 b₁ being Element of E st b₁ 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 associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed domRing-like gcd-like Euclidian ordered left_zeroed add-left-invertible add-right-invertible Loop-like PID K619() -homomorphic factorial F -extending for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ 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 b₁ -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 b₁ -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 b₁ -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 b₁ being Integer st a in P \ {(0. R)} & a = 0. R holds
( b₁ = 1 iff b₁ = 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 b₁ being Function of the carrier of R,INT st
for a being Element of R holds b₁ . a = signum (P,a)

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of R,INT st ( for a being Element of R holds b₁ . a = signum (P,a) ) & ( for a being Element of R holds b₂ . a = signum (P,a) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem sgnF defines signum REALALG3:def 10 :
for R being ordered Ring
for P being Ordering of R
for b₃ being Function of the carrier of R,INT holds
( b₃ = signum P iff for a being Element of R holds b₃ . 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 finite FinSequence-like FinSubsequence-like P -quadratic for FinSequence of the carrier of E;

existence
ex b₁ being FinSequence of E st
( b₁ is P -quadratic & not b₁ 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 b₁ being FinSequence of E st b₁ = f ^ g holds
b₁ 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 b₃ -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 b₃ -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 b₂ -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 b₂ -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 b₂ -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 b₃ -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 b₃ -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 b₃ -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;