:: Ordered Rings and Fields
:: by Christoph Schwarzweller
::
:: Received March 17, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, ALGSTR_0, TARSKI,
STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, PYTHTRIP, REALSET1, GLIB_000,
VECTSP_2, CARD_1, MESFUNC1, INT_3, LATTICES, ORDINAL4, INT_1, ALGSEQ_1,
COMPLFLD, BINOP_1, NUMBERS, IDEAL_1, C0SP1, SQUARE_1, RATFUNC1, FUNCSDOM,
XXREAL_0, HURWITZ, GROUP_1, FINSEQ_1, CARD_3, ZFMISC_1, COMPLEX1,
POLYNOM1, POLYNOM3, XBOOLE_0, ARYTM_1, GAUSSINT, XCMPLX_0, RING_3,
INTERVA1, RELAT_2, PARTFUN1, REALALG1, QMAX_1, ARROW, O_RING_1;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2,
FUNCT_1, FINSEQ_1, REALSET1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2,
BINOP_1, XCMPLX_0, SQUARE_1, XXREAL_0, XREAL_0, CARD_1, XXREAL_2,
COMPLEX1, NAT_1, INT_1, NAT_D, RAT_1, INT_3, NUMBERS, STRUCT_0, BINOM,
ALGSTR_0, GROUP_1, GROUP_2, O_RING_1, VFUNCT_1, RATFUNC1, POLYNOM1,
ALGSEQ_1, POLYNOM3, HURWITZ, RLVECT_1, VECTSP_2, VECTSP_1, COMPLFLD,
GAUSSINT, IDEAL_1, C0SP1, RING_3, ALG_1, UPROOTS, ARROW;
constructors BINOM, REALSET1, BINOP_2, RINGCAT1, ARYTM_2, ARYTM_3, XXREAL_2,
RING_3, GAUSSINT, NAT_D, TOPALG_7, RATFUNC1, FINSEQ_1, GROUP_4, COMPLEX1,
FVSUM_1, XXREAL_0, XREAL_0, SQUARE_1, POLYNOM3, ALGSEQ_1, VFUNCT_1,
HURWITZ, UPROOTS, ARROW, O_RING_1, GROUP_2;
registrations ORDINAL1, XXREAL_0, XREAL_0, RELSET_1, VECTSP_1, STRUCT_0,
MEMBERED, NUMBERS, RLVECT_1, INT_1, INT_3, COMPLFLD, RATFUNC1, POLYNOM4,
POLYNOM3, RAT_1, REALSET1, GAUSSINT, NAT_1, ALGSTR_1, SUBSET_1, RELAT_2,
FUNCT_2, RING_3, XCMPLX_0, FINSEQ_1, NAT_2, CARD_1, VFUNCT_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, IDEAL_1;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1,
COMPLEX1, POLYNOM3, GROUP_2, O_RING_1, HURWITZ, SQUARE_1, RATFUNC1;
expansions STRUCT_0, XBOOLE_0, TARSKI, ARROW, IDEAL_1, UPROOTS, O_RING_1,
ALGSEQ_1;
theorems GROUP_1, VECTSP_1, FUNCT_2, TARSKI, BINOM, INT_1, XREAL_0, BHSP_1,
FUNCT_1, RLVECT_1, RING_3, XBOOLE_0, IDEAL_1, C0SP1, NAT_1, GAUSSINT,
RELAT_1, ZFMISC_1, COMPLFLD, RAT_1, INT_3, XXREAL_0, XREAL_1, RELSET_1,
FINSEQ_1, RELAT_2, POLYNOM1, POLYNOM3, NORMSP_1, ALGSEQ_1, PARTFUN1,
FINSEQ_2, XTUPLE_0, POLYNOM8, SQUARE_1, POLYNOM4, FUNCOP_1, STRUCT_0,
VECTSP_2, HURWITZ, POLYNOM2, ORDINAL1, FINSEQ_3, UPROOTS;
schemes NAT_1, FINSEQ_1;
begin :: On Order Relations
definition
let X be set;
let R be Relation of X;
attr R is strongly_reflexive means :defstr:
R is_reflexive_in X;
attr R is totally_connected means :Rtot:
R is_strongly_connected_in X;
end;
registration
let X be set;
cluster strongly_reflexive for Relation of X;
existence
proof
per cases;
suppose AS: X is empty;
reconsider R = {} as Relation of X,X by RELSET_1:12;
take R;
for o be object st o in X holds [o,o] in R by AS;
hence R is strongly_reflexive by RELAT_2:def 1;
end;
suppose AS: X is non empty;
set R = the set of all [x,y] where x,y is Element of X;
now let o be object;
assume o in R;
then consider x,y being Element of X such that A: o = [x,y];
thus o in [:X,X:] by AS,A,ZFMISC_1:def 2;
end;
then reconsider R as Relation of X by TARSKI:def 3;
take R;
for o be object st o in X holds [o,o] in R;
hence R is strongly_reflexive by RELAT_2:def 1;
end;
end;
cluster totally_connected for Relation of X;
existence
proof
per cases;
suppose AS: X is empty;
reconsider R = {} as Relation of X,X by RELSET_1:12;
take R;
for x,y be object st x in X & y in X holds [x,y] in R or [y,x] in R by AS;
hence R is totally_connected by RELAT_2:def 7;
end;
suppose AS: X is non empty;
set R = the set of all [x,y] where x,y is Element of X;
now let o be object;
assume o in R;
then consider x,y being Element of X such that A: o = [x,y];
thus o in [:X,X:] by AS,A,ZFMISC_1:def 2;
end;
then reconsider R as Relation of X by TARSKI:def 3;
take R;
for x,y be object st x in X & y in X holds [x,y] in R or [y,x] in R;
hence R is totally_connected by RELAT_2:def 7;
end;
end;
end;
registration
let X be set;
cluster strongly_reflexive -> reflexive for Relation of X;
coherence
proof
let R be Relation of X;
assume AS: R is strongly_reflexive;
H: field R c= X \/ X by RELSET_1:8;
now let o be object;
assume A: o in field R;
then reconsider x = o as Element of X by H;
per cases;
suppose X is empty;
hence [o,o] in R by H,A;
end;
suppose X is non empty;
then x in X;
hence [o,o] in R by AS,RELAT_2:def 1;
end;
end;
hence R is reflexive by RELAT_2:def 9,RELAT_2:def 1;
end;
cluster totally_connected -> strongly_connected for Relation of X;
coherence
proof
let R be Relation of X;
assume AS: R is totally_connected;
H: field R c= X \/ X by RELSET_1:8;
now let o1,o2 be object;
assume A: o1 in field R & o2 in field R;
then reconsider x = o1, y = o2 as Element of X by H;
per cases;
suppose X is empty;
hence [o1,o2] in R or [o2,o1] in R by H,A;
end;
suppose X is non empty;
then [x,y] in R or [y,x] in R by AS,RELAT_2:def 7;
hence [o1,o2] in R or [o2,o1] in R;
end;
end;
hence R is strongly_connected by RELAT_2:def 15,RELAT_2:def 7;
end;
end;
registration
let X be non empty set;
cluster strongly_reflexive -> non empty for Relation of X;
coherence
proof
let R be Relation of X;
assume AS: R is strongly_reflexive;
set x = the Element of X;
[x,x] in R by AS,RELAT_2:def 1;
hence thesis;
end;
cluster totally_connected -> non empty for Relation of X;
coherence
proof
let R be Relation of X;
assume R is totally_connected; then
for x,y being Element of X holds [x,y] in R or [y,x] in R by RELAT_2:def 7;
hence thesis;
end;
end;
theorem
for X being non empty set
for R being strongly_reflexive Relation of X
for x being Element of X holds x <=_R,x by defstr,RELAT_2:def 1;
theorem lemanti:
for X being non empty set
for R being antisymmetric Relation of X
for x,y being Element of X st x <=_R,y & y <=_R,x holds x = y
proof
let X be non empty set; let R be antisymmetric Relation of X;
let x,y be Element of X;
assume A: x <=_R,y & y <=_R,x;
then x in field R & y in field R by RELAT_1:15;
hence x = y by A,RELAT_2:def 4,RELAT_2:def 12;
end;
theorem lemtrans:
for X being non empty set
for R being transitive Relation of X
for x,y,z being Element of X st x <=_R,y & y <=_R,z holds x <=_R,z
proof
let X be non empty set; let R be transitive Relation of X;
let x,y,z be Element of X;
assume A: x <=_R,y & y <=_R,z;
then x in field R & y in field R & z in field R by RELAT_1:15;
hence thesis by A,RELAT_2:def 8,RELAT_2:def 16;
end;
theorem
for X being non empty set
for R being totally_connected Relation of X
for x,y being Element of X holds x <=_R,y or y <=_R,x by Rtot,RELAT_2:def 7;
definition
let L be addLoopStr;
let R be Relation of L;
attr R is respecting_addition means :respadd:
for a,b,c being Element of L st a <=_R,b holds a+c <=_R,b+c;
end;
definition
let L be multLoopStr_0;
let R be Relation of L;
attr R is respecting_multiplication means :respmult:
for a,b,c being Element of L st a <=_R,b & 0.L <=_R,c holds a*c <=_R,b*c;
end;
begin :: About Minimal Positive Indices of Polynomials
::: present in NIVEN, make there explicit and remove
lemmul: for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for p,q be Polynomial of L
st p <> 0_.(L) & q <> 0_.(L)
holds (p*'q).(len p + len q - 1 -'1) = p.(len p-'1) * q.(len q-'1)
proof
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr; let p,q be Polynomial of L;
assume p <> 0_.(L) & q <> 0_.(L);
then B: len p >= 1 & len q >= 1 by NAT_1:14,POLYNOM4:5;
then len p + len q >= 1 + 1 by XREAL_1:7;
then A: len p + len q - 1 >= 1 + 1 - 1 by XREAL_1:9;
reconsider j = len p + len q - 1 as Element of NAT by B,INT_1:3;
set i = j -' 1;
consider r being FinSequence of the carrier of L such that
M: len r = i+1 & (p*'q).i = Sum r &
for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i+1-'k)
by POLYNOM3:def 9;
A7: j - 1 = i by A,XREAL_0:def 2;
reconsider x = len q - 1 as Element of NAT by B,INT_1:3;
A3: j = len p + x;
then j >= len p by NAT_1:11;
then A1: len p in dom r by A7,M,B,FINSEQ_3:25;
A2: i+1-'(len p)
= (len p + len q - 1 - 1 + 1) - (len p) by A3,A7,XREAL_0:def 2
.= len p - (len p) + len q - 1
.= len q -' 1 by B,XREAL_0:def 2;
now let k be Element of NAT;
assume E: k in dom r & k <> len p;
per cases by E,XXREAL_0:1;
suppose E1: k > len p;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
E2: k1 + 1 > len p by E1;
k -' 1 = k - 1 by E1,XREAL_0:def 2;
then p.(k-'1) = 0.L by E2,ALGSEQ_1:8,NAT_1:13;
then r.k = 0.L * q.(i+1-'k) by E,M;
hence r/.k = 0.L by E,PARTFUN1:def 6;
end;
suppose k < len p;
then k + 1 <= len p by INT_1:7;
then k + 1 - k <= len p - k by XREAL_1:9;
then len p - k + len q >= 1 + len q by XREAL_1:6;
then E2: len p - k + len q - 1 >= len q + 1 - 1 by XREAL_1:9;
i + 1 - k = (len p + len q - 1 - 1 + 1) - k by A,XREAL_0:def 2;
then i+1-'k = len p + len q - 1 - k by E2,XREAL_0:def 2;
then q.(i+1-'k) = 0.L by E2,ALGSEQ_1:8;
then r.k = p.(k-'1) * 0.L by E,M;
hence r/.k = 0.L by E,PARTFUN1:def 6;
end;
end;
then Sum r = r/.(len p) by A1,POLYNOM2:3
.= r.(len p) by A1,PARTFUN1:def 6
.= p.(len p-'1) * q.(i+1-'(len p)) by A1,M;
hence thesis by M,A2;
end;
theorem
for R being degenerated Ring,
p being Polynomial of R
holds {i where i is Nat : p.i <> 0.R} = {}
proof
let R be degenerated Ring, p be Polynomial of R;
A:now let i be Nat;
thus p.i = p.i * 1.R .= p.i * 0.R by STRUCT_0:def 8 .= 0.R;
end;
set M = {i where i is Nat : p.i <> 0.R};
now assume B: M <> {};
let x be Element of M;
x in M by B;
then consider j being Nat such that H1: j = x & p.j <> 0.R;
thus contradiction by H1,A;
end;
hence thesis;
end;
theorem lemlp0:
for R being Ring,
p being Polynomial of R
holds p = 0_.(R) iff {i where i is Nat : p.i <> 0.R} = {}
proof
let R be Ring, p be Polynomial of R;
hereby assume AS: p = 0_.(R);
now assume {i where i is Nat : p.i <> 0.R} is non empty;
then consider x being object such that
H1: x in {i where i is Nat : p.i <> 0.R};
consider i being Nat such that H2: x = i & p.i <> 0.R by H1;
thus contradiction by AS,H2,FUNCOP_1:7,ORDINAL1:def 12;
end;
hence {i where i is Nat : p.i <> 0.R} = {};
end;
assume AS: {i where i is Nat : p.i <> 0.R} = {};
assume p <> 0_.(R);
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then reconsider k = len p - 1 as Element of NAT by INT_1:3;
reconsider k as Nat;
len p = k + 1;
then p.k <> 0.R by ALGSEQ_1:10;
then k in {i where i is Nat : p.i <> 0.R};
hence contradiction by AS;
end;
theorem lemlowp0:
for R being Ring,
p being Polynomial of R
holds min* {i where i is Nat : (p+0_.R).i <> 0.R}
= min* {i where i is Nat : p.i <> 0.R}
proof
let R be Ring, p be Polynomial of R;
now let o be object;
assume o in {i where i is Nat : p.i <> 0.R};
then consider i being Nat such that H1: o = i & p.i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cp = {i where i is Nat : p.i <> 0.R} as Subset of NAT
by TARSKI:def 3;
now let o be object;
assume o in {i where i is Nat : (p+0_.R).i <> 0.R};
then consider i being Nat such that H1: o = i & (p+0_.R).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cpq = {i where i is Nat : (p+0_.R).i <> 0.R} as Subset of NAT
by TARSKI:def 3;
per cases;
suppose cp is non empty;
then min* cp in cp by NAT_1:def 1;
then consider i being Nat such that H1: min* cp = i & p.i <> 0.R;
(p+0_.R).i = p.i + (0_.R).i by NORMSP_1:def 2
.= p.i + 0.R by ORDINAL1:def 12,FUNCOP_1:7
.= p.i;
then B: min* cp in cpq by H1;
now let k be Nat;
assume k in cpq;
then consider i being Nat such that C1: k = i & (p+0_.R).i <> 0.R;
now assume min* cp > k;
then C2: not(k in cp) by NAT_1:def 1;
(p+0_.R).k = p.k + (0_.R).k by NORMSP_1:def 2
.= p.k + 0.R by ORDINAL1:def 12,FUNCOP_1:7
.= 0.R by C2;
hence contradiction by C1;
end;
hence min* cp <= k;
end;
hence min*{i where i is Nat : (p+0_.R).i <> 0.R}
= min*{i where i is Nat : p.i <> 0.R} by B,NAT_1:def 1;
end;
suppose A: cp is empty;
then p = 0_.(R) by lemlp0;
hence min*{i where i is Nat : (p+0_.R).i <> 0.R}
= min*{i where i is Nat : p.i <> 0.R} by A,lemlp0,POLYNOM3:28;
end;
end;
lemlp1:
for R being non degenerated Ring, p being non zero Polynomial of R
holds {i where i is Nat : p.i <> 0.R} is non empty Subset of NAT
proof
let R be non degenerated Ring, p be non zero Polynomial of R;
A: now let o be object;
assume o in {i where i is Nat : p.i <> 0.R};
then consider i being Nat such that H: o = i & p.i <> 0.R;
thus o in NAT by H,ORDINAL1:def 12;
end;
p <> 0_.(R);
hence thesis by A,lemlp0,TARSKI:def 3;
end;
theorem lemlowp2:
for R being non degenerated Ring,
p being Polynomial of R holds
min* {i where i is Nat : (-p).i <> 0.R}
= min* {i where i is Nat : p.i <> 0.R}
proof
let R be non degenerated Ring, p be Polynomial of R;
per cases;
suppose p = 0_.(R);
then -p = p by HURWITZ:9;
hence thesis;
end;
suppose p <> 0_.(R);
then reconsider pp = p as non zero Polynomial of R by UPROOTS:def 5;
reconsider cp = {i where i is Nat : pp.i <> 0.R} as
non empty Subset of NAT by lemlp1;
min* cp in cp by NAT_1:def 1;
then consider j being Nat such that A0: j = min* cp & p.j <> 0.R;
now assume (-p).j = 0.R;
then A1: 0.R = -(p.j) by BHSP_1:44;
p.j = -(-p.j) .= 0.R by A1;
hence contradiction by A0;
end;
then A: j in {i where i is Nat : (-p).i <> 0.R};
now let o be object;
assume o in {i where i is Nat : (-p).i <> 0.R};
then consider i being Nat such that H1: o = i & (-p).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cmp = {i where i is Nat : (-p).i <> 0.R} as
non empty Subset of NAT by A,TARSKI:def 3;
now let k be Nat;
assume k in {i where i is Nat : (-p).i <> 0.R};
then consider i being Nat such that A3: k = i & (-p).i <> 0.R;
now assume p.i = 0.R;
then -(p.i) = 0.R;
hence (-p).i = 0.R by BHSP_1:44;
end;
then i in cp by A3;
hence j <= k by A3,A0,NAT_1:def 1;
end;
then j = min* cmp by A,NAT_1:def 1;
hence thesis by A0;
end;
end;
theorem lemlowp1a1:
for R being non degenerated Ring,
p,q being non zero Polynomial of R
st min* {i where i is Nat : p.i <> 0.R} > min* {i where i is Nat : q.i <> 0.R}
holds min* {i where i is Nat : (p+q).i <> 0.R} =
min* {i where i is Nat : q.i <> 0.R}
proof
let R be non degenerated Ring;
let p,q be non zero Polynomial of R;
assume AS1: min*{i where i is Nat : p.i<>0.R} >
min*{i where i is Nat : q.i<>0.R};
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R} as non empty Subset of NAT
by lemlp1;
now let o be object;
assume o in {i where i is Nat : (p+q).i <> 0.R};
then consider i being Nat such that H1: o = i & (p+q).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cpq = {i where i is Nat : (p+q).i <> 0.R} as Subset of NAT
by TARSKI:def 3;
not( (min* cq) in cp ) by AS1,NAT_1:def 1;
then p.(min* cq) = 0.R;
then A: (p+q).(min* cq) = 0.R + q.(min* cq) by NORMSP_1:def 2;
min* cq in cq by NAT_1:def 1;
then consider u being Nat such that H1: u = min* cq & q.u <> 0.R;
B: min* cq in cpq by A,H1;
then reconsider cpq as non empty Subset of NAT;
now let k be Nat;
assume k in cpq;
then consider v being Nat such that H2: v = k & (p+q).v <> 0.R;
now let j be Nat;
assume D0: j < min* cq;
D1: now assume q.j <> 0.R;
then j in cq;
hence contradiction by D0,NAT_1:def 1;
end;
now assume p.j <> 0.R;
then j in cp;
then j >= min* cp by NAT_1:def 1;
hence contradiction by D0,AS1,XXREAL_0:2;
end;
hence (p+q).j = 0.R + q.j by NORMSP_1:def 2
.= 0.R by D1;
end;
hence min* cq <= k by H2;
end;
hence thesis by B,NAT_1:def 1;
end;
theorem lemlowp1a2:
for R being non degenerated Ring,
p,q being non zero Polynomial of R
st p + q <> 0_.(R) &
min* {i where i is Nat : p.i <> 0.R} = min* {i where i is Nat : q.i <> 0.R}
holds min* {i where i is Nat : (p+q).i <> 0.R} >=
min* {i where i is Nat : p.i <> 0.R}
proof
let R be non degenerated Ring, p,q be non zero Polynomial of R;
assume XX: p + q <> 0_.(R) & min* {i where i is Nat : p.i <> 0.R} =
min* {i where i is Nat : q.i <> 0.R};
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R} as non empty Subset of NAT
by lemlp1;
now let o be object;
assume o in {i where i is Nat : (p+q).i <> 0.R};
then consider i being Nat such that H1: o = i & (p+q).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cpq = {i where i is Nat : (p+q).i <> 0.R}
as non empty Subset of NAT by lemlp0,XX,TARSKI:def 3;
min* cpq in cpq by NAT_1:def 1;
then consider u being Nat such that H1: u = min* cpq & (p+q).u <> 0.R;
now let j be Nat;
assume D0: j < min* cp;
D1a: now assume p.j <> 0.R;
then j in cp;
hence contradiction by D0,NAT_1:def 1;
end;
now assume q.j <> 0.R;
then j in cq;
hence contradiction by XX,D0,NAT_1:def 1;
end;
hence (p+q).j = p.j + 0.R by NORMSP_1:def 2 .= 0.R by D1a;
end;
hence thesis by H1;
end;
theorem lemlowp1b:
for R being non degenerated Ring,
p,q being non zero Polynomial of R
st p.(min* {i where i is Nat : p.i <> 0.R}) +
q.(min* {i where i is Nat : q.i <> 0.R}) <> 0.R
holds min* {i where i is Nat : (p+q).i <> 0.R} =
min( min* {i where i is Nat : p.i <> 0.R},
min* {i where i is Nat : q.i <> 0.R})
proof
let R be non degenerated Ring, p,q be non zero Polynomial of R;
assume XX: p.(min* {i where i is Nat : p.i <> 0.R}) +
q.(min* {i where i is Nat : q.i <> 0.R}) <> 0.R;
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R} as non empty Subset of NAT
by lemlp1;
now let o be object;
assume o in {i where i is Nat : (p+q).i <> 0.R};
then consider i being Nat such that H1: o = i & (p+q).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cpq = {i where i is Nat : (p+q).i <> 0.R}
as Subset of NAT by TARSKI:def 3;
per cases by XXREAL_0:1;
suppose A: min* cp > min* cq;
then min* cpq = min* cq by lemlowp1a1;
hence thesis by A,XXREAL_0:def 9;
end;
suppose A: min* cp < min* cq;
then min* cpq = min* cp by lemlowp1a1;
hence thesis by A,XXREAL_0:def 9;
end;
suppose A: min* cp = min* cq;
then (p+q).(min* cp) <> 0.R by XX,NORMSP_1:def 2;
then D1: min* cp in cpq;
then p + q <> 0_.(R) by lemlp0;
then D4: min* cpq >= min* cp by A,lemlowp1a2;
not(min* cpq > min* cp) by D1,NAT_1:def 1;
hence thesis by A,D4,XXREAL_0:1;
end;
end;
theorem lemlowp3a:
for R being non degenerated Ring,
p,q being non zero Polynomial of R
st p *' q <> 0_.(R)
holds min* {i where i is Nat : (p*'q).i <> 0.R} >=
min* {i where i is Nat : p.i <> 0.R} +
min* {i where i is Nat : q.i <> 0.R}
proof
let R be non degenerated Ring, p,q be non zero Polynomial of R;
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R} as
non empty Subset of NAT by lemlp1;
assume p *' q <> 0_.(R);
then p *' q is non zero;
then reconsider cpq = {i where i is Nat : (p*'q).i <> 0.R} as
non empty Subset of NAT by lemlp1;
set m = min* cp + min* cq;
A: min* cpq in cpq by NAT_1:def 1;
now let z1 be Nat;
assume z1 in cpq;
then consider w being Nat such that H1: w = z1 & (p*'q).w <> 0.R;
reconsider z = z1 as Element of NAT by ORDINAL1:def 12;
consider r1 being FinSequence of the carrier of R such that
R: len r1 = z+1 & (p*'q).z = Sum r1 &
for k be Element of NAT st k in dom r1 holds r1.k = p.(k-'1) * q.(z+1-'k)
by POLYNOM3:def 9;
1 <= z + 1 by NAT_1:11;
then A1: 1 in dom r1 by FINSEQ_3:25,R;
now assume AA1: z < m;
F: for k being Nat st k in dom r1 holds p.(k-'1) = 0.R or q.(z+1-'k) = 0.R
proof
let k be Nat;
assume k in dom r1;
then EF: 1 <= k & k <= len r1 by FINSEQ_3:25;
per cases;
suppose AA0: k-'1 >= min* cp;
AA2: k -' 1 = k - 1 by EF,XREAL_0:def 2;
z + 1 - k in NAT by INT_1:5,R,EF;
then z + 1 -' k = z + 1 - k by XREAL_0:def 2;
then (k -' 1) + (z + 1 -' k) < min* cp + min* cq by AA1,AA2;
then S: z+1-'k < min* cq by AA0,XREAL_1:7;
now assume q.(z+1-'k) <> 0.R;
then z+1-'k in cq;
hence contradiction by S,NAT_1:def 1;
end;
hence thesis;
end;
suppose S: k-'1 < min* cp;
now assume p.(k-'1) <> 0.R;
then k-'1 in cp;
hence contradiction by S,NAT_1:def 1;
end;
hence thesis;
end;
end;
now let k be Element of NAT;
assume E: k in dom r1 & k <> 1;
per cases by F,E;
suppose p.(k-'1) = 0.R;
then r1.k = 0.R * q.(z+1-'k) by E,R;
hence r1/.k = 0.R by E,PARTFUN1:def 6;
end;
suppose q.(z+1-'k) = 0.R;
then r1.k = p.(k-'1) * 0.R by E,R;
hence r1/.k = 0.R by E,PARTFUN1:def 6;
end;
end;
then T: Sum r1 = r1/.1 by A1,POLYNOM2:3
.= r1.1 by A1,PARTFUN1:def 6
.= p.(1-'1) * q.(z+1-'1) by A1,R;
now per cases by A1,F;
suppose p.(1-'1) = 0.R;
hence Sum r1 = 0.R by T;
end;
suppose q.(z+1-'1) = 0.R;
hence Sum r1 = 0.R by T;
end;
end;
hence contradiction by H1,R;
end;
hence z1 >= m;
end;
hence thesis by A;
end;
theorem lemlowp3b:
for R being domRing,
p,q being non zero Polynomial of R
holds min* {i where i is Nat : (p*'q).i <> 0.R} =
min* {i where i is Nat : p.i <> 0.R} +
min* {i where i is Nat : q.i <> 0.R}
proof
let R be domRing, p,q be non zero Polynomial of R;
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R},
cpq = {i where i is Nat : (p*'q).i <> 0.R}
as non empty Subset of NAT by lemlp1;
set m = min* cp + min* cq;
consider r being FinSequence of the carrier of R such that
M: len r = m+1 & (p*'q).m = Sum r &
for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(m+1-'k)
by POLYNOM3:def 9;
B1: 1 <= min* cp + 1 by NAT_1:11;
min* cp + 1 <= (min* cp + 1) + min* cq by NAT_1:11;
then min* cp + 1 in Seg(m+1) by B1,FINSEQ_1:1;
then A1: min* cp + 1 in dom r by M,FINSEQ_1:def 3;
A2: (min* cp + 1) - 1 >= 0;
A4: m+1-'(min* cp + 1) = m+1-(min* cp + 1) by XREAL_0:def 2;
now let k be Element of NAT;
assume E: k in dom r & k <> min* cp + 1;
then EE: 1 <= k <= m + 1 by M,FINSEQ_3:25;
per cases by E,XXREAL_0:1;
suppose E1: k < min* cp + 1;
reconsider k1 = k - 1 as Element of NAT by EE,INT_1:3;
E4: k -' 1 = k - 1 by EE,XREAL_0:def 2;
then E3: k -' 1 < (min* cp + 1) - 1 by E1,XREAL_1:9;
now assume p.k1 <> 0.R;
then k1 in cp;
hence contradiction by E3,E4,NAT_1:def 1;
end;
then r.k = 0.R * q.(m+1-'k) by E4,E,M;
hence r/.k = 0.R by E,PARTFUN1:def 6;
end;
suppose k > min* cp + 1;
then E1: m + 1 - k < m + 1 - (min* cp + 1) by XREAL_1:10;
m + 1 - k in NAT by EE,INT_1:5;
then E3: m + 1 -' k < min* cq by E1,XREAL_0:def 2;
now assume q.(m+1-'k) <> 0.R;
then m+1-'k in cq;
hence contradiction by E3,NAT_1:def 1;
end;
then r.k = p.(k-'1) * 0.R by E,M;
hence r/.k = 0.R by E,PARTFUN1:def 6;
end;
end;
then X: Sum r = r/.(min* cp + 1) by A1,POLYNOM2:3
.= r.(min* cp + 1) by A1,PARTFUN1:def 6
.= p.((min* cp + 1)-'1) * q.(m+1-'(min* cp + 1)) by A1,M
.= p.(min* cp) * q.(min* cq) by A4,A2,XREAL_0:def 2;
min* cp in cp by NAT_1:def 1;
then consider u being Nat such that H1: u = min* cp & p.u <> 0.R;
min* cq in cq by NAT_1:def 1;
then consider v being Nat such that H2: v = min* cq & q.v <> 0.R;
p.u * q.v <> 0.R by H1,H2,VECTSP_2:def 1;
then m in {i where i is Nat : (p*'q).i <> 0.R} by H1,H2,X,M;
then C1: min* cpq <= m by NAT_1:def 1;
p *' q <> 0_.(R);
then min* cpq >= m by lemlowp3a;
hence thesis by C1,XXREAL_0:1;
end;
begin :: Preliminaries
definition
let L be non empty multLoopStr;
let S be Subset of L;
attr S is mult-closed means
for s1,s2 being Element of L st s1 in S & s2 in S holds s1 * s2 in S;
end;
definition ::: compare GROUP_1A
let L be non empty addLoopStr;
let S be Subset of L;
func -S -> Subset of L equals
{ -s where s is Element of L : s in S };
coherence
proof
set M = {-s where s is Element of L : s in S};
now let x be object;
assume x in M;
then consider s being Element of L such that
A1: x = -s & s in S;
thus x in the carrier of L by A1;
end;
then M c= the carrier of L;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let S be Subset of L;
reduce -(-S) to S;
reducibility
proof
A: now let x be object;
assume x in --S;
then consider a being Element of L such that A: x = -a & a in -S;
consider b being Element of L such that B: -b = a & b in S by A;
thus x in S by A,B;
end;
now let x be object;
assume AS: x in S;
then reconsider y = x as Element of L;
consider a being Element of L such that A: -y = -a & a in S by AS;
consider b being Element of L such that C: -b = -a & b in S by A;
B: -a in { - s where s is Element of L : s in S } by A;
y = --b by A,C;
hence x in --S by C,B;
end;
hence thesis by A,TARSKI:2;
end;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for S being Subset of L
for a being Element of L holds a in S iff -a in -S
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let S be Subset of L, a be Element of L;
now assume -a in -S;
then -- a in --S;
hence a in S;
end;
hence thesis;
end;
theorem min1:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for S1,S2 being Subset of L holds -(S1 /\ S2) = (-S1) /\ (-S2)
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr, S1,S2 be Subset of L;
A: now let o be object;
assume o in -(S1 /\ S2);
then consider s being Element of L such that A: -s = o & s in S1 /\ S2;
s in S1 & s in S2 by A,XBOOLE_0:def 4;
then -s in -S1 & -s in -S2;
hence o in (-S1) /\ (-S2) by A,XBOOLE_0:def 4;
end;
now let o be object;
assume o in (-S1) /\ (-S2);
then A: o in -S1 & o in -S2 by XBOOLE_0:def 4;
then consider s1 being Element of L such that B: -s1 = o & s1 in S1;
consider s2 being Element of L such that C: -s2 = o & s2 in S2 by A;
s1 = -(-s2) by B,C .= s2;
then s1 in S1 /\ S2 by B,C,XBOOLE_0:def 4;
hence o in -(S1 /\ S2) by B;
end;
hence thesis by A,TARSKI:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for S1,S2 being Subset of L holds -(S1 \/ S2) = (-S1) \/ (-S2)
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr, S1,S2 be Subset of L;
A: now let o be object;
assume o in -(S1 \/ S2);
then consider s being Element of L such that A: -s = o & s in S1 \/ S2;
s in S1 or s in S2 by A,XBOOLE_0:def 3;
then -s in -S1 or -s in -S2;
hence o in (-S1) \/ (-S2) by A,XBOOLE_0:def 3;
end;
now let o be object;
assume A: o in (-S1) \/ (-S2);
per cases by A,XBOOLE_0:def 3;
suppose o in -S1;
then consider s1 being Element of L such that B: -s1 = o & s1 in S1;
s1 in S1 \/ S2 by B,XBOOLE_0:def 3;
hence o in -(S1 \/ S2) by B;
end;
suppose o in -S2;
then consider s1 being Element of L such that B: -s1 = o & s1 in S2;
s1 in S1 \/ S2 by B,XBOOLE_0:def 3;
hence o in -(S1 \/ S2) by B;
end;
end;
hence thesis by A,TARSKI:2;
end;
definition
let L be non empty addLoopStr;
let S be Subset of L;
attr S is negative-disjoint means :defneg:
S /\ (-S) = {0.L};
end;
definition
let L be non empty addLoopStr;
let S be Subset of L;
attr S is spanning means :defsp:
S \/ (-S) = the carrier of L;
end;
begin :: Squares and Sums of Squares
notation
let R be Ring;
let a be Element of R;
synonym a is square for a is being_a_square;
end;
registration
let R be Ring;
cluster 0.R -> square;
coherence
proof
0.R = (0.R)^2;
hence thesis;
end;
cluster 1.R -> square;
coherence
proof
1.R = (1.R)^2;
hence thesis;
end;
end;
registration
let R be Ring;
cluster square for Element of R;
existence
proof
take 1.R;
thus thesis;
end;
end;
definition ::: should be unified with O_RING_1; definition there should be
::: tuned accordingly
let R be Ring;
let a be Element of R;
attr a is sum_of_squares means
ex f being FinSequence of R st Sum f = a &
for i being Nat st i in dom f ex a being Element of R st f.i = a^2;
end;
AS0:
for R being Ring
for a being Element of R st a is square holds a is sum_of_squares
proof
let R be Ring, a be Element of R;
assume AS: a is square;
set f = <*a*>;
A: Sum f = a by RLVECT_1:44;
now let i be Nat;
assume i in dom f;
then i in {1} by FINSEQ_1:2,FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
hence ex b being Element of R st f.i = b^2 by AS;
end;
hence thesis by A;
end;
registration
let R be Ring;
cluster square -> sum_of_squares for Element of R;
coherence by AS0;
end;
S1:
for R being Ring
for a,b being Element of R
st a is sum_of_squares & b is sum_of_squares holds a + b is sum_of_squares
proof
let R be Ring, a,b be Element of R;
assume AS: a is sum_of_squares & b is sum_of_squares;
then consider f being FinSequence of R such that A: Sum f = a &
for i being Nat st i in dom f ex a being Element of R st f.i = a^2;
consider g being FinSequence of R such that B: Sum g = b &
for i being Nat st i in dom g ex a being Element of R st g.i = a^2 by AS;
set t = f ^ g;
C: Sum t = a + b by A,B,RLVECT_1:41;
now let i be Nat;
assume D: i in dom t;
per cases by D,FINSEQ_1:25;
suppose E: i in dom f;
then t.i = f.i by FINSEQ_1:def 7;
hence ex x being Element of R st t.i = x^2 by E,A;
end;
suppose ex n being Nat st n in dom g & i = len f + n;
then consider n being Nat such that E: n in dom g & i = len f + n;
t.i = g.n by E,FINSEQ_1:def 7;
hence ex x being Element of R st t.i = x^2 by E,B;
end;
end;
hence thesis by C;
end;
S2:
for R being commutative Ring
for a,b being Element of R
st a is square & b is sum_of_squares holds a * b is sum_of_squares
proof
let R be commutative Ring, a,b be Element of R;
assume AS: a is square & b is sum_of_squares;
then consider f being FinSequence of R such that A: Sum f = b &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2;
set g = a * f;
B: Sum g = a * b by A,BINOM:4;
now let i be Nat;
assume C: i in dom g;
then D: i in dom f by POLYNOM1:def 1;
E: g.i = g/.i by C,PARTFUN1:def 6
.= a * (f/.i) by D,POLYNOM1:def 1;
consider x being Element of R such that F: f.i = x^2 by D,A;
consider y being Element of R such that G: a = y^2 by AS;
g.i = (y^2) * x^2 by E,G,D,F,PARTFUN1:def 6
.= x*(x * (y*y)) by GROUP_1:def 3
.= x*(x * y*y) by GROUP_1:def 3
.= (x*y)^2 by GROUP_1:def 3;
hence ex z being Element of R st g.i = z^2;
end;
hence thesis by B;
end;
SM1:
for R being commutative Ring
for a,b being Element of R
st a is square & b is square holds a * b is square
proof
let R be commutative Ring, a,b be Element of R;
assume AS: a is square & b is square;
then consider x being Element of R such that A: a = x^2;
consider y being Element of R such that B: b = y^2 by AS;
a * b = x * (x * (y * y)) by GROUP_1:def 3,A,B
.= x * (y * (x * y)) by GROUP_1:def 3
.= (x*y)^2 by GROUP_1:def 3;
hence thesis;
end;
S3:
for R being commutative Ring
for a,b being Element of R
st a is sum_of_squares & b is sum_of_squares holds a * b is sum_of_squares
proof
let R be commutative Ring, a,b be Element of R;
assume AS: a is sum_of_squares & b is sum_of_squares;
defpred P[Nat] means
for f being FinSequence of R st len f = $1 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2
holds a * Sum f is sum_of_squares;
now let f be FinSequence of R;
assume len f = 0 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2;
then f = <*>(the carrier of R);
then Sum f = 0.R by RLVECT_1:43;
hence a * Sum f is sum_of_squares;
end;
then A: P[0];
B: now let k be Nat;
assume IV: P[k];
now let f be FinSequence of R;
assume B0: len f = k+1 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2;
then f <> {};
then consider g being FinSequence, x being object such that
B1: f = g^<*x*> by FINSEQ_1:46;
reconsider g, h = <*x*> as FinSequence of R by B1,FINSEQ_1:36;
len h = 1 by FINSEQ_1:39;
then B2: len f = len g + 1 by B1,FINSEQ_1:22;
now let i be Nat;
assume C1: i in dom g;
then C2: g.i = f.i by B1,FINSEQ_1:def 7;
dom g c= dom f by B1,FINSEQ_1:26;
hence ex x being Element of R st g.i = x^2 by B0,C2,C1;
end;
then B3: a * Sum g is sum_of_squares by IV,B2,B0;
C2: dom f = Seg(k+1) by B0,FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
B5: x = f.(k+1) by B0,B2,B1,FINSEQ_1:42;
then reconsider x as Element of R by B4,C2,FINSEQ_1:1,FINSEQ_2:11;
consider z being Element of R such that
B6: x = z^2 by B0,B4,B5,C2,FINSEQ_1:1;
x is square by B6;
then B7: x * a is sum_of_squares by S2,AS;
(a * Sum g) + (a * x)
= a * (Sum g + x) by VECTSP_1:def 3
.= a * (Sum g + Sum <*x*>) by RLVECT_1:44
.= a * Sum f by B1,RLVECT_1:41;
hence a * Sum f is sum_of_squares by B7,B3,S1;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider f being FinSequence of R such that H: Sum f = b &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2 by AS;
consider k being Nat such that K: len f = k;
thus thesis by I,H,K;
end;
registration
let R be commutative Ring;
let a,b be square Element of R;
cluster a * b -> square;
coherence by SM1;
end;
registration
let R be Ring;
let a,b be sum_of_squares Element of R;
cluster a + b -> sum_of_squares;
coherence by S1;
end;
registration
let R be commutative Ring;
let a,b be sum_of_squares Element of R;
cluster a * b -> sum_of_squares;
coherence by S3;
end;
definition
let R be Ring;
func Squares_of R -> Subset of R equals
{ a where a is Element of R : a is square };
coherence
proof
set M = {a where a is Element of R : a is square};
now let x be object;
assume x in M;
then consider a being Element of R such that
A1: x = a & a is square;
thus x in the carrier of R by A1;
end;
then M c= the carrier of R;
hence thesis;
end;
func Quadratic_Sums_of R -> Subset of R equals
{ a where a is Element of R : a is sum_of_squares };
coherence
proof
set M = {a where a is Element of R : a is sum_of_squares};
now let x be object;
assume x in M;
then consider a being Element of R such that
A1: x = a & a is sum_of_squares;
thus x in the carrier of R by A1;
end;
then M c= the carrier of R;
hence thesis;
end;
end;
notation
let R be Ring;
synonym SQ R for Squares_of R;
synonym QS R for Quadratic_Sums_of R;
end;
SQ0: for R being Ring holds 0.R in SQ R;
QS0: for R being Ring holds 0.R in QS R;
registration
let R be Ring;
cluster SQ R -> non empty;
coherence by SQ0;
cluster QS R -> non empty;
coherence by QS0;
end;
definition
let R be Ring;
let S be Subset of R;
attr S is with_squares means
SQ R c= S;
attr S is with_sums_of_squares means
QS R c= S;
end;
registration
let R be Ring;
cluster with_squares for Subset of R;
existence
proof
take SQ R;
thus thesis;
end;
cluster with_sums_of_squares for Subset of R;
existence
proof
take QS R;
thus thesis;
end;
end;
registration
let R be Ring;
cluster with_squares -> non empty for Subset of R;
coherence;
cluster with_sums_of_squares -> non empty for Subset of R;
coherence;
end;
registration
let R be Ring;
cluster with_sums_of_squares -> with_squares for Subset of R;
coherence
proof
let S be Subset of R;
assume AS: S is with_sums_of_squares;
SQ R c= S
proof let o be object;
assume o in SQ R;
then consider a being Element of R such that A: o = a & a is square;
a in QS R by A;
hence o in S by A,AS;
end;
hence thesis;
end;
cluster with_squares add-closed -> with_sums_of_squares for Subset of R;
coherence
proof
let S be Subset of R;
assume AS: S is with_squares add-closed;
defpred P[Nat] means
for f being FinSequence of R st len f = $1 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2
holds Sum f in S;
now let f be FinSequence of R;
assume len f = 0 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2;
then f = <*>(the carrier of R);
then Sum f = 0.R by RLVECT_1:43;
then Sum f in SQ R;
hence Sum f in S by AS;
end;
then A: P[0];
B: now let k be Nat;
assume IV: P[k];
now let f be FinSequence of R;
assume B0: len f = k+1 &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2;
then f <> {};
then consider g being FinSequence, x being object such that
B1: f = g^<*x*> by FINSEQ_1:46;
reconsider g, h = <*x*> as FinSequence of R by B1,FINSEQ_1:36;
len h = 1 by FINSEQ_1:39;
then B2: len f = len g + 1 by B1,FINSEQ_1:22;
now let i be Nat;
assume C1: i in dom g;
then C2: g.i = f.i by B1,FINSEQ_1:def 7;
dom g c= dom f by B1,FINSEQ_1:26;
hence ex x being Element of R st g.i = x^2 by B0,C2,C1;
end;
then B3: Sum g in S by IV,B2,B0;
C2: dom f = Seg(k+1) by B0,FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
B5: x = f.(k+1) by B0,B2,B1,FINSEQ_1:42;
then reconsider x as Element of R by B4,C2,FINSEQ_1:1,FINSEQ_2:11;
consider z being Element of R such that
B6: x = z^2 by B0,B4,B5,C2,FINSEQ_1:1;
x is square by B6;
then B7: x in SQ R;
Sum g + x = Sum g + Sum <*x*> by RLVECT_1:44
.= Sum f by B1,RLVECT_1:41;
hence Sum f in S by B7,B3,AS;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
now let o be object;
assume o in QS R;
then consider a being Element of R such that A: o = a & a is sum_of_squares;
consider f being FinSequence of R such that B: Sum f = o &
for i being Nat st i in dom f ex x being Element of R st f.i = x^2 by A;
consider n being Nat such that H: len f = n;
thus o in S by H,B,I;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let R be Ring;
cluster SQ R -> with_squares;
coherence;
cluster QS R -> with_sums_of_squares;
coherence;
end;
theorem
for R being Ring holds 0.R in SQ R & 1.R in SQ R;
theorem
for R being Ring holds SQ R c= QS R
proof
let R be Ring;
let o be object;
assume o in SQ R;
then consider a being Element of R such that A: o = a & a is square;
thus o in QS R by A;
end;
registration
let R be Ring;
cluster QS R -> add-closed;
coherence
proof
let x,y be Element of R;
assume AS: x in QS R & y in QS R;
then consider a being Element of R such that
A: x = a & a is sum_of_squares;
consider b being Element of R such that
B: y = b & b is sum_of_squares by AS;
thus x + y in QS R by A,B;
end;
end;
registration
let R be commutative Ring;
cluster QS R -> mult-closed;
coherence
proof
let x,y be Element of R;
assume AS: x in QS R & y in QS R;
then consider a being Element of R such that
A: x = a & a is sum_of_squares;
consider b being Element of R such that
B: y = b & b is sum_of_squares by AS;
thus x * y in QS R by A,B;
end;
end;
lemminus:
for R be Ring, S be Subring of R,
a be Element of R, b be Element of S st a = b holds -a = -b
proof
let R be Ring, S be Subring of R,
a be Element of R, b be Element of S;
assume AS: a = b;
the carrier of S c= the carrier of R by C0SP1:def 3; then
reconsider c = -b as Element of R;
dom(the addF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then A6: [c,a] in dom(the addF of S) by AS,ZFMISC_1:def 2;
c + a = ((the addF of R)||(the carrier of S)).(c,a) by A6,FUNCT_1:49
.= (-b) + b by AS,C0SP1:def 3
.= 0.S by RLVECT_1:5
.= 0.R by C0SP1:def 3
.= (-a) + a by RLVECT_1:5;
hence thesis by RLVECT_1:8;
end;
lemminus1:
for R be Ring, S be Subring of R,
S1 be Subset of R, S2 be Subset of S st S1 = S2 holds -S1 = -S2
proof
let R be Ring, S be Subring of R,
S1 be Subset of R, S2 be Subset of S;
assume AS: S1 = S2;
hereby let o be object;
assume o in -S1;
then consider a being Element of R such that A1: -a = o & a in S1;
reconsider b = a as Element of S by A1,AS;
-b in -S2 by A1,AS;
hence o in -S2 by A1,lemminus;
end;
let o be object;
assume o in -S2;
then consider a being Element of S such that A1: -a = o & a in S2;
reconsider b = a as Element of R by A1,AS;
-b in -S1 by A1,AS;
hence o in -S1 by A1,lemminus;
end;
lemsum:
for R be Ring, S be Subring of R,
f be FinSequence of R, g be FinSequence of S st f = g holds Sum f = Sum g
proof
let R be Ring, S be Subring of R,
f be FinSequence of R, g be FinSequence of S;
assume AS: f = g;
defpred P[Nat] means
for f be FinSequence of R, g be FinSequence of S
st f = g & len f = $1 holds Sum f = Sum g;
now let f be FinSequence of R, g be FinSequence of S;
assume f = g & len f = 0;
then A: f = <*>(the carrier of R) & g = <*>(the carrier of S);
hence Sum f = 0.R by RLVECT_1:43
.= 0.S by C0SP1:def 3 .= Sum g by A,RLVECT_1:43;
end;
then A: P[0];
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
B: now let k be Nat;
assume IA: P[k];
now let f be FinSequence of R, g be FinSequence of S;
assume B0: f = g & len f = k+1;
then g <> {};
then consider h being FinSequence, x being object such that
B1: g = h^<*x*> by FINSEQ_1:46;
reconsider h, o = <*x*> as FinSequence of S by B1,FINSEQ_1:36;
len o = 1 by FINSEQ_1:39;
then B2: len g = len h + 1 by B1,FINSEQ_1:22;
C2: dom g = Seg(k+1) by B0,FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
x = g.(k+1) by B0,B2,B1,FINSEQ_1:42;
then reconsider x as Element of S by B4,C2,FINSEQ_1:1,FINSEQ_2:11;
reconsider y = x as Element of R by AS4;
rng h c= the carrier of R by AS4;
then reconsider hh = h as FinSequence of R by FINSEQ_1:def 4;
rng o c= the carrier of R by AS4;
then reconsider oo = o as FinSequence of R by FINSEQ_1:def 4;
dom(the addF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then B7: [Sum h,Sum o] in dom(the addF of S);
B8: Sum o = y by RLVECT_1:44 .= Sum oo by RLVECT_1:44;
thus Sum f = Sum hh + Sum oo by B0,B1,RLVECT_1:41
.= (the addF of R).(Sum h,Sum o) by B8,B0,B2,IA
.= ((the addF of R)||(the carrier of S)).(Sum h,Sum o)
by B7,FUNCT_1:49
.= Sum h + Sum o by C0SP1:def 3
.= Sum g by B1,RLVECT_1:41;
end;
hence P[k+1];
end;
I: for k be Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that H: len f = n;
thus thesis by AS,I,H;
end;
theorem SQsub:
for R being Ring
for S being Subring of R holds SQ S c= SQ R
proof
let R be Ring, S be Subring of R;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
let o be object;
assume o in SQ S;
then consider a being Element of S such that A: o = a & a is square;
consider b being Element of S such that B: a = b^2 by A;
reconsider a1 = a, b1 = b as Element of R by AS4;
dom(the multF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then B6: [b,b] in dom(the multF of S);
a1 = ((the multF of R)||(the carrier of S)).(b,b) by C0SP1:def 3,B
.= b1^2 by B6,FUNCT_1:49;
then a1 is square;
hence o in SQ R by A;
end;
theorem
for R being Ring
for S being Subring of R holds QS S c= QS R
proof
let R be Ring, S be Subring of R;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
let o be object;
assume o in QS S;
then consider a being Element of S such that
D2: a = o & a is sum_of_squares;
consider f being FinSequence of S such that D3: Sum f = a &
for i being Nat st i in dom f ex a being Element of S st f.i = a^2 by D2;
reconsider a1 = a as Element of R by AS4;
rng f c= the carrier of R by AS4;
then reconsider g = f as FinSequence of R by FINSEQ_1:def 4;
D9: Sum g = Sum f by lemsum;
now let i be Nat;
assume i in dom g;
then consider a being Element of S such that E1: f.i = a^2 by D3;
reconsider a1 = a as Element of R by AS4;
dom(the multF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then B6: [a,a] in dom(the multF of S);
a1^2 = ((the multF of R)||(the carrier of S)).(a,a) by B6,FUNCT_1:49
.= a^2 by C0SP1:def 3;
hence ex a being Element of R st g.i = a^2 by E1;
end;
then a1 is sum_of_squares by D3,D9;
hence o in QS R by D2;
end;
begin :: Positive Cones and Orderings
definition
let R be Ring,
S be Subset of R;
attr S is prepositive_cone means :defppc:
S + S c= S & S * S c= S & S /\ (-S) = {0.R} & SQ R c= S;
attr S is positive_cone means :defpc:
S + S c= S & S * S c= S & S /\ (-S) = {0.R} & S \/ (-S) = the carrier of R;
end;
registration
let R be Ring;
cluster prepositive_cone -> non empty for Subset of R;
coherence;
cluster positive_cone -> non empty for Subset of R;
coherence;
end;
registration
let R be Ring;
cluster prepositive_cone -> add-closed mult-closed negative-disjoint
with_squares for Subset of R;
coherence
proof
let S be Subset of R; assume AS: S is prepositive_cone;
thus S is add-closed
proof
let x,y be Element of R;
assume x in S & y in S;
then x+y in {a+b where a,b is Element of R : a in S & b in S};
then x + y in S + S by IDEAL_1:def 19;
hence x+y in S by AS;
end;
thus S is mult-closed
proof
let x,y be Element of R;
assume x in S & y in S;
then x * y in S * S;
hence x*y in S by AS;
end;
thus S is negative-disjoint with_squares by AS;
end;
cluster add-closed mult-closed negative-disjoint with_squares
-> prepositive_cone for Subset of R;
coherence
proof
let S be Subset of R;
assume AS: S is add-closed mult-closed negative-disjoint with_squares;
B: S + S c= S
proof let x be object;
assume x in S + S; then
x in {a+b where a,b is Element of R : a in S & b in S} by IDEAL_1:def 19;
then consider a,b being Element of R such that
A1: x = a + b & a in S & b in S;
thus x in S by AS,A1;
end;
S * S c= S
proof let x be object;
assume x in S * S;
then consider a,b being Element of R such that
A1: x = a * b & a in S & b in S;
thus x in S by A1,AS;
end;
hence thesis by AS,B;
end;
end;
registration
let R be Ring;
cluster positive_cone ->
add-closed mult-closed negative-disjoint spanning for Subset of R;
coherence
proof
let S be Subset of R; assume AS: S is positive_cone;
thus S is add-closed
proof
let x,y be Element of R;
assume x in S & y in S;
then x+y in {a+b where a,b is Element of R : a in S & b in S};
then x + y in S + S by IDEAL_1:def 19;
hence x+y in S by AS;
end;
thus S is mult-closed
proof
let x,y be Element of R;
assume x in S & y in S;
then x * y in S * S;
hence x*y in S by AS;
end;
thus S is negative-disjoint spanning by AS;
end;
cluster add-closed mult-closed negative-disjoint spanning
-> positive_cone for Subset of R;
coherence
proof
let S be Subset of R;
assume AS: S is add-closed mult-closed negative-disjoint spanning;
B: S + S c= S
proof let x be object;
assume x in S + S; then
x in {a+b where a,b is Element of R : a in S & b in S} by IDEAL_1:def 19;
then consider a,b being Element of R such that
A1: x = a + b & a in S & b in S;
thus x in S by AS,A1;
end;
S * S c= S
proof let x be object;
assume x in S * S;
then consider a,b being Element of R such that
A1: x = a * b & a in S & b in S;
thus x in S by A1,AS;
end;
hence thesis by AS,B;
end;
end;
registration
let R be Ring;
cluster positive_cone -> prepositive_cone for Subset of R;
coherence
proof
let P be Subset of R;
assume AS: P is positive_cone;
SQ R c= P
proof let o be object;
assume o in SQ R;
then consider a being Element of R such that A: o = a & a is square;
consider b being Element of R such that B: a = b^2 by A;
per cases by AS,XBOOLE_0:def 3;
suppose b in P;
then b * b in {x*y where x,y is Element of R : x in P & y in P};
hence o in P by A,B,AS;
end;
suppose b in -P;
then consider b1 being Element of R such that D: -b1 = b & b1 in P;
E: b1 * b1 in {x*y where x,y is Element of R : x in P & y in P} by D;
b1 * b1 = b * b by D,VECTSP_1:10;
hence o in P by E,B,A,AS;
end;
end;
hence thesis by AS;
end;
end;
theorem X1:
for F being Field
for S being Subset of F st S * S c= S & SQ F c= S
holds S /\ (-S) = {0.F} iff not -1.F in S
proof
let R be Field, S be Subset of R;
assume AS: S * S c= S & SQ R c= S;
A0: 1.R in SQ R;
X: now assume A: S /\ (-S) = {0.R};
now assume -1.R in S;
then -(-1.R) in -S;
then 1.R in S /\ -S by XBOOLE_0:def 4,A0,AS;
hence contradiction by A,TARSKI:def 1;
end;
hence not -1.R in S;
end;
now assume A: not -1.R in S;
now assume A2: S /\ (-S) <> {0.R};
B0: 0.R in SQ R;
then -0.R in -S by AS;
then 0.R in S /\ (-S) by AS,B0,XBOOLE_0:def 4;
then A3: {0.R} c= S /\ (-S) by TARSKI:def 1;
now assume A4: not(ex a being Element of R st
a <> 0.R & a in S /\ (-S));
now let o be object;
assume o in S /\ (-S);
then o = 0.R by A4;
hence o in {0.R} by TARSKI:def 1;
end;
hence contradiction by A2,A3,TARSKI:2;
end;
then consider a being Element of R such that
A5: a <> 0.R & a in S /\ (-S);
A9: a in S & a in (-S) by A5,XBOOLE_0:def 4;
then A6: -a in -(-S);
A7: now assume -a = 0.R;
then --a = 0.R;
hence contradiction by A5;
end;
((-a)")^2 is square;
then ((-a)")^2 in SQ R;
then A8: ((-a)")^2 * (-a) in S * S by AS,A6;
(-a)" in S
proof
((-a)")^2 * (-a) = (-a)" * ((-a)" *(-a)) by GROUP_1:def 3
.= (-a)" * 1.R by A7,VECTSP_1:def 10
.= (-a)";
hence thesis by A8,AS;
end;
then A8: a * (-a)" in S * S by A9;
(-(a")) * (-a) = a * a" by VECTSP_1:10 .= 1.R by A5,VECTSP_1:def 10; then
a * (-a)" = a * (-(a")) by A7,VECTSP_1:def 10
.= -(a * a") by VECTSP_1:8
.= -1.R by A5,VECTSP_1:def 10;
hence contradiction by A8,A,AS;
end;
hence S /\ (-S) = {0.R};
end;
hence thesis by X;
end;
theorem
for F being Field
for S being Subset of F st S * S c= S & S \/ (-S) = the carrier of F
holds S /\ (-S) = {0.F} iff not -1.F in S
proof
let F be Field, S be Subset of F;
assume AS: S * S c= S & S \/ (-S) = the carrier of F;
SQ F c= S
proof let o be object;
assume o in SQ F;
then consider a being Element of F such that A: a = o & a is square;
consider b being Element of F such that B: b^2 = a by A;
per cases by AS,XBOOLE_0:def 3;
suppose b in S;
then b * b in S * S;
hence o in S by AS,A,B;
end;
suppose b in -S;
then -b in -(-S);
then (-b) * (-b) in S * S;
then (-b) * (-b) in S by AS;
hence o in S by A,B,VECTSP_1:10;
end;
end;
hence thesis by X1,AS;
end;
definition
let R be Ring;
attr R is preordered means :defpord:
ex P being Subset of R st P is prepositive_cone;
attr R is ordered means :deford:
ex P being Subset of R st P is positive_cone;
end;
lemEX:
for S being Subset of F_Real st S = {x where x is Element of REAL : 0 <= x}
holds S is positive_cone
proof
let S be Subset of F_Real;
assume AS: S = {x where x is Element of REAL : 0 <= x};
set R = F_Real;
A: S + S c= S
proof let o be object;
assume o in S + S;
then o in {a+b where a,b is Element of R : a in S & b in S}
by IDEAL_1:def 19;
then consider a,b being Element of R such that A: o = a+b & a in S & b in S;
consider x being Element of R such that B: x = a & 0 <= x by A,AS;
consider y being Element of R such that C: y = b & 0 <= y by A,AS;
thus o in S by A,B,C,AS;
end;
B: S * S c= S
proof let o be object;
assume o in S * S;
then consider a,b being Element of R such that A: o = a*b & a in S & b in S;
consider x being Element of R such that B: x = a & 0 <= x by A,AS;
consider y being Element of R such that C: y = b & 0 <= y by A,AS;
thus o in S by A,B,C,AS;
end;
K: now let o be object;
assume K0: o in S /\ (-S);
then K1: o in S & o in (-S) by XBOOLE_0:def 4;
reconsider x = o as Element of F_Real by K0;
consider y1 being Element of R such that K2: y1 = o & 0 <= y1 by AS,K1;
consider y2 being Element of R such that K3: -y2 = o & y2 in S by K1;
consider y being Element of R such that K4: y2 = y & 0 <= y by AS,K3;
y1 = 0.R by K4,K2,K3;
hence o in {0.R} by K2,TARSKI:def 1;
end;
C: now let o be object;
assume K0: o in {0.R};
then K1: o = 0.R by TARSKI:def 1;
reconsider x = o as Element of F_Real by K0;
K2: 0 <= x & 0 <= -x by K1;
K3: x in S by AS,K0;
x in { - s where s is Element of R : s in S } by K2,K3,K1;
hence o in S /\ (-S) by K3,XBOOLE_0:def 4;
end;
F: now let o be object;
assume o in the carrier of R;
then reconsider x = o as Element of F_Real;
per cases;
suppose 0 <= x;
then x in S by AS;
hence o in S \/ (-S) by XBOOLE_0:def 3;
end;
suppose 0 <= -x;
then -x in S by AS;
then -(-x) in -S;
hence o in S \/ (-S) by XBOOLE_0:def 3;
end;
end;
for o be object st o in S \/ (-S) holds o in the carrier of R;
hence S is positive_cone by A,B,C,K,F,TARSKI:2;
end;
EX: F_Real is ordered
proof
set R = F_Real, S = {x where x is Element of REAL : 0 <= x};
now let o be object;
assume o in S;
then consider x being Element of REAL such that A: o = x & 0 <= x;
thus o in the carrier of F_Real by A;
end;
then reconsider S as Subset of F_Real by TARSKI:def 3;
S is positive_cone by lemEX;
hence thesis;
end;
registration
cluster preordered for Field;
existence
proof
take F_Real;
thus thesis by EX;
end;
cluster ordered for Field;
existence by EX;
end;
registration
cluster ordered -> preordered for Ring;
coherence;
end;
registration
let R be preordered Ring;
cluster prepositive_cone for Subset of R;
existence by defpord;
end;
registration
let R be ordered Ring;
cluster positive_cone for Subset of R;
existence by deford;
end;
definition
let R be preordered Ring;
mode Preordering of R is prepositive_cone Subset of R;
end;
definition
let R be ordered Ring;
mode Ordering of R is positive_cone Subset of R;
end;
theorem ord1:
for R being preordered Ring
for P being Preordering of R
for a being Element of R holds a^2 in P
proof
let R be preordered Ring, P be Preordering of R, a be Element of R;
a^2 is square;
then A: a^2 in SQ R;
SQ R c= P by defppc;
hence thesis by A;
end;
theorem ord2:
for R being preordered Ring
for P being Preordering of R holds QS R c= P
proof
let R be preordered Ring, P be Preordering of R;
P is with_sums_of_squares;
hence thesis;
end;
theorem ord3:
for R being preordered Ring
for P being Preordering of R holds 0.R in P & 1.R in P
proof
let R be preordered Ring, O be Preordering of R;
0.R in QS R & 1.R in QS R;
hence thesis by ord2,TARSKI:def 3;
end;
theorem ord4:
for R being preordered non degenerated Ring
for P being Preordering of R holds not -1.R in P
proof
let R be preordered non degenerated Ring, P be Preordering of R;
A: 1.R in P by ord3;
assume -1.R in P;
then -(-1.R) in - P;
then 1.R in P /\ -P by XBOOLE_0:def 4,A;
then 1.R in {0.R} by defppc;
hence contradiction by TARSKI:def 1;
end;
theorem ord5:
for F being preordered Field
for P being Preordering of F
for a being non zero Element of F st a in P holds a" in P
proof
let F be preordered Field; let P be Preordering of F;
let a be non zero Element of F;
assume A: a in P;
E: a <> 0.F;
set b = a";
C: P * P c= P by defppc;
b * b = b^2;
then b * b in P by ord1;
then B: a*(b*b) in {x*y where x,y is Element of F : x in P & y in P} by A;
a * (b * b) = (a * b) * b by GROUP_1:def 3
.= 1.F * b by E,VECTSP_1:def 10
.= b;
hence thesis by B,C;
end;
theorem tchar:
for R being preordered non degenerated Ring holds Char R = 0
proof
let R be preordered non degenerated Ring;
set P = the Preordering of R;
A: 1.R in P by ord3;
B: QS R c= P by ord2;
set n = Char R;
now assume AS: Char R <> 0;
then C: n '*' 1.R = 0.R by RING_3:def 5;
(n '*' 1.R) - 1.R = (n '*' 1.R) - (1 '*' 1.R) by RING_3:60;
then F: (n-1) '*' 1.R = - 1.R by C,RING_3:64;
reconsider n1 = n-1 as Element of NAT by AS,INT_1:3;
deffunc F(object) = 1.R;
consider f being FinSequence such that
D: len f = n1 & for k being Nat st k in dom f holds f.k = F(k)
from FINSEQ_1:sch 2;
now let o be object;
assume o in rng f;
then consider k being object such that
E: k in dom f & o = f.k by FUNCT_1:def 3;
f.k = 1.R by E,D;
hence o in the carrier of R by E;
end;
then rng f c= the carrier of R;
then reconsider f as FinSequence of R by FINSEQ_1:def 4;
now let k be Element of NAT;
assume 1 <= k & k <= n1;
then E: k in dom f by D,FINSEQ_3:25;
hence f/.k = f.k by PARTFUN1:def 6 .= 1.R by E,D;
end;
then E: Sum f = n1 * 1.R by D,POLYNOM8:4 .= -1.R by F,RING_3:def 2;
now let k be Nat;
assume G: k in dom f;
1.R is square;
hence ex a being Element of R st f.k = a^2 by G,D;
end;
then -1.R is sum_of_squares by E;
then -1.R in QS R;
then --1.R in -P by B;
then 1.R in P /\ (-P) by A,XBOOLE_0:def 4;
then 1.R in {0.R} by defppc;
hence contradiction by TARSKI:def 1;
end;
hence thesis;
end;
theorem ordsub:
for R being ordered Ring
for O,P being Ordering of R st O c= P holds O = P
proof
let R be ordered Ring, O,P be Ordering of R;
assume AS: O c= P;
now assume not(P c= O);
then consider a being Element of R such that
A: a in P & not(a in O);
a in the carrier of R;
then a in O \/ - O by defsp;
then a in -O by A,XBOOLE_0:def 3;
then B: -a in --O;
-a in -P by A;
then -a in P /\ (-P) by AS,B,XBOOLE_0:def 4;
then -a in {0.R} by defneg;
then C: -a = 0.R by TARSKI:def 1;
a = --a .= 0.R by C;
hence contradiction by A,ord3;
end;
hence thesis by AS;
end;
begin :: Orderings vs. Order Relations
definition
let R be preordered Ring,
P be Preordering of R;
let a,b be Element of R;
pred a <= P,b means
b - a in P;
end;
definition
let R be preordered Ring,
P be Preordering of R;
func OrdRel P -> Relation of R equals
{ [a,b] where a,b is Element of R : a <= P,b };
coherence
proof
set M = {[a,b] where a,b is Element of R : a <= P,b};
M c= [:the carrier of R,the carrier of R:]
proof let x be object;
assume x in M;
then consider a,b being Element of R such that
A1: x = [a,b] & a <= P,b;
thus x in [:the carrier of R,the carrier of R:] by A1;
end;
hence thesis;
end;
end;
registration
let R be preordered Ring;
let P be Preordering of R;
cluster OrdRel P -> non empty;
coherence
proof
0.R <= P,0.R by ord3;
then [0.R,0.R] in {[a,b] where a,b is Element of R : a <= P,b};
hence thesis;
end;
end;
registration
let R be preordered Ring,
P be Preordering of R;
cluster OrdRel P -> strongly_reflexive antisymmetric transitive;
coherence
proof
set H = OrdRel P;
now let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
a - a = 0.R by RLVECT_1:15;
then a <= P,a by ord3;
hence [x,x] in H;
end;
hence H is strongly_reflexive by RELAT_2:def 1;
now let x,y be object;
assume AS: x in field H & y in field H & [x,y] in H & [y,x] in H;
then consider a,b being Element of R such that
A1: [x,y] = [a,b] & a <= P,b;
consider e,f being Element of R such that
A2: [e,f] = [y,x] & e <= P,f by AS;
C: x = a & y = b & y = e & x = f by A1,A2,XTUPLE_0:1;
-(b - a) = a - b by RLVECT_1:33;
then a - b in -P by A1;
then a - b in P /\ (-P) by C,A2,XBOOLE_0:def 4;
then a - b in {0.R} by defneg;
then a - b = 0.R by TARSKI:def 1;
hence x = y by C,RLVECT_1:21;
end;
hence H is antisymmetric by RELAT_2:def 12,RELAT_2:def 4;
now let x,y,z be object;
assume AS: x in field H & y in field H & z in field H &
[x,y] in H & [y,z] in H;
then consider a,b being Element of R such that
A1: [x,y] = [a,b] & a <= P,b;
consider e,c being Element of R such that
A2: [e,c] = [y,z] & e <= P,c by AS;
C: x = a & y = b & y = e & z = c by A1,A2,XTUPLE_0:1;
then (c - b) + (b - a) in
{s1+s2 where s1,s2 is Element of R : s1 in P & s2 in P} by A1,A2;
then D: (c - b) + (b - a) in P + P by IDEAL_1:def 19;
B: P + P c= P by defppc;
(c - b) + (b - a)
= ((c + -b) + b) + -a by RLVECT_1:def 3
.= (c + (-b + b)) + -a by RLVECT_1:def 3
.= (c + 0.R) + -a by RLVECT_1:5
.= c - a;
then a <= P,c by B,D;
hence [x,z] in H by C;
end;
hence H is transitive by RELAT_2:def 16,RELAT_2:def 8;
end;
end;
registration
let R be preordered Ring,
P be Preordering of R;
cluster OrdRel P -> respecting_addition respecting_multiplication;
coherence
proof
set Q = OrdRel P;
now let r1,r2,r3 be Element of R;
assume r1 <=_Q,r2;
then consider a,b being Element of R such that
A: [a,b] = [r1,r2] & a <= P,b;
B: a = r1 & b = r2 by A,XTUPLE_0:1;
(r2 + r3) - (r1 + r3) = (r2 + r3) + (-r3 + -r1) by RLVECT_1:31
.= ((r2 + r3) + -r3) + -r1 by RLVECT_1:def 3
.= (r2 + (r3 + -r3)) + -r1 by RLVECT_1:def 3
.= (r2 + 0.R) + -r1 by RLVECT_1:5
.= r2 - r1;
then (r1 + r3) <= P,(r2 + r3) by A,B;
hence (r1+r3) <=_Q,(r2+r3);
end;
hence Q is respecting_addition;
let r1,r2,r3 be Element of R;
assume H: r1 <=_Q,r2 & 0.R <=_Q,r3;
then consider a,b being Element of R such that
A: [a,b] = [r1,r2] & a <= P,b;
consider e,f being Element of R such that
B: [e,f] = [0.R,r3] & e <= P,f by H;
D: r1 = a & r2 = b & e = 0.R & r3 = f by A,B,XTUPLE_0:1;
(r2 * r3) - (r1 * r3) = (r2 - r1) * r3 by VECTSP_1:13;
then E: (r2 * r3) - (r1 * r3) in P * P by D,B,A;
P * P c= P by defppc;
then (r1 * r3) <= P,(r2 * r3) by E;
hence r1*r3 <=_Q,r2*r3;
end;
end;
registration
let R be ordered Ring,
O be Ordering of R;
cluster OrdRel O -> totally_connected;
coherence
proof
set H = OrdRel O;
now let x,y be object;
assume x in the carrier of R & y in the carrier of R;
then reconsider a=x, b=y as Element of R;
A: O \/ -O = the carrier of R by defpc;
per cases by A,XBOOLE_0:def 3;
suppose a-b in O;
then b <= O,a;
hence [x,y] in H or [y,x] in H;
end;
suppose a-b in -O;
then -(a-b) in --O;
then a <= O,b by RLVECT_1:33;
hence [x,y] in H or [y,x] in H;
end;
end;
hence thesis by RELAT_2:def 7;
end;
end;
registration
let R be preordered Ring;
cluster strongly_reflexive antisymmetric transitive respecting_addition
respecting_multiplication for Relation of R;
existence
proof
set P = the Preordering of R;
take OrdRel P;
thus thesis;
end;
end;
registration
let R be ordered Ring;
cluster strongly_reflexive antisymmetric transitive respecting_addition
respecting_multiplication totally_connected for Relation of R;
existence
proof
set P = the Ordering of R;
take OrdRel P;
thus thesis;
end;
end;
definition
let R be preordered Ring;
mode OrderRelation of R is
strongly_reflexive antisymmetric transitive respecting_addition
respecting_multiplication Relation of R;
end;
definition
let R be ordered Ring;
mode total_OrderRelation of R is
strongly_reflexive antisymmetric transitive respecting_addition
respecting_multiplication totally_connected Relation of R;
end;
definition
let R be Ring;
let Q be Relation of R;
func Positives Q -> Subset of R equals
{ a where a is Element of R : 0.R <=_Q,a };
coherence
proof
set M = {a where a is Element of R : 0.R <=_Q,a};
M c= the carrier of R
proof let x be object;
assume x in M;
then consider a being Element of R such that
A1: x = a & 0.R <=_Q,a;
thus x in the carrier of R by A1;
end;
hence thesis;
end;
end;
registration
let R be preordered Ring;
let Q be strongly_reflexive Relation of R;
cluster Positives Q -> non empty;
coherence
proof
0.R <=_Q,0.R by defstr,RELAT_2:def 1;
then 0.R in Positives Q;
hence thesis;
end;
end;
registration
let R be preordered Ring;
let Q be OrderRelation of R;
cluster Positives Q -> add-closed mult-closed negative-disjoint;
coherence
proof
set P = Positives Q;
now let x,y be Element of R;
assume A0: x in P & y in P;
then consider a being Element of R such that A1: x = a & 0.R <=_Q,a;
consider b being Element of R such that A2: y = b & 0.R <=_Q,b by A0;
0.R + b <=_Q,a+b by respadd,A1;
then 0.R <=_Q,a+b by A2,lemtrans;
hence x + y in P by A1,A2;
end;
hence P is add-closed;
now let x,y be Element of R;
assume A0: x in P & y in P;
then consider a being Element of R such that A1: x = a & 0.R <=_Q,a;
consider b being Element of R such that A2: y = b & 0.R <=_Q,b by A0;
0.R * b <=_Q,a*b by respmult,A1,A2;
hence x * y in P by A1,A2;
end;
hence P is mult-closed;
A: now let x be object;
assume x in P /\ (-P);
then A0: x in P & x in -P by XBOOLE_0:def 4;
consider a being Element of R such that A1: x = a & 0.R <=_Q,a by A0;
consider b being Element of R such that A2: x = -b & b in P by A0;
consider c being Element of R such that A3: c = b & 0.R <=_Q,c by A2;
a+ 0.R <=_Q,a + -a by A3,respadd,A1,A2;
then a <=_Q,0.R by RLVECT_1:5;
then a = 0.R by A1,lemanti;
hence x in {0.R} by A1,TARSKI:def 1;
end;
now let x be object;
assume C: x in {0.R};
then A: x = 0.R by TARSKI:def 1;
reconsider a = x as Element of R by C;
a <=_Q,a by defstr,RELAT_2:def 1;
then B: a in P by A;
-a = a by A;
then a in -P by B;
hence x in P /\ (-P) by B,XBOOLE_0:def 4;
end;
hence P is negative-disjoint by A,TARSKI:2;
end;
end;
registration
let R be ordered Ring;
let Q be total_OrderRelation of R;
cluster Positives Q -> spanning;
coherence
proof
set P = Positives Q;
A: now let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
per cases by Rtot,RELAT_2:def 7;
suppose 0.R <=_Q,a;
then a in P;
hence x in P \/ (-P) by XBOOLE_0:def 3;
end;
suppose a <=_Q,0.R;
then a + (-a) <=_Q,0.R + (-a) by respadd;
then 0.R <=_Q,0.R + (-a) by RLVECT_1:5;
then -a in P;
then --a in -P;
hence x in P \/ (-P) by XBOOLE_0:def 3;
end;
end;
for x be object st x in P \/ (-P) holds x in the carrier of R;
hence thesis by A,TARSKI:2;
end;
end;
theorem
for R being preordered Ring
for P being Preordering of R holds OrdRel P is OrderRelation of R;
theorem
for R being ordered Ring
for P being Ordering of R holds OrdRel P is total_OrderRelation of R;
theorem
for R being ordered Ring
for Q being total_OrderRelation of R holds Positives Q is Ordering of R;
begin :: Some ordered (and non ordered) Rings
lemsubpreord:
for R being preordered Ring, P being Preordering of R
for S being Subring of R, Q being Subset of S
st Q = P /\ (the carrier of S) holds Q is prepositive_cone
proof
let R be preordered Ring, P be Preordering of R, S be Subring of R,
Q be Subset of S;
assume AS: Q = P /\ (the carrier of S);
now let o be object;
assume A: o in Q;
the carrier of S c= the carrier of R by C0SP1:def 3;
hence o in the carrier of R by A;
end;
then reconsider Q1 = Q as Subset of R by TARSKI:def 3;
AS1: -Q1 = -Q by lemminus1;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
reconsider E = the carrier of S as Subset of R by C0SP1:def 3;
AS3: now let o be object;
assume o in the carrier of S;
then reconsider a = o as Element of S;
reconsider b = -a as Element of R by AS4;
-b = -(-a) by lemminus .= o;
hence o in -E;
end;
now let o be object;
assume o in -E;
then consider a being Element of R such that B: -a = o & a in E;
reconsider b = a as Element of S by B;
-a = -b by lemminus;
hence o in the carrier of S by B;
end;
then AS2: the carrier of S = -E by AS3,TARSKI:2;
A: Q + Q c= Q
proof let x be object;
assume x in Q + Q;
then x in {a + b where a,b is Element of S : a in Q & b in Q}
by IDEAL_1:def 19;
then consider a,b being Element of S such that
A1: x = a + b & a in Q & b in Q;
A2: a in P & b in P by A1,AS,XBOOLE_0:def 4;
reconsider a1 = a, b1 = b as Element of R by A1,AS;
a1 + b1 in {u+v where u,v is Element of R : u in P & v in P} by A2;
then A3: a1 + b1 in P + P by IDEAL_1:def 19;
A4: P + P c= P by defppc;
dom(the addF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then A6: [a,b] in dom(the addF of S);
a1 + b1 = ((the addF of R)||(the carrier of S)).(a,b) by A6,FUNCT_1:49
.= a + b by C0SP1:def 3;
hence x in Q by A1,AS,A4,A3,XBOOLE_0:def 4;
end;
B: Q * Q c= Q
proof let x be object;
assume x in Q * Q;
then consider a,b being Element of S such that
B1: x = a * b & a in Q & b in Q;
B2: a in P & b in P by B1,AS,XBOOLE_0:def 4;
reconsider a1 = a, b1 = b as Element of R by B1,AS;
B3: a1 * b1 in P * P by B2;
B4: P * P c= P by defppc;
dom(the multF of S) = [:the carrier of S,the carrier of S:]
by FUNCT_2:def 1;
then B6: [a,b] in dom(the multF of S);
a1 * b1 = ((the multF of R)||(the carrier of S)).(a,b) by B6,FUNCT_1:49
.= a * b by C0SP1:def 3;
hence x in Q by B1,AS,B4,B3,XBOOLE_0:def 4;
end;
C1: now let o be object;
assume o in Q /\ -Q;
then C3: o in Q & o in -Q by XBOOLE_0:def 4;
then o in -(P /\ (the carrier of S)) by AS,lemminus1;
then o in (-P) /\ (- E) by min1;
then o in P & o in -P by C3,AS,XBOOLE_0:def 4;
then C2: o in P /\ -P by XBOOLE_0:def 4;
P /\ -P = {0.R} by defppc;
hence o in {0.S} by C2,C0SP1:def 3;
end;
C:now let o be object;
assume CC: o in {0.S};
then o = 0.S by TARSKI:def 1 .= 0.R by C0SP1:def 3;
then o in {0.R} by TARSKI:def 1;
then o in P /\ -P by defppc;
then C2: o in P & o in -P by XBOOLE_0:def 4;
then C5: o in Q by CC,AS,XBOOLE_0:def 4;
o in (-P) /\ (-E) by AS2,C2,CC,XBOOLE_0:def 4;
then o in -(P /\ the carrier of S) by min1;
hence o in Q /\ -Q by AS1,AS,C5,XBOOLE_0:def 4;
end;
Q: SQ S c= SQ R by SQsub;
SQ R c= P by defppc;
then SQ S c= P by Q;
then SQ S c= P /\ (the carrier of S) by XBOOLE_0:def 4;
hence thesis by A,B,C,C1,AS,TARSKI:2;
end;
lemsubord:
for R being ordered Ring, O being Ordering of R
for S being Subring of R, Q being Subset of S
st Q = O /\ (the carrier of S) holds Q is positive_cone
proof
let R be ordered Ring, O be Ordering of R, S be Subring of R, Q be Subset of S;
assume AS: Q = O /\ (the carrier of S);
then AS1: Q is prepositive_cone by lemsubpreord;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
reconsider E = the carrier of S as Subset of R by C0SP1:def 3;
AS3: now let o be object;
assume o in the carrier of S;
then reconsider a = o as Element of S;
reconsider b = -a as Element of R by AS4;
-b = -(-a) by lemminus .= o;
hence o in -E;
end;
now let o be object;
assume o in -E;
then consider a being Element of R such that B: -a = o & a in E;
reconsider b = a as Element of S by B;
-a = -b by lemminus;
hence o in the carrier of S by B;
end;
then AS2: the carrier of S = -E by AS3,TARSKI:2;
B: now let o be object;
assume A0: o in the carrier of S;
then reconsider a = o as Element of R by AS4;
A1: O is spanning;
per cases by A1,XBOOLE_0:def 3;
suppose a in O;
then a in O /\ (the carrier of S) by A0,XBOOLE_0:def 4;
hence o in Q \/ (-Q) by AS,XBOOLE_0:def 3;
end;
suppose a in -O;
then a in (-O) /\ (-E) by AS2,A0,XBOOLE_0:def 4;
then o in -(O /\ (the carrier of S)) by min1;
then o in -Q by AS,lemminus1;
hence o in Q \/ (-Q) by XBOOLE_0:def 3;
end;
end;
for o be object st o in Q \/ (-Q) holds o in the carrier of S;
hence thesis by AS1,B,TARSKI:2;
end;
registration
let R be preordered Ring;
cluster -> preordered for Subring of R;
coherence
proof
let S be Subring of R;
set P = the Preordering of R;
for o be object st o in P /\ (the carrier of S) holds
o in the carrier of S by XBOOLE_0:def 4;
then reconsider M = P /\ (the carrier of S) as Subset of S by TARSKI:def 3;
M is prepositive_cone by lemsubpreord;
hence thesis;
end;
end;
registration
let R be ordered Ring;
cluster -> ordered for Subring of R;
coherence
proof
let S be Subring of R;
set P = the Ordering of R;
for o be object st o in P /\ (the carrier of S) holds
o in the carrier of S by XBOOLE_0:def 4;
then reconsider M = P /\ (the carrier of S) as Subset of S by TARSKI:def 3;
M is positive_cone by lemsubord;
hence thesis;
end;
end;
theorem
for R being preordered Ring
for P being Preordering of R
for S being Subring of R holds P /\ (the carrier of S) is Preordering of S
proof
let R be preordered Ring, O be Preordering of R, S be Subring of R;
for o be object st o in O /\ (the carrier of S) holds
o in the carrier of S by XBOOLE_0:def 4;
then reconsider M = O /\ (the carrier of S) as Subset of S by TARSKI:def 3;
M is prepositive_cone by lemsubpreord;
hence thesis;
end;
theorem
for R being ordered Ring
for O being Ordering of R
for S being Subring of R holds O /\ (the carrier of S) is Ordering of S
proof
let R be ordered Ring, O be Ordering of R, S be Subring of R;
for o be object st o in O /\ (the carrier of S) holds
o in the carrier of S by XBOOLE_0:def 4;
then reconsider M = O /\ (the carrier of S) as Subset of S by TARSKI:def 3;
M is positive_cone by lemsubord;
hence thesis;
end;
registration
cluster F_Complex -> non preordered;
coherence
proof
assume F_Complex is preordered;
then reconsider F = F_Complex as preordered Field;
consider P being Subset of F such that
A1: P is prepositive_cone by defpord;
reconsider P as Preordering of F by A1;
reconsider i = <i> as Element of F by COMPLFLD:def 1;
A2: QS F c= P by ord2;
-1.F = -1r by COMPLFLD:2,COMPLFLD:8
.= <i>*<i>
.= i^2 by COMPLFLD:4;
then -1.F is square;
then -1.F in QS F;
hence contradiction by A2,ord4;
end;
end;
registration
let n be non trivial Nat;
cluster Z/n -> non preordered;
coherence
proof
Char(Z/n) <> 0;
hence thesis by tchar;
end;
end;
definition
func Positives(F_Real) -> Subset of F_Real equals
{ r where r is Element of REAL : 0 <= r };
coherence
proof
now let o be object;
assume o in {x where x is Element of REAL : 0 <= x};
then consider x being Element of F_Real such that A: o = x & 0 <= x;
thus o in the carrier of F_Real by A;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
cluster Positives(F_Real) -> add-closed mult-closed negative-disjoint spanning;
coherence
proof
Positives(F_Real) is positive_cone by lemEX;
hence thesis;
end;
end;
registration
cluster F_Real -> ordered;
coherence
proof
Positives(F_Real) is positive_cone; hence thesis;
end;
end;
theorem
Positives(F_Real) is Ordering of F_Real;
theorem
for O being Ordering of F_Real holds O = Positives(F_Real)
proof
let O be Ordering of F_Real;
X: QS F_Real c= O by ord2;
now let x be object;
assume x in Positives(F_Real);
then consider r being Element of F_Real such that A: x = r & 0 <= r;
reconsider q = sqrt r as Element of F_Real by XREAL_0:def 1;
r = (sqrt r)^2 by A,SQUARE_1:def 2
.= q^2;
then r is square;
then r in QS F_Real;
hence x in O by A,X;
end;
then Positives(F_Real) c= O;
hence thesis by ordsub;
end;
definition
func Positives(F_Rat) -> Subset of F_Rat equals
{ r where r is Element of RAT : 0 <= r };
coherence
proof
now let o be object;
assume o in {x where x is Element of RAT : 0 <= x};
then consider x being Element of RAT such that A: o = x & 0 <= x;
thus o in the carrier of F_Rat by A,GAUSSINT:def 14;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
cluster Positives(F_Rat) -> add-closed mult-closed negative-disjoint spanning;
coherence
proof
set S = Positives(F_Rat); set R = F_Rat;
A: S + S c= S
proof let o be object;
assume o in S + S;
then o in {a+b where a,b is Element of R : a in S & b in S}
by IDEAL_1:def 19;
then consider a,b being Element of R such that A: o = a+b & a in S & b in S;
consider x being Element of RAT such that B: x = a & 0 <= x by A;
consider y being Element of RAT such that C: y = b & 0 <= y by A;
thus o in S by A,B,C,GAUSSINT:def 14;
end;
B: S * S c= S
proof let o be object;
assume o in S * S;
then consider a,b being Element of R such that A: o = a*b & a in S & b in S;
consider x being Element of RAT such that B: x = a & 0 <= x by A;
consider y being Element of RAT such that C: y = b & 0 <= y by A;
thus o in S by A,B,C,GAUSSINT:def 14;
end;
K: now let o be object;
assume K0: o in S /\ (-S);
then K1: o in S & o in (-S) by XBOOLE_0:def 4;
reconsider x = o as Element of F_Rat by K0;
consider y1 being Element of RAT such that K2: y1 = o & 0 <= y1 by K1;
consider y2 being Element of F_Rat such that K3: -y2 = o & y2 in S by K1;
reconsider y2 as Element of RAT by GAUSSINT:def 14;
consider y being Element of RAT such that K4: y2 = y & 0 <= y by K3;
y1 = 0.R by K4,K2,K3,GAUSSINT:def 14;
hence o in {0.R} by K2,TARSKI:def 1;
end;
C: now let o be object;
assume K0: o in {0.R};
then K1: o = 0.R by TARSKI:def 1;
reconsider x = o as Element of RAT by K0,GAUSSINT:def 14;
reconsider xx = x as Element of R by GAUSSINT:def 14;
K3: x in S by K0,GAUSSINT:def 14;
-xx in {-s where s is Element of R : s in S} by K3;
hence o in S /\ (-S) by K1,K3,XBOOLE_0:def 4;
end;
F: now let o be object;
assume o in the carrier of R;
then reconsider x = o as Element of RAT by GAUSSINT:def 14;
F1: -x is Element of RAT by RAT_1:def 2;
reconsider xx = x as Element of F_Rat by GAUSSINT:def 14;
per cases;
suppose 0 <= x;
then x in S;
hence o in S \/ (-S) by XBOOLE_0:def 3;
end;
suppose 0 <= -x;
then -xx in S by F1;
then --xx in -S;
hence o in S \/ (-S) by XBOOLE_0:def 3;
end;
end;
for o be object st o in S \/ (-S) holds o in the carrier of R;
then S is positive_cone by A,B,C,K,F,TARSKI:2;
hence thesis;
end;
end;
registration
cluster F_Rat -> ordered;
coherence
proof
Positives(F_Rat) is positive_cone; hence thesis;
end;
end;
theorem
Positives(F_Rat) is Ordering of F_Rat;
theorem
for O being Ordering of F_Rat holds O = Positives(F_Rat)
proof
let O be Ordering of F_Rat;
defpred P[Nat] means $1 in O;
A: 0.(F_Rat) = 0 & 1.(F_Rat) = 1 by GAUSSINT:def 14;
B: 1.F_Rat in O & 0.F_Rat in O by ord3;
IA: P[0] by A,ord3;
E: O + O c= O & O * O c= O by defpc;
IS: now let k be Nat;
assume C: P[k];
then consider a being Element of F_Rat such that D: a = k;
a + 1.F_Rat in {x + y where x,y is Element of F_Rat :
x in O & y in O} by D,C,B;
then k + 1 in O + O by GAUSSINT:def 14,D,IDEAL_1:def 19;
hence P[k+1] by E;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
Positives(F_Rat) c= O
proof let o be object;
assume o in Positives(F_Rat);
then consider r being Element of RAT such that A1: o = r & 0 <= r;
consider m,n being Integer such that B1: n > 0 & r = m/n by RAT_1:1;
reconsider a=n,b=m as Element of F_Rat by RAT_1:def 2,GAUSSINT:def 14;
per cases;
suppose m = 0;
hence o in O by B1,A1,A,ord3;
end;
suppose C1: 0 < m;
0 <= n by B1;
then reconsider n1 = n, m1 = m as Element of NAT by C1,INT_1:3;
C: m1 in O & n1 in O by I;
a is non zero by B1,GAUSSINT:def 14;
then a" in O by C,ord5;
then b * a" in O * O by C;
then b * a" in O by E;
hence o in O by A1,B1,GAUSSINT:def 14,GAUSSINT:15;
end;
suppose C1: m < 0;
then 0 >= n by A1,B1;
then reconsider n1 = -n, m1 = -m as Element of NAT by C1,INT_1:3;
C: m1 in O & n1 in O by I;
K: -a <> 0.F_Rat by B1,GAUSSINT:def 14;
-a is non zero by B1,GAUSSINT:def 14;
then (-a)" in O by C,ord5;
then F: (-b) * ((-a)") in O * O by C;
H: -(n") = -(a") by B1,GAUSSINT:def 14,GAUSSINT:15;
a <> 0.F_Rat by B1,GAUSSINT:def 14; then
1.F_Rat = a * a" by VECTSP_1:def 10 .= (-(a")) * (-a);
then (-a)" = -(a") by VECTSP_1:def 10,K;
hence o in O by A1,B1,F,E,H;
end;
end;
hence thesis by ordsub;
end;
definition
func Positives(INT.Ring) -> Subset of INT.Ring equals
{ i where i is Element of INT : 0 <= i };
coherence
proof
now
let o be object;
assume o in {x where x is Element of INT : 0 <= x};
then consider x being Element of INT such that A: o = x & 0 <= x;
thus o in the carrier of INT.Ring by A,INT_3:def 3;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
cluster Positives(INT.Ring)
-> add-closed mult-closed negative-disjoint spanning;
coherence
proof
B: now let o be object;
assume o in Positives(INT.Ring);
then consider i being Element of INT such that A1: o = i & 0 <= i;
reconsider r = i as Element of RAT by RAT_1:def 2;
r in {x where x is Element of RAT : 0 <= x} by A1;
hence o in Positives(F_Rat) /\ (the carrier of INT.Ring)
by A1,INT_3:def 3,XBOOLE_0:def 4;
end;
now let o be object;
assume B1: o in Positives(F_Rat) /\ (the carrier of INT.Ring);
then o in Positives(F_Rat) & o in (the carrier of INT.Ring)
by XBOOLE_0:def 4;
then consider a being Element of RAT such that B2: o = a & 0 <= a;
a is Element of INT by B1,B2,INT_3:def 3,XBOOLE_0:def 4;
hence o in Positives(INT.Ring) by B2;
end;
then Positives(INT.Ring) is positive_cone by RING_3:47,B,lemsubord,TARSKI:2;
hence thesis;
end;
end;
registration
cluster INT.Ring -> ordered;
coherence
proof
Positives(INT.Ring) is positive_cone; hence thesis;
end;
end;
theorem
Positives(INT.Ring) is Ordering of INT.Ring;
theorem
for O being Ordering of INT.Ring holds O = Positives(INT.Ring)
proof
let O be Ordering of INT.Ring;
defpred P[Nat] means $1 in O;
B: 1.INT.Ring in O & 0.INT.Ring in O by ord3;
0.(INT.Ring) = 0 & 1.(INT.Ring) = 1 by INT_3:def 3; then
IA: P[0] by ord3;
E: O + O c= O by defpc;
IS: now let k be Nat;
assume C: P[k];
then consider a being Element of INT.Ring such that D: a = k;
a + 1.INT.Ring in {x + y where x,y is Element of INT.Ring :
x in O & y in O} by D,C,B;
then k + 1 in O + O by INT_3:def 3,D,IDEAL_1:def 19;
hence P[k+1] by E;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
now let o be object;
assume o in Positives(INT.Ring);
then consider i being Element of INT such that A: o = i & 0 <= i;
i is Element of NAT by A,INT_1:3;
hence o in O by A,I;
end;
then Positives(INT.Ring) c= O;
hence thesis by ordsub;
end;
begin :: Ordered Polynomial Rings
definition
let R be preordered Ring;
let P be Preordering of R;
func Positives(Poly) P -> Subset of Polynom-Ring R equals
{ p where p is Polynomial of R : LC p in P };
coherence
proof
now let o be object;
assume o in {x where x is Polynomial of R : LC x in P};
then consider x being Polynomial of R such that A: o = x & LC x in P;
thus o in the carrier of Polynom-Ring R by A,POLYNOM3:def 10;
end;
hence thesis by TARSKI:def 3;
end;
end;
lemminuspoly:
for R be Ring, a be Element of Polynom-Ring R,
b be Polynomial of R st a = b holds -a = -b
proof
let R be Ring, a be Element of Polynom-Ring R, b be Polynomial of R;
assume AS: a = b;
set K = Polynom-Ring R;
reconsider c = -b as Element of Polynom-Ring R by POLYNOM3:def 10;
a + c = b - b by AS,POLYNOM3:def 10
.= 0_.(R) by POLYNOM3:29
.= 0.K by POLYNOM3:def 10
.= a + (-a) by RLVECT_1:5;
hence thesis by RLVECT_1:8;
end;
registration
let R be preordered non degenerated Ring;
let P be Preordering of R;
cluster Positives(Poly) P -> add-closed negative-disjoint;
coherence
proof
set M = Positives(Poly) P, K = Polynom-Ring R;
X1: P + P c= P & P *P c= P by defppc;
now let x,y be Element of K;
assume AS: x in M & y in M;
then consider p being Polynomial of R such that
A: x = p & LC p in P;
consider q being Polynomial of R such that
B: y = q & LC q in P by AS;
LC p + LC q in {x+y where x,y is Element of R : x in P & y in P} by A,B;
then C: LC p + LC q in P+P by IDEAL_1:def 19;
D: now assume D1: LC p + LC q = 0.R;
then LC q = -(LC p) by RLVECT_1:6;
then -(-(LC p)) in -P by B;
then LC p in P /\ (-P) by A,XBOOLE_0:def 4;
then LC p in {0.R} by defppc;
hence LC p = 0.R by TARSKI:def 1;
hence LC q = 0.R by D1;
end;
LC(p+q) in P
proof
per cases by XXREAL_0:1;
suppose AS: len p = len q; then
C0: (p+q).(len(p)-'1) = LC p + LC q by NORMSP_1:def 2;
C11: len p is_at_least_length_of p &
len p is_at_least_length_of q by AS,ALGSEQ_1:def 3;
C1: len(p+q) = len p
proof
now let m be Nat;
assume c13: m is_at_least_length_of p+q;
thus len p <= m
proof assume C14: m < len p;
then C15: len p - 1 = len p -' 1 by NAT_1:14,XREAL_1:233;
m < (len p - 1) + 1 by C14;
then p is zero by D,C0,c13,C15,NAT_1:13;
hence contradiction by C14,POLYNOM4:3;
end;
end;
hence thesis by C11,ALGSEQ_1:def 3,POLYNOM3:24;
end;
LC(p+q) = LC p + LC q by C1,AS,NORMSP_1:def 2;
hence thesis by C,X1;
end;
suppose AS: len p < len q;
then C11: len(p+q) = max(len p,len q) by POLYNOM4:7
.= len q by AS,XXREAL_0:def 10;
C15: len q - 1 = len q -' 1 by AS,NAT_1:14,XREAL_1:233;
len p < (len q - 1) + 1 by AS;
then C13: len p <= len(q) -' 1 by C15,NAT_1:13;
len p is_at_least_length_of p by ALGSEQ_1:def 3;
then C12: p.(len(q)-'1) = 0.R by C13;
LC(p+q) = p.(len(q)-'1) + q.(len(q)-'1) by NORMSP_1:def 2,C11
.= LC q by C12;
hence thesis by B;
end;
suppose AS: len p > len q;
then C11: len(p+q) = max(len p,len q) by POLYNOM4:7
.= len p by AS,XXREAL_0:def 10;
C15: len p - 1 = len p -' 1 by XREAL_1:233,AS,NAT_1:14;
len q < (len p - 1) + 1 by AS;
then C13: len q <= len(p) -' 1 by C15,NAT_1:13;
len q is_at_least_length_of q by ALGSEQ_1:def 3;
then C12: q.(len(p)-'1) = 0.R by C13;
LC(p+q) = p.(len(p)-'1) + q.(len(p)-'1) by NORMSP_1:def 2,C11
.= LC p by C12;
hence thesis by A;
end;
end;
then p+q in {r where r is Polynomial of R : LC r in P};
hence x + y in M by A,B,POLYNOM3:def 10;
end;
hence M is add-closed;
X: now let o be object;
assume o in {0.K};
then o = 0.K by TARSKI:def 1;
then X1: o = 0_.(R) by POLYNOM3:def 10;
LC 0_.(R) = 0.R by FUNCOP_1:7;
then LC 0_.(R) in {0.R} by TARSKI:def 1;
then LC 0_.(R) in P /\ (-P) by defppc;
then LC 0_.(R) in P & LC 0_.(R) in -P by XBOOLE_0:def 4;
then X3: 0_.(R) in M;
reconsider q = 0_.(R) as Element of K by POLYNOM3:def 10;
X4: -q in {-p where p is Element of K : p in M} by X3;
len(-(0_.(R))) = len(0_.(R)) by POLYNOM4:8 .= 0 by POLYNOM4:3;
then 0_.(R) = -(0_.(R)) by POLYNOM4:5 .= -q by lemminuspoly;
hence o in M /\ (-M) by X1,X3,X4,XBOOLE_0:def 4;
end;
now let o be object;
assume o in M /\ (-M);
then X1: o in M & o in -M by XBOOLE_0:def 4;
then consider p being Polynomial of R such that X2: o = p & LC p in P;
consider x being Element of K such that X3: o = -x & x in M by X1;
consider q being Polynomial of R such that X4: x = q & LC q in P by X3;
X6: p = -q by X4,X3,X2,lemminuspoly;
then len p = len q by POLYNOM4:8;
then LC p = -(LC q) by BHSP_1:44,X6;
then LC p in -P by X4;
then LC p in P /\ (-P) by X2,XBOOLE_0:def 4;
then LC p in {0.R} by defppc;
then p is zero by TARSKI:def 1;
then p = 0.K by POLYNOM3:def 10;
hence o in {0.K} by X2,TARSKI:def 1;
end;
hence M is negative-disjoint by X,TARSKI:2;
end;
end;
registration
let R be preordered domRing;
let P be Preordering of R;
cluster Positives(Poly) P -> mult-closed with_sums_of_squares;
coherence
proof
set M = Positives(Poly) P, K = Polynom-Ring R;
X: P + P c= P & P *P c= P & SQ R c= P by defppc;
now let x,y be Element of K;
assume AS: x in M & y in M;
then consider p being Polynomial of R such that
A: x = p & LC p in P;
consider q being Polynomial of R such that
B: y = q & LC q in P by AS;
C1: LC p * LC q in P*P by A,B;
per cases;
suppose p = 0_.(R);
then p *' q = 0_.(R) by POLYNOM3:34;
then LC(p *'q) = 0.R by FUNCOP_1:7;
then LC(p *'q) in P by ord3;
then p*'q in {r where r is Polynomial of R : LC r in P};
hence x * y in M by A,B,POLYNOM3:def 10;
end;
suppose q = 0_.(R);
then p *' q = 0_.(R) by POLYNOM4:2;
then LC(p *'q) = 0.R by FUNCOP_1:7;
then LC(p *'q) in P by ord3;
then p*'q in {r where r is Polynomial of R : LC r in P};
hence x * y in M by A,B,POLYNOM3:def 10;
end;
suppose Z: p <> 0_.(R) & q <> 0_.(R);
then p is non zero & q is non zero;
then LC p <> 0.R & LC q <> 0.R;
then p.(len p -'1) * q.(len q -'1) <> 0.R by VECTSP_2:def 1;
then len(p*'q) = len p + len q - 1 by POLYNOM4:10;
then LC(p*'q) = LC(p) * LC(q) by Z,lemmul;
then p*'q in {r where r is Polynomial of R : LC r in P} by C1,X;
hence x * y in M by A,B,POLYNOM3:def 10;
end;
end;
hence M is mult-closed;
now let o be object;
assume o in SQ K;
then consider a being Element of K such that X1: o = a & a is square;
reconsider p = a as Polynomial of R by POLYNOM3:def 10;
consider b being Element of K such that X2: a = b^2 by X1;
reconsider q = b as Polynomial of R by POLYNOM3:def 10;
X3: p = q *' q by POLYNOM3:def 10,X2;
per cases;
suppose q = 0_.(R);
then p = 0_.(R) by X3,POLYNOM3:34;
then LC p = 0.R by FUNCOP_1:7;
then LC p in P by ord3;
hence o in M by X1;
end;
suppose Z: q <> 0_.(R);
then q is non zero;
then LC q <> 0.R;
then q.(len q -'1) * q.(len q -'1) <> 0.R by VECTSP_2:def 1;
then len(q*'q) = len q + len q - 1 by POLYNOM4:10;
then LC(q*'q) = (LC q)^2 by Z,lemmul;
then LC(q*'q) is square;
then LC(q*'q) in SQ R;
hence o in M by X,X1,X3;
end;
end;
then SQ K c= M;
then M is with_squares;
hence M is with_sums_of_squares;
end;
end;
registration
let R be ordered Ring;
let O be Ordering of R;
cluster Positives(Poly) O -> spanning;
coherence
proof
set P = Positives(Poly) O, K = Polynom-Ring R;
X: now let o be object;
assume o in the carrier of K;
then reconsider p = o as Polynomial of R by POLYNOM3:def 10;
X1: O \/ (-O) = the carrier of R by defpc;
per cases by X1,XBOOLE_0:def 3;
suppose LC p in O;
then p in P;
hence o in P \/ (-P) by XBOOLE_0:def 3;
end;
suppose LC p in -O;
then consider a being Element of R such that A: -a = LC p & a in O;
reconsider b = -p as Element of K by POLYNOM3:def 10;
LC(-p) = (-p).(len(p) -'1) by POLYNOM4:8
.= -(p.(len p -'1)) by BHSP_1:44
.= a by A;
then -p in P by A;
then C: -b in -P;
-b = -(-p) by lemminuspoly .= p by HURWITZ:10;
hence o in P \/ (-P) by C,XBOOLE_0:def 3;
end;
end;
for o be object st o in P \/ (-P) holds o in the carrier of K;
hence thesis by X,TARSKI:2;
end;
end;
registration
let R be preordered domRing;
cluster Polynom-Ring R -> preordered;
coherence
proof
set P = the Preordering of R;
Positives(Poly) P is prepositive_cone;
hence thesis;
end;
end;
registration
let R be ordered domRing;
cluster Polynom-Ring R -> ordered;
coherence
proof
set P = the Ordering of R;
Positives(Poly) P is positive_cone;
hence thesis;
end;
end;
theorem
for R being preordered domRing
for P being Preordering of R
holds Positives(Poly) P is Preordering of Polynom-Ring R;
theorem
for R being ordered domRing
for O being Ordering of R
holds Positives(Poly) O is Ordering of Polynom-Ring R;
definition
let R be preordered Ring;
let P be Preordering of R;
func LowPositives(Poly) P -> Subset of Polynom-Ring R equals
{ p where p is Polynomial of R :
p.(min*{i where i is Nat : p.i <> 0.R}) in P };
coherence
proof
set M = { p where p is Polynomial of R :
p.(min*{i where i is Nat : p.i <> 0.R}) in P };
now let x be object;
assume x in M;
then consider p being Polynomial of R such that
H: x = p & p.(min*{i where i is Nat : p.i <> 0.R}) in P;
thus x in the carrier of Polynom-Ring R by H,POLYNOM3:def 10;
end;
hence thesis by TARSKI:def 3;
end;
end;
lemlowp1:
for R being preordered non degenerated Ring
for P being Preordering of R
for p,q being non zero Polynomial of R
st p.(min*{i where i is Nat : p.i <> 0.R}) in P &
q.(min*{i where i is Nat : q.i <> 0.R}) in P
holds (p+q).(min*{i where i is Nat : (p+q).i <> 0.R}) in P
proof
let R be preordered non degenerated Ring; let P be Preordering of R;
let p,q be non zero Polynomial of R;
assume AS: p.(min*{i where i is Nat : p.i <> 0.R}) in P &
q.(min*{i where i is Nat : q.i <> 0.R}) in P;
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R} as non empty Subset of NAT
by lemlp1;
Z1: P + P c= P & P /\ (-P) = {0.R} by defppc;
now let o be object;
assume o in {i where i is Nat : (p+q).i <> 0.R};
then consider i being Nat such that H1: o = i & (p+q).i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cpq = {i where i is Nat : (p+q).i <> 0.R} as Subset of NAT
by TARSKI:def 3;
per cases by XXREAL_0:1;
suppose AS1: min* cp > min* cq;
not( (min* cq) in cp ) by AS1,NAT_1:def 1;
then p.(min* cq) = 0.R;
then (p+q).(min* cq) = 0.R + q.(min* cq) by NORMSP_1:def 2;
hence thesis by AS1,AS,lemlowp1a1;
end;
suppose AS1: min* cp < min* cq;
not( (min* cp) in cq ) by AS1,NAT_1:def 1;
then q.(min* cp) = 0.R;
then (p+q).(min* cp) = 0.R + p.(min* cp) by NORMSP_1:def 2;
hence thesis by AS1,AS,lemlowp1a1;
end;
suppose XX: min* cp = min* cq;
then D1: (p+q).(min* cp) = p.(min* cp) + q.(min* cq) by NORMSP_1:def 2;
now assume 0.R = p.(min* cp) + q.(min* cp);
then p.(min* cp) = -(q.(min* cp)) by RLVECT_1:6;
then p.(min* cp) in - P by AS,XX;
then Y: p.(min* cp) in P /\ (-P) by AS,XBOOLE_0:def 4;
(min* cp) in cp by NAT_1:def 1;
then consider w1 being Nat such that H2: w1 = min* cp & p.w1 <> 0.R;
thus contradiction by Y,H2,Z1,TARSKI:def 1;
end;
then min* cpq = min( min* cp, min* cq) by XX,lemlowp1b
.= min* cp by XX;
hence thesis by D1,AS,IDEAL_1:def 1;
end;
end;
lemlowp3:
for R being domRing,
p,q being non zero Polynomial of R holds
(p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) =
p.(min*{i where i is Nat : p.i<>0.R}) * q.(min*{i where i is Nat : q.i<>0.R})
proof
let R be domRing, p,q be non zero Polynomial of R;
reconsider cp = {i where i is Nat : p.i <> 0.R},
cq = {i where i is Nat : q.i <> 0.R},
cpq = {i where i is Nat : (p*'q).i <> 0.R}
as non empty Subset of NAT by lemlp1;
set m = min* cp + min* cq;
consider r being FinSequence of the carrier of R such that
M: len r = m+1 & (p*'q).m = Sum r &
for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(m+1-'k)
by POLYNOM3:def 9;
B1: 1 <= min* cp + 1 by NAT_1:11;
min* cp + 1 <= (min* cp + 1) + min* cq by NAT_1:11;
then A1: min* cp + 1 in dom r by M,B1,FINSEQ_3:25;
A2: (min* cp + 1) - 1 >= 0;
A4: m+1-'(min* cp + 1) = m+1-(min* cp + 1) by XREAL_0:def 2;
now let k be Element of NAT;
assume E: k in dom r & k <> min* cp + 1;
then EE: 1 <= k <= m + 1 by M,FINSEQ_3:25;
per cases by E,XXREAL_0:1;
suppose E1: k < min* cp + 1;
reconsider k1 = k - 1 as Element of NAT by EE,INT_1:3;
E4: k -' 1 = k - 1 by EE,XREAL_0:def 2;
then E3: k -' 1 < (min* cp + 1) - 1 by E1,XREAL_1:9;
now assume p.k1 <> 0.R;
then k1 in cp;
hence contradiction by E3,E4,NAT_1:def 1;
end;
then r.k = 0.R * q.(m+1-'k) by E4,E,M;
hence r/.k = 0.R by E,PARTFUN1:def 6;
end;
suppose k > min* cp + 1;
then E1: m + 1 - k < m + 1 - (min* cp + 1) by XREAL_1:10;
m + 1 - k in NAT by EE,INT_1:5;
then E3: m + 1 -' k < min* cq by E1,XREAL_0:def 2;
now assume q.(m+1-'k) <> 0.R;
then m+1-'k in cq;
hence contradiction by E3,NAT_1:def 1;
end;
then r.k = p.(k-'1) * 0.R by E,M;
hence r/.k = 0.R by E,PARTFUN1:def 6;
end;
end;
then Sum r = r/.(min* cp + 1) by A1,POLYNOM2:3
.= r.(min* cp + 1) by A1,PARTFUN1:def 6
.= p.((min* cp + 1)-'1) * q.(m+1-'(min* cp + 1)) by A1,M
.= p.(min* cp) * q.(min* cq) by A4,A2,XREAL_0:def 2;
hence thesis by M,lemlowp3b;
end;
registration
let R be preordered non degenerated Ring;
let P be Preordering of R;
cluster LowPositives(Poly) P -> add-closed negative-disjoint;
coherence
proof
set M = LowPositives(Poly) P, K = Polynom-Ring R;
X2: 0.R in P by ord3;
now let x,y be Element of K;
assume AS: x in M & y in M;
then consider p being Polynomial of R such that
H1: x = p & p.(min*{i where i is Nat : p.i <> 0.R}) in P;
consider q being Polynomial of R such that
H2: y = q & q.(min*{i where i is Nat : q.i <> 0.R}) in P by AS;
per cases;
suppose A: p is zero;
B: min*{i where i is Nat : (p+q).i <> 0.R}
= min*{i where i is Nat : q.i <> 0.R} by lemlowp0,A;
(p+q).(min*{i where i is Nat : q.i <> 0.R})
= q.(min*{i where i is Nat : q.i <> 0.R}) by A,POLYNOM3:28;
then p+q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P} by B,H2;
hence x + y in M by H1,H2,POLYNOM3:def 10;
end;
suppose A: q is zero;
then B: min*{i where i is Nat : (p+q).i <> 0.R}
= min*{i where i is Nat : p.i <> 0.R} by lemlowp0;
(p+q).(min*{i where i is Nat : p.i <> 0.R})
= p.(min*{i where i is Nat : p.i <> 0.R}) by A,POLYNOM3:28;
then p+q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P} by B,H1;
hence x + y in M by H1,H2,POLYNOM3:def 10;
end;
suppose p is non zero & q is non zero;
then (p+q).(min*{i where i is Nat : (p+q).i <> 0.R}) in P
by H1,H2,lemlowp1;
then p+q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P};
hence x + y in M by H1,H2,POLYNOM3:def 10;
end;
end;
hence M is add-closed;
X: now let o be object;
assume X00: o in {0.K};
then X0: o = 0.K by TARSKI:def 1;
then X1: o = 0_.(R) by POLYNOM3:def 10;
reconsider q = o as Polynomial of R by X00,POLYNOM3:def 10;
q.(min* {i where i is Nat : q.i <> 0.R}) = 0.R by X1,FUNCOP_1:7;
then X3: q in M by X2;
reconsider q as Element of K by POLYNOM3:def 10;
-q in {-p where p is Element of K : p in M} by X3;
hence o in M /\ (-M) by X0,X3,XBOOLE_0:def 4;
end;
now let o be object;
assume o in M /\ (-M);
then X1: o in M & o in -M by XBOOLE_0:def 4;
then consider p being Polynomial of R such that
X2: o = p & p.(min*{i where i is Nat : p.i <> 0.R}) in P;
set V = {i where i is Nat : p.i <> 0.R};
consider x being Element of K such that X3: o = -x & x in M by X1;
consider q being Polynomial of R such that
X4: x = q & q.(min*{i where i is Nat : q.i <> 0.R}) in P by X3;
X8: now let o be object;
assume o in {i where i is Nat : p.i <> 0.R};
then consider i being Nat such that H1: o = i & p.i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
now assume {i where i is Nat : p.i <> 0.R} <> {};
then reconsider cp = {i where i is Nat : p.i <> 0.R} as
non empty Subset of NAT by X8,TARSKI:def 3;
min* cp in cp by NAT_1:def 1;
then consider i being Nat such that X9: i = min* cp & p.i <> 0.R;
X15: -(-x) = x;
then X13: q.i = (-p).i by X4,X3,X2,lemminuspoly .= -(p.i) by BHSP_1:44;
now assume q.i = 0.R;
then -(-(p.i)) = - 0.R by X13;
hence contradiction by X9;
end;
then X11: i in {i where i is Nat : q.i <> 0.R};
now let o be object;
assume o in {i where i is Nat : q.i <> 0.R};
then consider i being Nat such that H1: o = i & q.i <> 0.R;
thus o in NAT by H1,ORDINAL1:def 12;
end;
then reconsider cq = {i where i is Nat : q.i <> 0.R} as
non empty Subset of NAT by X11,TARSKI:def 3;
now let k be Nat;
assume k in {i where i is Nat : q.i <> 0.R};
then consider j being Nat such that X14: k = j & q.j <> 0.R;
q.j = (-p).j by X15,X4,X3,X2,lemminuspoly .= -(p.j) by BHSP_1:44;
then p.j <> 0.R by X14;
then j in cp;
hence i <= k by X14,X9,NAT_1:def 1;
end;
then min* cq = i by X11,NAT_1:def 1;
then p.i = (-q).(min*{i where i is Nat : q.i <> 0.R})
by X4,X3,X2,lemminuspoly
.= -(q.(min*{i where i is Nat : q.i <> 0.R})) by BHSP_1:44;
then p.(min*{i where i is Nat : p.i<>0.R}) in -P by X4,X9;
then p.(min*{i where i is Nat : p.i <> 0.R}) in P /\ (-P)
by X2,XBOOLE_0:def 4;
then p.(min*{i where i is Nat : p.i <> 0.R}) in {0.R} by defppc;
hence contradiction by X9,TARSKI:def 1;
end;
then p = 0_.(R) by lemlp0 .= 0.K by POLYNOM3:def 10;
hence o in {0.K} by X2,TARSKI:def 1;
end;
hence M is negative-disjoint by X,TARSKI:2;
end;
end;
registration
let R be preordered domRing;
let P be Preordering of R;
cluster LowPositives(Poly) P -> mult-closed with_sums_of_squares;
coherence
proof
set M = LowPositives(Poly) P, K = Polynom-Ring R;
X: P + P c= P & P *P c= P & SQ R c= P by defppc;
now let x,y be Element of K;
assume AS: x in M & y in M;
then consider p being Polynomial of R such that
A: x = p & p.(min*{i where i is Nat : p.i <> 0.R}) in P;
consider q being Polynomial of R such that
B: y = q & q.(min*{i where i is Nat : q.i <> 0.R}) in P by AS;
C1: p.(min*{i where i is Nat : p.i <> 0.R}) *
q.(min*{i where i is Nat : q.i <> 0.R}) in P*P by A,B;
per cases;
suppose p = 0_.(R);
then p *' q = 0_.(R) by POLYNOM3:34;
then (p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) = 0.R
by FUNCOP_1:7;
then (p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) in P by ord3;
then p*'q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P};
hence x * y in M by A,B,POLYNOM3:def 10;
end;
suppose q = 0_.(R);
then p *' q = 0_.(R) by POLYNOM4:2;
then (p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) = 0.R
by FUNCOP_1:7;
then (p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) in P by ord3;
then p*'q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P};
hence x * y in M by A,B,POLYNOM3:def 10;
end;
suppose p <> 0_.(R) & q <> 0_.(R);
then p is non zero & q is non zero;
then (p*'q).(min*{i where i is Nat : (p*'q).i <> 0.R}) in P*P
by C1,lemlowp3;
then p*'q in {r where r is Polynomial of R :
r.(min*{i where i is Nat : r.i <> 0.R}) in P} by X;
hence x * y in M by A,B,POLYNOM3:def 10;
end;
end;
hence M is mult-closed;
now let o be object;
assume o in SQ K;
then consider a being Element of K such that X1: o = a & a is square;
reconsider p = a as Polynomial of R by POLYNOM3:def 10;
consider b being Element of K such that X2: a = b^2 by X1;
reconsider q = b as Polynomial of R by POLYNOM3:def 10;
X3: p = q *' q by POLYNOM3:def 10,X2;
per cases;
suppose q = 0_.(R);
then p = 0_.(R) by X3,POLYNOM3:34;
then p.(min*{i where i is Nat : p.i <> 0.R}) = 0.R by FUNCOP_1:7;
then p.(min*{i where i is Nat : p.i <> 0.R}) in P by ord3;
hence o in M by X1;
end;
suppose q <> 0_.(R);
then reconsider qq = q as non zero Polynomial of R by UPROOTS:def 5;
(q*'q).(min*{i where i is Nat : (qq*'qq).i <> 0.R}) =
q.(min*{i where i is Nat : qq.i<>0.R}) *
q.(min*{i where i is Nat : qq.i<>0.R}) by lemlowp3;
then (q*'q).(min*{i where i is Nat : (q*'q).i <> 0.R})
= (q.(min*{i where i is Nat : q.i<>0.R}))^2;
then (q*'q).(min*{i where i is Nat : (q*'q).i <> 0.R}) is square;
then (q*'q).(min*{i where i is Nat : (q*'q).i <> 0.R}) in SQ R;
hence o in M by X,X1,X3;
end;
end;
then SQ K c= M;
then M is with_squares;
hence M is with_sums_of_squares;
end;
end;
registration
let R be ordered non degenerated Ring;
let O be Ordering of R;
cluster LowPositives(Poly) O -> spanning;
coherence
proof
set P = LowPositives(Poly) O, K = Polynom-Ring R;
X: now let o be object;
assume o in the carrier of K;
then reconsider p = o as Polynomial of R by POLYNOM3:def 10;
X1: O \/ (-O) = the carrier of R by defpc;
per cases by X1,XBOOLE_0:def 3;
suppose p.(min*{i where i is Nat : p.i<>0.R}) in O;
then p in P;
hence o in P \/ (-P) by XBOOLE_0:def 3;
end;
suppose p.(min*{i where i is Nat : p.i<>0.R}) in -O;
then consider a being Element of R such that
A: -a = p.(min*{i where i is Nat : p.i<>0.R}) & a in O;
reconsider b = -p as Element of K by POLYNOM3:def 10;
(-p).(min*{i where i is Nat : (-p).i<>0.R})
= -(p.(min*{i where i is Nat : (-p).i<>0.R})) by BHSP_1:44
.= -(p.(min*{i where i is Nat : p.i<>0.R})) by lemlowp2
.= a by A;
then -p in P by A;
then C: -b in -P;
-b = -(-p) by lemminuspoly .= p by HURWITZ:10;
hence o in P \/ (-P) by C,XBOOLE_0:def 3;
end;
end;
for o be object st o in P \/ (-P) holds o in the carrier of K;
hence thesis by X,TARSKI:2;
end;
end;
theorem
for R being preordered domRing
for P being Preordering of R
holds LowPositives(Poly) P is Preordering of Polynom-Ring R;
theorem
for R being ordered domRing
for O being Ordering of R
holds LowPositives(Poly) O is Ordering of Polynom-Ring R;
theorem
for R being preordered non degenerated Ring
for P being Preordering of R
holds Positives(Poly) P <> LowPositives(Poly) P
proof
let R be preordered non degenerated Ring, P be Preordering of R;
set p = rpoly(1,1.R);
reconsider cp = {i where i is Nat : p.i <> 0.R} as non empty Subset of NAT
by lemlp1;
deg p = 1 by HURWITZ:27;
then len p -' 1 = 1 by XREAL_0:def 2;
then p.(len p-'1) = 1_R by HURWITZ:25;
then B: LC p = 1.R;
A: 1.R in P by ord3;
E: p.0 = -(power(R).(1.R,0+1)) by HURWITZ:25
.= -((power(R).(1.R,0)) * 1.R) by GROUP_1:def 7
.= -(1_R * 1.R) by GROUP_1:def 7
.= - 1.R;
now assume - 1.R = 0.R;
then -(-1.R) = 0.R;
hence contradiction;
end;
then 0 in cp by E;
then C: min* cp = 0 by NAT_1:def 1;
now assume p in LowPositives(Poly) P;
then consider q being Polynomial of R such that
H: q = p & q.(min*{i where i is Nat : q.i <> 0.R}) in P;
thus contradiction by H,C,E,ord4;
end;
hence thesis by A,B;
end;