:: Polynomial Reduction :: by Christoph Schwarzweller :: :: Received December 20, 2002 :: Copyright (c) 2002-2018 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 NUMBERS, ORDINAL1, ZFMISC_1, STRUCT_0, VALUED_0, POLYNOM7, SUBSET_1, RELAT_1, SUPINF_2, POLYNOM1, VECTSP_1, ORDERS_1, TARSKI, PRE_POLY, ARYTM_3, FUNCT_1, ALGSEQ_1, NAT_1, FINSET_1, CARD_1, XXREAL_0, XBOOLE_0, RLVECT_1, ALGSTR_0, FINSEQ_1, CARD_3, PARTFUN1, ORDINAL4, ARYTM_1, ALGSTR_1, LATTICES, VECTSP_2, BINOP_1, CAT_3, RELAT_2, BAGORDER, TERMORD, XCMPLX_0, BROUWER, ORDERS_2, WELLORD1, FINSUB_1, WAYBEL_4, MESFUNC1, REWRITE1, INT_1, IDEAL_1, POLYRED; notations CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XXREAL_0, STRUCT_0, ALGSTR_0, ALGSTR_1, WAYBEL_0, FINSUB_1, WAYBEL_4, REWRITE1, RLVECT_1, FINSEQ_1, XTUPLE_0, MCART_1, ORDERS_1, VFUNCT_1, GROUP_1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1, IDEAL_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD, PRE_POLY; constructors REWRITE1, VECTSP_2, TRIANG_1, WAYBEL_4, WELLFND1, IDEAL_1, BAGORDER, TERMORD, DOMAIN_1, RELSET_1, BINOP_2, FVSUM_1, VFUNCT_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, FINSUB_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, BAGORDER, TERMORD, VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1, RELSET_1; requirements NUMERALS, REAL, SUBSET, BOOLE; definitions POLYNOM7; equalities STRUCT_0, POLYNOM7, ALGSTR_0; expansions STRUCT_0, POLYNOM7; theorems TARSKI, RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1, BINOM, RLVECT_1, VECTSP_2, FINSET_1, NAT_1, POLYNOM2, ALGSTR_1, RELAT_2, CARD_1, CARD_2, WAYBEL_0, ORDERS_2, ORDERS_1, POLYNOM7, FINSUB_1, WELLORD1, WELLFND1, REWRITE1, WAYBEL_4, XBOOLE_0, XBOOLE_1, MATRLIN, IDEAL_1, BAGORDER, TERMORD, XCMPLX_1, GROUP_1, XREAL_1, XXREAL_0, PARTFUN1, STRUCT_0, PRE_POLY, XTUPLE_0; schemes NAT_1, RELSET_1; begin :: Preliminaries registration let n be Ordinal, R be non trivial ZeroStr; cluster non-zero for Monomial of n,R; existence proof set a = the Element of NonZero R; reconsider a as Element of R; take q = a |(n,R); A1: a <> 0.R & 0_(n,R) = 0.R |(n,R) by POLYNOM7:19,ZFMISC_1:56; assume q = 0_(n,R); hence contradiction by A1,POLYNOM7:21; end; end; registration cluster non trivial for Field; existence proof set F = the Field; take F; thus thesis; end; end; Lm1: for X being set, S being Subset of X, R being Order of X st R is being_linear-order holds R linearly_orders S proof let X be set, S be Subset of X, R be Order of X; S c= X; then A1: S c= field R by ORDERS_1:15; assume R is being_linear-order; hence thesis by A1,ORDERS_1:37,38; end; Lm2: for n being Ordinal, b1,b2,b3 being bag of n holds b1 <=' b2 implies b1 + b3 <=' b2 + b3 proof let n be Ordinal, b1,b2,b3 be bag of n; assume A1: b1 <=' b2; per cases; suppose b1 = b2; hence thesis; end; suppose b1 <> b2; then b1 < b2 by A1,PRE_POLY:def 10; then consider k being Ordinal such that A2: b1.k < b2.k and A3: for l being Ordinal st l in k holds b1.l = b2.l by PRE_POLY:def 9; A4: now let l be Ordinal; assume A5: l in k; thus (b1 + b3).l = b1.l + b3.l by PRE_POLY:def 5 .= b2.l + b3.l by A3,A5 .= (b2 + b3).l by PRE_POLY:def 5; end; (b1 + b3).k = b1.k + b3.k & (b2 + b3).k = b2.k + b3.k by PRE_POLY:def 5; then (b1 + b3).k < (b2 + b3).k by A2,XREAL_1:8; then (b1 + b3) < (b2 + b3) by A4,PRE_POLY:def 9; hence thesis by PRE_POLY:def 10; end; end; Lm3: for n being Ordinal, b1,b2 being bag of n holds b1 <=' b2 & b2 <=' b1 implies b1 = b2 proof let n be Ordinal, b1,b2 be bag of n; assume that A1: b1 <=' b2 and A2: b2 <=' b1; now assume A3: b1 <> b2; then b1 < b2 by A1,PRE_POLY:def 10; hence contradiction by A2,A3,PRE_POLY:def 10; end; hence thesis; end; Lm4: for n being Ordinal, b1,b2 being bag of n holds not b1 < b2 iff b2 <=' b1 proof let n be Ordinal, b1,b2 be bag of n; A1: now assume A2: not b1 < b2; now per cases; case b1 = b2; hence b2 <=' b1; end; case b1 <> b2; then not b1 <=' b2 by A2,PRE_POLY:def 10; hence b2 <=' b1 by PRE_POLY:45; end; end; hence b2 <=' b1; end; now assume A3: b2 <=' b1; now per cases; case b2 <> b1; hence not b1 < b2 by A3,PRE_POLY:def 10; end; case b1 = b2; hence not(ex k being Ordinal st b1.k < b2.k & for l being Ordinal st l in k holds b1.l = b2.l); end; end; hence not b1 < b2; end; hence thesis by A1; end; Lm5: for n being Ordinal, L being non trivial ZeroStr, p being non-zero finite-Support Series of n,L holds ex b being bag of n st p.b <> 0.L & for b9 being bag of n st b < b9 holds p.b9 = 0.L proof let n be Ordinal, L be non trivial ZeroStr, p be non-zero finite-Support Series of n,L; defpred P[Nat] means for B being finite Subset of Bags n st card B = \$1 holds ex b being bag of n st b in B & for b9 being bag of n st b9 in B holds b9 <=' b; A1: for k being Nat st 1 <= k holds P[k] implies P[k+1] proof let k be Nat; assume A2: 1 <= k; thus P[k] implies P[k+1] proof assume A3: P[k]; thus P[k+1] proof let B be finite Subset of Bags n; assume A4: card B = k + 1; then reconsider B as non empty finite Subset of Bags n; set x = the Element of B; reconsider x as Element of Bags n; reconsider x as bag of n; set X = B \ {x}; now let u be object; assume u in {x}; then u = x by TARSKI:def 1; hence u in B; end; then {x} c= B by TARSKI:def 3; then A5: B = {x} \/ B by XBOOLE_1:12 .= {x} \/ X by XBOOLE_1:39; x in X iff x in B & not x in {x} by XBOOLE_0:def 5; then A6: card(X) + 1 = k + 1 by A4,A5,CARD_2:41,TARSKI:def 1; then reconsider X as non empty set by A2,XCMPLX_1:2; reconsider X as non empty finite Subset of Bags n; consider b being bag of n such that A7: b in X and A8: for b9 being bag of n st b9 in X holds b9 <=' b by A3,A6,XCMPLX_1:2; A9: now per cases by PRE_POLY:45; case A10: x <=' b; now let b9 be bag of n; assume A11: b9 in B; now per cases; case b9 in X; hence b9 <=' b by A8; end; case not b9 in X; then b9 in {x} by A5,A11,XBOOLE_0:def 3; hence b9 <=' b by A10,TARSKI:def 1; end; end; hence b9 <=' b; end; hence for b9 being bag of n st b9 in B holds b9 <=' b; end; case A12: b <=' x; now let b9 be bag of n; assume A13: b9 in B; now per cases; case b9 in X; then b9 <=' b by A8; hence b9 <=' x by A12,PRE_POLY:42; end; case not b9 in X; then b9 in {x} by A5,A13,XBOOLE_0:def 3; hence b9 <=' x by TARSKI:def 1; end; end; hence b9 <=' x; end; hence for b9 being bag of n st b9 in B holds b9 <=' x; end; end; b in B by A5,A7,XBOOLE_0:def 3; hence thesis by A9; end; end; end; reconsider sp = Support p as finite set by POLYNOM1:def 5; A14: Support p is finite Subset of Bags n by POLYNOM1:def 5; card sp is finite; then consider m being Nat such that A15: card(Support p) = card m by CARD_1:48; p <> 0_(n,L) by POLYNOM7:def 1; then Support p <> {} by POLYNOM7:1; then m <> 0 by A15; then A16: 1 <= m by NAT_1:14; A17: card(Support p) = m by A15; A18: P[1] proof let B be finite Subset of Bags n; assume card B = 1; then card {{}} = card B by CARD_1:30; then consider b being object such that A19: B = {b} by CARD_1:29; A20: b in B by A19,TARSKI:def 1; then reconsider b as Element of Bags n; reconsider b as bag of n; for b9 being bag of n st b9 in B holds b9 <=' b by A19,TARSKI:def 1; hence thesis by A20; end; for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A18,A1); then consider b being bag of n such that A21: b in Support p and A22: for b9 being bag of n st b9 in Support p holds b9 <=' b by A17,A16,A14; A23: now let b9 be bag of n; assume b < b9; then not b9 <=' b by Lm4; then A24: not b9 in Support p by A22; b9 is Element of Bags n by PRE_POLY:def 12; hence p.b9 = 0.L by A24,POLYNOM1:def 4; end; p.b <> 0.L by A21,POLYNOM1:def 4; hence thesis by A23; end; Lm6: for L being Abelian add-associative right_zeroed right_complementable non empty addLoopStr, f,g being FinSequence of the carrier of L, n being Nat st len f = n + 1 & g = f|(Seg n) holds Sum f = Sum g + f/.(len f) proof let L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, f,g be FinSequence of the carrier of L, n be Nat; assume that A1: len f = n + 1 and A2: g = f|(Seg n); A3: n <= len f by A1,NAT_1:11; set q = <*(f/.(len f))*>; set p = g^q; A4: len q = 1 by FINSEQ_1:39; A5: dom f = Seg(n+1) by A1,FINSEQ_1:def 3; A6: now let u be object; assume A7: u in dom f; then u in { k where k is Nat : 1 <= k & k <= n+1 } by A5,FINSEQ_1:def 1; then consider i being Nat such that A8: u = i and A9: 1 <= i and A10: i <= n+1; now per cases; case A11: i = n+1; then len g + 1 <= i & i <= len g + len q by A2,A3,A4,FINSEQ_1:17; hence p.i = q.(i-len g) by FINSEQ_1:23 .= q.(n+1-n) by A2,A3,A11,FINSEQ_1:17 .= q.1 by XCMPLX_1:26 .= f/.(n+1) by A1,FINSEQ_1:40 .= f.i by A7,A8,A11,PARTFUN1:def 6; end; case i <> n+1; then i < n+1 by A10,XXREAL_0:1; then i <= n by NAT_1:13; then i in { k where k is Nat : 1 <= k & k <= n } by A9; then i in Seg n by FINSEQ_1:def 1; then A12: i in dom g by A2,A3,FINSEQ_1:17; then p.i = g.i by FINSEQ_1:def 7; hence p.i = f.i by A2,A12,FUNCT_1:47; end; end; hence f.u = p.u by A8; end; len(g^q) = len g + len q by FINSEQ_1:22 .= len g + 1 by FINSEQ_1:40 .= len f by A1,A2,A3,FINSEQ_1:17; then dom f = Seg(len(g^q)) by FINSEQ_1:def 3 .= dom(g^q) by FINSEQ_1:def 3; then f = g^<*(f/.(len f))*> by A6,FUNCT_1:2; hence Sum f = Sum g + Sum <*(f/.(len f))*> by RLVECT_1:41 .= Sum g + (f/.(len f)) by RLVECT_1:44; end; registration let n be Ordinal, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p,q be non-zero finite-Support Series of n,L; cluster p *' q -> non-zero; coherence proof consider b22 being bag of n such that A1: q.b22 <> 0.L and A2: for b9 being bag of n st b22 < b9 holds q.b9 = 0.L by Lm5; consider b11 being bag of n such that A3: p.b11 <> 0.L and A4: for b9 being bag of n st b11 < b9 holds p.b9 = 0.L by Lm5; set b = b11 + b22; consider s being FinSequence of the carrier of L such that A5: (p*'q).b = Sum s and A6: len s = len decomp b and A7: for k being Element of NAT st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by POLYNOM1:def 10; A8: b is Element of Bags n & p.b11 * q.b22 <> 0.L by A3,A1,PRE_POLY:def 12 ,VECTSP_2:def 1; consider S being non empty finite Subset of Bags n such that A9: divisors b = SgmX(BagOrder n, S) and A10: for p being bag of n holds p in S iff p divides b by PRE_POLY:def 16; set sgm = SgmX(BagOrder n, S); A11: BagOrder n linearly_orders S by Lm1; b11 divides b by PRE_POLY:50; then b11 in S by A10; then b11 in rng(sgm) by A11,PRE_POLY:def 2; then consider i being object such that A12: i in dom sgm and A13: sgm.i = b11 by FUNCT_1:def 3; A14: i in dom decomp b by A9,A12,PRE_POLY:def 17; (divisors b)/.i = b11 by A9,A12,A13,PARTFUN1:def 6; then A15: (decomp b)/.i = <*b11, b-'b11*> by A14,PRE_POLY:def 17; then A16: (decomp b)/.i = <*b11, b22*> by PRE_POLY:48; A17: dom s = Seg(len decomp b) by A6,FINSEQ_1:def 3 .= dom(decomp b) by FINSEQ_1:def 3; then A18: i in dom s by A9,A12,PRE_POLY:def 17; reconsider i as Element of NAT by A12; consider b1,b2 being bag of n such that A19: (decomp b)/.i = <*b1, b2*> and A20: s/.i = p.b1*q.b2 by A7,A18; A21: b2 = <*b11,b22*>.2 by A16,A19,FINSEQ_1:44 .= b22 by FINSEQ_1:44; A22: now let k be Element of NAT; assume that A23: k in dom s and A24: k <> i; consider b1,b2 being bag of n such that A25: (decomp b)/.k = <*b1, b2*> and A26: s/.k = p.b1*q.b2 by A7,A23; consider b19, b29 being bag of n such that A27: (decomp b)/.k = <*b19, b29*> and A28: b = b19+b29 by A17,A23,PRE_POLY:68; A29: b2 = <*b19, b29*>.2 by A27,A25,FINSEQ_1:44 .= b29 by FINSEQ_1:44; A30: b1 = <*b19, b29*>.1 by A27,A25,FINSEQ_1:44 .= b19 by FINSEQ_1:44; A31: now assume that A32: p.b1 <> 0.L and A33: q.b2 <> 0.L; not b11 < b1 by A4,A32; then A34: b1 <=' b11 by Lm4; not b22 < b2 by A2,A33; then A35: b2 <=' b22 by Lm4; A36: now assume b1 = b11 & b2 = b22; then (decomp b).k = <*b11,b22*> by A17,A23,A25,PARTFUN1:def 6 .= (decomp b)/.i by A15,PRE_POLY:48 .= (decomp b).i by A14,PARTFUN1:def 6; hence contradiction by A14,A17,A23,A24,FUNCT_1:def 4; end; now per cases by A36; case A37: b1 <> b11; A38: now assume b1+b2 = b11+b2; then b1 = (b11+b2)-'b2 by PRE_POLY:48; hence contradiction by A37,PRE_POLY:48; end; b11+b22 <=' b11+b2 & b11+b2 <=' b11+b22 by A28,A30,A29,A34,A35,Lm2; hence contradiction by A28,A30,A29,A38,Lm3; end; case A39: b2 <> b22; A40: now assume b2+b1 = b22+b1; then b2 = (b22+b1)-'b1 by PRE_POLY:48; hence contradiction by A39,PRE_POLY:48; end; b11+b22 <=' b22+b1 & b22+b1 <=' b11+b22 by A28,A30,A29,A34,A35,Lm2; hence contradiction by A28,A30,A29,A40,Lm3; end; end; hence contradiction; end; now per cases by A31; case p.b1 = 0.L; hence p.b1*q.b2 = 0.L; end; case q.b2 = 0.L; hence p.b1*q.b2 = 0.L; end; end; hence s/.k = 0.L by A26; end; b1 = <*b11,b22*>.1 by A16,A19,FINSEQ_1:44 .= b11 by FINSEQ_1:44; then (p*'q).b = p.b11 * q.b22 by A5,A18,A22,A20,A21,POLYNOM2:3; then b in Support(p*'q) by A8,POLYNOM1:def 4; then p*'q <> 0_(n,L) by POLYNOM7:1; hence thesis; end; end; begin :: More on Polynomials and Monomials theorem Th1: for X being set, L being Abelian add-associative right_zeroed right_complementable non empty addLoopStr, p,q being Series of X, L holds -(p + q) = (-p) + (-q) proof let n be set, L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, p,q be Series of n,L; A1: now let x be object; assume x in dom -(p+q); then reconsider b = x as bag of n; ((-p) + (-q)).b = (-p).b + (-q).b by POLYNOM1:15 .= -(p.b) + (-q).b by POLYNOM1:17 .= -(p.b) + -(q.b) by POLYNOM1:17 .= -(q.b + p.b) by RLVECT_1:31 .= -((p+q).b) by POLYNOM1:15 .= (-(p+q)).b by POLYNOM1:17; hence (-(p+q)).x = ((-p) + (-q)).x; end; dom (-(p+q)) = Bags n by FUNCT_2:def 1 .= dom ((-p) + (-q)) by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th2: for X being set, L being left_zeroed non empty addLoopStr, p being Series of X, L holds 0_(X,L) + p = p proof let n be set, L be left_zeroed non empty addLoopStr, p be Series of n, L; reconsider ls = 0_(n,L) + p, p9 = p as Function of (Bags n), the carrier of L; now let b be Element of Bags n; thus ls.b = 0_(n,L).b + p.b by POLYNOM1:15 .= 0.L + p9.b by POLYNOM1:22 .= p9.b by ALGSTR_1:def 2; end; hence thesis by FUNCT_2:63; end; theorem Th3: for X being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p being Series of X, L holds -p + p = 0_(X,L) & p + -p = 0_(X,L) proof let n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L; set q = -p + p; now let b be Element of Bags n; thus q.b = (-p).b + p.b by POLYNOM1:15 .= -(p.b) + p.b by POLYNOM1:17 .= 0.L by RLVECT_1:5 .= (0_(n,L)).b by POLYNOM1:22; end; hence -p + p = 0_(n,L) by FUNCT_2:63; set q = p + -p; now let b be Element of Bags n; thus q.b = p.b + (-p).b by POLYNOM1:15 .= p.b + -p.b by POLYNOM1:17 .= 0.L by RLVECT_1:5 .= (0_(n,L)).b by POLYNOM1:22; end; hence thesis by FUNCT_2:63; end; theorem Th4: for n being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds p - 0_(n ,L) = p proof let n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L; reconsider pp = p-0_(n,L) as Function of Bags n,the carrier of L; now let b be Element of Bags n; thus pp.b = (p+-0_(n,L)).b by POLYNOM1:def 7 .= p.b + (-0_(n,L)).b by POLYNOM1:15 .= p.b + -((0_(n,L)).b) by POLYNOM1:17 .= p.b + -0.L by POLYNOM1:22 .= p.b - 0.L .= p.b by RLVECT_1:13; end; hence thesis by FUNCT_2:63; end; theorem Th5: for n being Ordinal, L being add-associative right_complementable right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p being Series of n,L holds 0_(n,L) *' p = 0_(n,L) proof let n be Ordinal, L be add-associative right_complementable right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of n,L; set Z = 0_(n,L); now let b be Element of Bags n; consider s being FinSequence of the carrier of L such that A1: (Z*'p).b = Sum s and len s = len decomp b and A2: for k being Element of NAT st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = Z.b1*p.b2 by POLYNOM1:def 10; now let k be Nat; assume k in dom s; then consider b1,b2 being bag of n such that (decomp b)/.k = <*b1, b2*> and A3: s/.k = Z.b1*p.b2 by A2; thus s/.k = 0.L*p.b2 by A3,POLYNOM1:22 .= 0.L; end; then Sum s = 0.L by MATRLIN:11; hence (Z*'p).b = Z.b by A1,POLYNOM1:22; end; hence thesis by FUNCT_2:63; end; Lm7: for n being Ordinal, L being Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p being Polynomial of n,L, q being Element of Polynom-Ring(n,L) st p = q holds -p = -q proof let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p be Polynomial of n,L, q be Element of Polynom-Ring(n, L); set R = Polynom-Ring(n,L); reconsider x = -p as Element of R by POLYNOM1:def 11; reconsider x as Element of R; assume p = q; then x + q = -p + p by POLYNOM1:def 11 .= 0_(n,L) by Th3 .= 0.R by POLYNOM1:def 11; hence thesis by RLVECT_1:6; end; theorem Th6: for n being Ordinal, L being Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p,q being Polynomial of n,L holds -(p *' q) = (-p) *' q & -(p *' q) = p *' (-q) proof let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p,q be Polynomial of n,L; reconsider p9 = p, q9 = q as Element of Polynom-Ring(n,L) by POLYNOM1:def 11; reconsider p9,q9 as Element of Polynom-Ring(n,L); A1: p9 * q9 = p *' q by POLYNOM1:def 11; -p = -p9 by Lm7; then A2: (-p9) * q9 = (-p) *' q by POLYNOM1:def 11; -q = -q9 by Lm7; then A3: p9 * (-q9) = p *' (-q) by POLYNOM1:def 11; -(p9 * q9) = (-p9) * q9 & -(p9 * q9) = p9 * (-q9) by VECTSP_1:9; hence thesis by A2,A3,A1,Lm7; end; Lm8: for n being Ordinal, L being add-associative right_complementable right_zeroed non empty addLoopStr, p being Polynomial of n,L, m being Monomial of n,L, b being bag of n st b <> term(m) holds m.b = 0.L proof let n be Ordinal, L be add-associative right_complementable right_zeroed non empty addLoopStr, p be Polynomial of n,L, m be Monomial of n,L, b be bag of n; assume A1: b <> term(m); per cases by POLYNOM7:7; suppose Support m = {}; then m = 0_(n,L) by POLYNOM7:1; hence thesis by POLYNOM1:22; end; suppose A2: Support(m) = {term(m)}; A3: b is Element of Bags n by PRE_POLY:def 12; not b in Support m by A1,A2,TARSKI:def 1; hence thesis by A3,POLYNOM1:def 4; end; end; theorem Th7: for n being Ordinal, L being add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p being Polynomial of n,L, m being Monomial of n,L, b being bag of n holds (m*'p).(term(m)+b) = m.term(m) * p.b proof let n be Ordinal, L be add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p be Polynomial of n,L, m be Monomial of n,L, b2 be bag of n; set q = m*'p, b = term(m)+b2; consider s being FinSequence of the carrier of L such that A1: q.b = Sum s and A2: len s = len decomp b and A3: for k being Element of NAT st k in dom s ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = m.b1*p.b2 by POLYNOM1:def 10; consider k being Element of NAT such that A4: k in dom decomp b and A5: (decomp(term(m)+b2))/.k = <*term(m),b2*> by PRE_POLY:69; A6: dom s = Seg(len s) by FINSEQ_1:def 3 .= dom decomp(term(m)+b2) by A2,FINSEQ_1:def 3; then consider b19,b29 being bag of n such that A7: (decomp(term(m)+b2))/.k = <*b19,b29*> and A8: s/.k = m.b19 * p.b29 by A3,A4; A9: b2 = <*term(m),b2*>.2 by FINSEQ_1:44 .= b29 by A5,A7,FINSEQ_1:44; A10: for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.k9 = 0.L proof let k9 be Element of NAT; assume that A11: k9 in dom s and A12: k9 <> k; consider b19,b29 being bag of n such that A13: (decomp(term(m)+b2))/.k9 = <*b19,b29*> and A14: s/.k9 = m.b19 * p.b29 by A3,A11; A15: b19 = (divisors b)/.k9 by A6,A11,A13,PRE_POLY:70; A16: b-'b19 = <*b19,b-'b19*>.2 by FINSEQ_1:44 .= <*b19,b29*>.2 by A6,A11,A13,A15,PRE_POLY:def 17 .= b29 by FINSEQ_1:44; per cases; suppose A17: b19 = term(m) & b29 = b2; (decomp(term(m)+b2)).k9 = (decomp(term(m)+b2))/.k9 by A6,A11, PARTFUN1:def 6 .= (decomp(term(m)+b2)).k by A4,A5,A13,A17,PARTFUN1:def 6; hence thesis by A6,A4,A11,A12,FUNCT_1:def 4; end; suppose b19 <> term(m); then m.b19 = 0.L by Lm8; hence thesis by A14; end; suppose b29 <> b2; then b19 <> term(m) by A16,PRE_POLY:48; then m.b19 = 0.L by Lm8; hence thesis by A14; end; end; term(m) = <*b19,b29*>.1 by A5,A7,FINSEQ_1:44 .= b19 by FINSEQ_1:44; hence thesis by A1,A6,A4,A8,A9,A10,POLYNOM2:3; end; theorem Th8: for X being set, L being right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p being Series of X,L holds 0.L * p = 0_(X,L) proof let n be set, L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of n,L; set op = 0.L * p; A1: now let u be object; assume u in dom op; then reconsider u9 = u as bag of n; op.u9 = 0.L * p.u9 by POLYNOM7:def 9 .= 0.L by BINOM:1; hence op.u = 0_(n,L).u by POLYNOM1:22; end; dom op = Bags n by FUNCT_2:def 1 .= dom 0_(n,L) by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th9: for X being set, L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p being Series of X,L, a being Element of L holds -(a * p) = (-a) * p & -(a * p) = a * (-p) proof let n be set, L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Series of n,L, a be Element of L; set ap = a * p; A1: now let u be object; assume u in dom -ap; then reconsider u9 = u as bag of n; (-ap).u9 = -(ap.u9) by POLYNOM1:17 .= -(a * p.u9) by POLYNOM7:def 9 .= (-a) * p.u9 by VECTSP_1:9 .= ((-a)*p).u9 by POLYNOM7:def 9; hence (-ap).u = ((-a)*p).u; end; dom -ap = Bags n by FUNCT_2:def 1 .= dom((-a) * p) by FUNCT_2:def 1; hence -(a * p) = (-a) * p by A1,FUNCT_1:2; A2: now let u be object; assume u in dom -ap; then reconsider u9 = u as bag of n; (-ap).u9 = -(ap.u9) by POLYNOM1:17 .= -(a * p.u9) by POLYNOM7:def 9 .= a * (-p.u9) by VECTSP_1:8 .= a * (-p).u9 by POLYNOM1:17 .= (a*(-p)).u9 by POLYNOM7:def 9; hence (-ap).u = (a*(-p)).u; end; dom -ap = Bags n by FUNCT_2:def 1 .= dom(a * (-p)) by FUNCT_2:def 1; hence thesis by A2,FUNCT_1:2; end; theorem Th10: for X being set, L being left-distributive non empty doubleLoopStr, p being Series of X,L, a,a9 being Element of L holds a * p + a9 * p = (a + a9) * p proof let n be set, L be left-distributive non empty doubleLoopStr, p be Series of n,L, a,a9 be Element of L; set p1 = a * p + a9 * p, p2 = (a + a9) * p; A1: now let u be object; assume u in dom p1; then reconsider u9 = u as bag of n; p1.u9 = (a*p).u9 + (a9*p).u9 by POLYNOM1:15 .= a * p.u9 + (a9*p).u9 by POLYNOM7:def 9 .= a * p.u9 + a9 * p.u9 by POLYNOM7:def 9 .= (a + a9) * p.u9 by VECTSP_1:def 3 .= p2.u9 by POLYNOM7:def 9; hence p1.u = p2.u; end; dom p1 = Bags n by FUNCT_2:def 1 .= dom p2 by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th11: for X being set, L being associative non empty multLoopStr_0, p being Series of X,L, a,a9 being Element of L holds (a * a9) * p = a * (a9 * p ) proof let n be set, L be associative non empty multLoopStr_0, p be Series of n,L , a,a9 be Element of L; set q = (a * a9) * p, r = a * (a9 * p); A1: now let u be object; assume u in dom q; then reconsider b = u as bag of n; q.b = (a * a9) * p.b by POLYNOM7:def 9 .= a * (a9 * p.b) by GROUP_1:def 3 .= a * (a9*p).b by POLYNOM7:def 9 .= r.b by POLYNOM7:def 9; hence q.u = r.u; end; dom q = Bags n by FUNCT_2:def 1 .= dom r by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th12: for n being Ordinal, L being add-associative right_zeroed right_complementable well-unital associative commutative distributive non empty doubleLoopStr, p,p9 being Series of n,L, a being Element of L holds a * (p *' p9) = p *' (a * p9) proof let n be Ordinal, L be add-associative right_zeroed right_complementable well-unital commutative associative distributive non empty doubleLoopStr, p, p9 be Series of n,L, a be Element of L; set app = a * (p *' p9), pap = p *' (a * p9), pp = p *' p9; A1: now let u be object; assume u in dom app; then reconsider b = u as bag of n; consider s being FinSequence of the carrier of L such that A2: pap.b = Sum s and A3: len s = len decomp b and A4: for k being Element of NAT st k in dom s ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*(a*p9).b2 by POLYNOM1:def 10; consider t being FinSequence of the carrier of L such that A5: pp.b = Sum t and A6: len t = len decomp b and A7: for k being Element of NAT st k in dom t ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*> & t/.k = p.b1*(p9).b2 by POLYNOM1:def 10; A8: dom t = Seg(len s) by A3,A6,FINSEQ_1:def 3 .= dom s by FINSEQ_1:def 3; now let i be object; assume A9: i in dom t; then reconsider k = i as Element of NAT; consider b1,b2 being bag of n such that A10: (decomp b)/.k = <*b1,b2*> and A11: t/.k = p.b1*(p9).b2 by A7,A9; consider a1,a2 being bag of n such that A12: (decomp b)/.k = <*a1,a2*> and A13: s/.k = p.a1*(a*p9).a2 by A4,A8,A9; A14: b2 = <*a1,a2*>.2 by A10,A12,FINSEQ_1:44 .= a2 by FINSEQ_1:44; b1 = <*a1,a2*>.1 by A10,A12,FINSEQ_1:44 .= a1 by FINSEQ_1:44; hence s/.i = p.b1 * (a*(p9).b2) by A13,A14,POLYNOM7:def 9 .= a*(t/.i) by A11,GROUP_1:def 3; end; then s = a * t by A8,POLYNOM1:def 1; then pap.b = a * Sum t by A2,POLYNOM1:12 .= app.b by A5,POLYNOM7:def 9; hence app.u = pap.u; end; dom app = Bags n by FUNCT_2:def 1 .= dom pap by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; begin :: Multiplication of polynomials with bags definition let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L; func b *' p -> Series of n,L means :Def1: for b9 being bag of n st b divides b9 holds it.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds it.b9 = 0.L; existence proof set M1 = {[b9,p.(b9-'b)] where b9 is Element of Bags n : b divides b9}, M2 = {[b9,0.L] where b9 is Element of Bags n : not(b divides b9)}; set M = M1 \/ M2; now let u be object; assume A1: u in M; now per cases by A1,XBOOLE_0:def 3; case u in M1; then ex b9 being Element of Bags n st u = [b9,p.(b9-'b)] & b divides b9; hence u in [:Bags n,the carrier of L:] by ZFMISC_1:def 2; end; case u in M2; then ex b9 being Element of Bags n st u = [b9,0.L] & not b divides b9; hence u in [:Bags n,the carrier of L:] by ZFMISC_1:def 2; end; end; hence u in [:Bags n,the carrier of L:]; end; then reconsider M as Relation of Bags n,the carrier of L by TARSKI:def 3; A2: now let u be object; assume u in Bags n; then reconsider u9 = u as bag of n; A3: u9 is Element of Bags n by PRE_POLY:def 12; now per cases; case not b divides u9; then [u9,0.L] in {[b9,0.L] where b9 is Element of Bags n : not(b divides b9)} by A3; then [u9,0.L] in M by XBOOLE_0:def 3; hence u in dom M by XTUPLE_0:def 12; end; case b divides u9; then [u9,p.(u9-'b)] in {[b9,p.(b9-'b)] where b9 is Element of Bags n : b divides b9} by A3; then [u9,p.(u9-'b)] in M by XBOOLE_0:def 3; hence u in dom M by XTUPLE_0:def 12; end; end; hence u in dom M; end; for u being object holds u in dom M implies u in Bags n; then A4: dom M = Bags n by A2,TARSKI:2; A5: now let x,y1,y2 be object; assume A6: [x,y1] in M & [x,y2] in M; A7: now assume that A8: [x,y1] in M2 and A9: [x,y2] in M1; consider v being Element of Bags n such that A10: [v,0.L] = [x,y1] and A11: not b divides v by A8; consider u being Element of Bags n such that A12: [u,p.(u-'b)] = [x,y2] and A13: b divides u by A9; u = x by A12,XTUPLE_0:1 .= v by A10,XTUPLE_0:1; hence contradiction by A13,A11; end; A14: now assume that A15: [x,y1] in M1 and A16: [x,y2] in M2; consider v being Element of Bags n such that A17: [v,0.L] = [x,y2] and A18: not b divides v by A16; consider u being Element of Bags n such that A19: [u,p.(u-'b)] = [x,y1] and A20: b divides u by A15; u = x by A19,XTUPLE_0:1 .= v by A17,XTUPLE_0:1; hence contradiction by A20,A18; end; thus [x,y1] in M1 & [x,y2] in M1 or [x,y1] in M2 & [x,y2] in M2 proof assume A21: not([x,y1] in M1 & [x,y2] in M1); now per cases by A21; case not [x,y1] in M1; hence thesis by A6,A7,XBOOLE_0:def 3; end; case not [x,y2] in M1; hence thesis by A6,A14,XBOOLE_0:def 3; end; end; hence thesis; end; end; now let x,y1,y2 be object; assume A22: [x,y1] in M & [x,y2] in M; now per cases by A5,A22; case A23: [x,y1] in M1 & [x,y2] in M1; then consider v being Element of Bags n such that A24: [v,p.(v-'b)] = [x,y2] and b divides v; consider u being Element of Bags n such that A25: [u,p.(u-'b)] = [x,y1] and b divides u by A23; u = x by A25,XTUPLE_0:1 .= v by A24,XTUPLE_0:1; hence y1 = p.(v-'b) by A25,XTUPLE_0:1 .= y2 by A24,XTUPLE_0:1; end; case A26: [x,y1] in M2 & [x,y2] in M2; then A27: ex v being Element of Bags n st [v,0.L] = [x,y2] & not b divides v; A28: ex u being Element of Bags n st [u,0.L] = [x,y1] & not b divides u by A26; thus y1 = 0.L by A28,XTUPLE_0:1 .= y2 by A27,XTUPLE_0:1; end; end; hence y1 = y2; end; then reconsider M as Function of Bags n,the carrier of L by A4, FUNCT_1:def 1,FUNCT_2:def 1; reconsider M as Function of Bags n,L; take M; A29: now let b9 be bag of n; A30: b9 is Element of Bags n by PRE_POLY:def 12; assume not b divides b9; then [b9,0.L] in {[u,0.L] where u is Element of Bags n : not(b divides u )} by A30; then [b9,0.L] in M by XBOOLE_0:def 3; hence M.b9 = 0.L by FUNCT_1:1; end; now let b9 be bag of n; A31: b9 is Element of Bags n by PRE_POLY:def 12; assume b divides b9; then [b9,p.(b9-'b)] in {[u,p.(u-'b)] where u is Element of Bags n : b divides u} by A31; then [b9,p.(b9-'b)] in M by XBOOLE_0:def 3; hence M.b9 = p.(b9-'b) by FUNCT_1:1; end; hence thesis by A29; end; uniqueness proof let p1,p2 be Series of n,L such that A32: for b9 being bag of n st b divides b9 holds p1.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds p1.b9 = 0.L and A33: for b9 being bag of n st b divides b9 holds p2.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds p2.b9 = 0.L; now let x be Element of Bags n; now per cases; case A34: b divides x; hence p1.x = p.(x -' b) by A32 .= p2.x by A33,A34; end; case A35: not b divides x; hence p1.x = 0.L by A32 .= p2.x by A33,A35; end; end; hence p1.x = p2.x; end; hence p1 = p2 by FUNCT_2:63; end; end; Lm9: for n being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p being Series of n,L holds (b*'p).(b9+b) = p.b9 proof let n be Ordinal, b,b9 be bag of n, L be non empty ZeroStr, p be Series of n ,L; b divides b9 + b by PRE_POLY:50; hence (b*'p).(b9+b) = p.(b9 + b -' b) by Def1 .= p.b9 by PRE_POLY:48; end; Lm10: for n being Ordinal, L being non empty ZeroStr, p being Polynomial of n, L, b being bag of n holds Support(b*'p) c= {b + b9 where b9 is Element of Bags n: b9 in Support p} proof let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n,L, b be bag of n; now let u be object; assume A1: u in Support(b*'p); then reconsider u9 = u as Element of Bags n; A2: (b*'p).u9 <> 0.L by A1,POLYNOM1:def 4; then b divides u9 by Def1; then consider s being bag of n such that A3: u9 = b + s by TERMORD:1; s is Element of Bags n & p.s <> 0.L by A2,A3,Lm9,PRE_POLY:def 12; then s in Support p by POLYNOM1:def 4; hence u in {b + b9 where b9 is Element of Bags n : b9 in Support p} by A3; end; hence thesis by TARSKI:def 3; end; registration let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be finite-Support Series of n,L; cluster b *' p -> finite-Support; coherence proof set f = {[b9,b + b9] where b9 is Element of Bags n : b9 in Support p}; A1: now let u be object; assume u in f; then ex b9 being Element of Bags n st u = [b9,b+b9] & b9 in Support p; hence ex y,z being object st u = [y,z]; end; now let x,y1,y2 be object; assume that A2: [x,y1] in f and A3: [x,y2] in f; consider b2 being Element of Bags n such that A4: [x,y2] = [b2,b+b2] and b2 in Support p by A3; consider b1 being Element of Bags n such that A5: [x,y1] = [b1,b+b1] and b1 in Support p by A2; b1 = x by A5,XTUPLE_0:1 .= b2 by A4,XTUPLE_0:1; hence y1 = y2 by A5,A4,XTUPLE_0:1; end; then reconsider f as Function by A1,FUNCT_1:def 1,RELAT_1:def 1; A6: now let u be object; assume u in dom f; then consider v being object such that A7: [u,v] in f by XTUPLE_0:def 12; consider b9 being Element of Bags n such that A8: [u,v] = [b9,b+b9] and A9: b9 in Support p by A7; u = b9 by A8,XTUPLE_0:1; hence u in Support p by A9; end; A10: Support(b*'p) c= {b + b9 where b9 is Element of Bags n : b9 in Support p} by Lm10; now let u be object; assume u in Support(b*'p); then u in {b + b9 where b9 is Element of Bags n : b9 in Support p} by A10; then consider b9 being Element of Bags n such that A11: u = b + b9 & b9 in Support p; [b9,u] in f by A11; hence u in rng f by XTUPLE_0:def 13; end; then A12: Support(b*'p) c= rng f by TARSKI:def 3; now let u be object; assume A13: u in Support p; then reconsider u9 = u as Element of Bags n; [u9,b+u9] in {[b9,b + b9] where b9 is Element of Bags n : b9 in Support p } by A13; hence u in dom f by XTUPLE_0:def 12; end; then dom f = Support p by A6,TARSKI:2; then dom f is finite by POLYNOM1:def 5; then rng f is finite by FINSET_1:8; hence thesis by A12,POLYNOM1:def 5; end; end; theorem for n being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p being Series of n,L holds (b*'p).(b9+b) = p.b9 by Lm9; theorem for n being Ordinal, L being non empty ZeroStr, p being Polynomial of n,L, b being bag of n holds Support(b*'p) c= {b + b9 where b9 is Element of Bags n : b9 in Support p} by Lm10; theorem Th15: for n being Ordinal, T being connected admissible TermOrder of n , L being non trivial ZeroStr, p being non-zero Polynomial of n,L, b being bag of n holds HT(b*'p,T) = b + HT(p,T) proof let n be Ordinal, T be connected admissible TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n,L, b be bag of n; set htp = HT(p,T); per cases; suppose A1: Support(b*'p) = {}; now assume Support p <> {}; then reconsider sp = Support p as non empty set; set u = the Element of sp; u in Support p; then reconsider u9 = u as Element of Bags n; b divides b+u9 by PRE_POLY:50; then (b*'p).(b+u9) = p.(b+u9-'b) by Def1 .= p.u9 by PRE_POLY:48; then A2: (b*'p).(b+u9) <> 0.L by POLYNOM1:def 4; b+u9 is Element of Bags n by PRE_POLY:def 12; hence contradiction by A1,A2,POLYNOM1:def 4; end; then p = 0_(n,L) by POLYNOM7:1; hence thesis by POLYNOM7:def 1; end; suppose A3: Support(b*'p) <> {}; now reconsider sp = Support(b*'p) as non empty set by A3; set u = the Element of sp; u in Support(b*'p); then reconsider u9 = u as Element of Bags n; A4: u9-'b is Element of Bags n by PRE_POLY:def 12; A5: (b*'p).u9 <> 0.L by POLYNOM1:def 4; then b divides u9 by Def1; then A6: p.(u9-'b) <> 0.L by A5,Def1; assume Support p = {}; hence contradiction by A6,A4,POLYNOM1:def 4; end; then htp in Support p by TERMORD:def 6; then A7: p.htp <> 0.L by POLYNOM1:def 4; A8: now let b9 be bag of n; assume b9 in Support(b*'p); then A9: (b*'p).b9 <> 0.L by POLYNOM1:def 4; then b divides b9 by Def1; then consider b3 being bag of n such that A10: b + b3 = b9 by TERMORD:1; A11: b3 is Element of Bags n by PRE_POLY:def 12; (b*'p).b9 = p.b3 by A10,Lm9; then b3 in Support p by A9,A11,POLYNOM1:def 4; then b3 <= htp,T by TERMORD:def 6; then [b3,htp] in T by TERMORD:def 2; then [b9,b+htp] in T by A10,BAGORDER:def 5; hence b9 <= b+htp,T by TERMORD:def 2; end; (b*'p).(b+htp) = p.htp & b+htp is Element of Bags n by Lm9,PRE_POLY:def 12; then b + htp in Support(b*'p) by A7,POLYNOM1:def 4; hence thesis by A8,TERMORD:def 6; end; end; theorem Th16: for n being Ordinal, T being connected admissible TermOrder of n , L being non empty ZeroStr, p being Polynomial of n,L, b,b9 being bag of n holds b9 in Support(b*'p) implies b9 <= b+HT(p,T),T proof let n be Ordinal, T be connected admissible TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L, b,b9 be bag of n; assume A1: b9 in Support(b*'p); Support(b*'p) c= {b + b2 where b2 is Element of Bags n : b2 in Support p } by Lm10; then b9 in {b + b2 where b2 is Element of Bags n : b2 in Support p} by A1; then consider s being Element of Bags n such that A2: b9 = b + s and A3: s in Support p; s <= HT(p,T),T by A3,TERMORD:def 6; then [s,HT(p,T)] in T by TERMORD:def 2; then [b+s,b+HT(p,T)] in T by BAGORDER:def 5; hence thesis by A2,TERMORD:def 2; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L holds (EmptyBag n) *' p = p proof let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n,L; set e = EmptyBag n; A1: now let u be object; assume u in dom p; then reconsider u9 = u as Element of Bags n; EmptyBag n divides u9 by PRE_POLY:59; then (e*'p).u9 = p.(u9-'e) by Def1 .= p.u9 by PRE_POLY:54; hence (e*'p).u = p.u; end; dom(e*'p) = Bags n by FUNCT_2:def 1 .= dom p by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th18: for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L, b1,b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p) proof let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n,L, b1,b2 be bag of n; set q = (b1 + b2) *' p, r = b1 *' (b2 *' p); A1: now let u be object; assume u in dom q; then reconsider b = u as bag of n; now per cases; case A2: b1+b2 divides b; then consider b3 being bag of n such that A3: (b1+b2) + b3 = b by TERMORD:1; A4: b1 + (b2+b3) = b by A3,PRE_POLY:35; then b2 + b3 = b -' b1 by PRE_POLY:48; then A5: b2 divides b -' b1 by TERMORD:1; b1 divides b by A4,TERMORD:1; then r.b = (b2 *' p).(b-'b1) by Def1; hence r.b = p.((b-'b1) -' b2) by A5,Def1 .= p.(b-'(b1+b2)) by PRE_POLY:36 .= q.b by A2,Def1; end; case A6: not b1+b2 divides b; then A7: q.b = 0.L by Def1; now per cases; case A8: b1 divides b; A9: now assume b2 divides b-'b1; then ((b -' b1) -' b2) + b2 = b-'b1 by PRE_POLY:47; then ((b -' b1) -' b2) + b2 + b1 = b by A8,PRE_POLY:47; then ((b -' b1) -' b2) + (b2 + b1) = b by PRE_POLY:35; hence contradiction by A6,TERMORD:1; end; r.b = (b2 *' p).(b-'b1) by A8,Def1; hence q.b = r.b by A7,A9,Def1; end; case not b1 divides b; hence q.b = r.b by A7,Def1; end; end; hence q.b = r.b; end; end; hence q.u = r.u; end; dom q = Bags n by FUNCT_2:def 1 .= dom r by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th19: for n being Ordinal, L being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L holds Support(a*p) c= Support(p) proof let n be Ordinal, L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p be Polynomial of n,L, a9 be Element of L; A1: dom(0_(n,L)) = Bags n by FUNCT_2:def 1 .= dom(a9*p) by FUNCT_2:def 1; per cases; suppose A2: a9 = 0.L; now let u be object; assume u in dom(a9*p); then reconsider u9 = u as Element of Bags n; (a9*p).u9 = a9 * p.u9 by POLYNOM7:def 9 .= 0.L by A2 .= (0_(n,L)).u9 by POLYNOM1:22; hence (a9*p).u = (0_(n,L)).u; end; then a9*p = 0_(n,L) by A1,FUNCT_1:2; then for u being object holds u in Support(a9*p) implies u in Support(p) by POLYNOM7:1; hence thesis by TARSKI:def 3; end; suppose a9 <> 0.L; then reconsider a = a9 as non zero Element of L by STRUCT_0:def 12; now let u be object; assume A3: u in Support(a*p); then reconsider u9 = u as Element of Bags n; A4: (a*p).u9 = a * p.u9 by POLYNOM7:def 9; (a*p).u9 <> 0.L by A3,POLYNOM1:def 4; then p.u9 <> 0.L by A4; hence u in Support(p) by POLYNOM1:def 4; end; hence thesis by TARSKI:def 3; end; end; theorem for n being Ordinal, L being domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, a being non zero Element of L holds Support(p) c= Support(a*p) proof let n be Ordinal, L be domRing-like non trivial doubleLoopStr, p be Polynomial of n,L, a be non zero Element of L; now let u be object; assume A1: u in Support p; then reconsider u9 = u as Element of Bags n; A2: (a*p).u9 = a * p.u9 & a <> 0.L by POLYNOM7:def 9; p.u9 <> 0.L by A1,POLYNOM1:def 4; then (a*p).u9 <> 0.L by A2,VECTSP_2:def 1; hence u in Support(a*p) by POLYNOM1:def 4; end; hence thesis by TARSKI:def 3; end; theorem Th21: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, a being non zero Element of L holds HT(a*p,T) = HT(p,T) proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n,L, a be non zero Element of L; set ht = HT(a*p,T), htp = HT(p,T); per cases; suppose A1: Support(a*p) = {}; now assume Support p <> {}; then reconsider sp = Support p as non empty set; set u = the Element of sp; u in Support p; then reconsider u9 = u as Element of Bags n; A2: (a*p).u9 = a * p.u9 by POLYNOM7:def 9; p.u9 <> 0.L & a <> 0.L by POLYNOM1:def 4; then (a*p).u9 <> 0.L by A2,VECTSP_2:def 1; hence contradiction by A1,POLYNOM1:def 4; end; hence htp = EmptyBag n by TERMORD:def 6 .= ht by A1,TERMORD:def 6; end; suppose A3: Support(a*p) <> {}; now reconsider sp = Support(a*p) as non empty set by A3; set u = the Element of sp; u in Support(a*p); then reconsider u9 = u as Element of Bags n; (a*p).u9 <> 0.L & (a*p).u9 = a * p.u9 by POLYNOM1:def 4,POLYNOM7:def 9; then A4: p.u9 <> 0.L; assume Support p = {}; hence contradiction by A4,POLYNOM1:def 4; end; then htp in Support p by TERMORD:def 6; then A5: p.htp <> 0.L by POLYNOM1:def 4; A6: now let b be bag of n; assume A7: b in Support(a*p); Support(a*p) c= Support(p) by Th19; hence b <= htp,T by A7,TERMORD:def 6; end; (a*p).htp = a * p.htp by POLYNOM7:def 9; then (a*p).htp <> 0.L by A5,VECTSP_2:def 1; then htp in Support(a*p) by POLYNOM1:def 4; hence thesis by A6,TERMORD:def 6; end; end; theorem Th22: for n being Ordinal, L being add-associative right_complementable right_zeroed distributive non trivial doubleLoopStr, p being Series of n,L, b being bag of n, a being Element of L holds a * (b *' p) = Monom(a,b) *' p proof let n be Ordinal, L be add-associative right_complementable right_zeroed distributive non trivial doubleLoopStr, p be Series of n,L, b be bag of n, a be Element of L; set q = a * (b *' p), q9 = Monom(a,b) *' p, m = Monom(a,b); per cases; suppose a <> 0.L; then reconsider a as non zero Element of L by STRUCT_0:def 12; A1: now let u be object; assume u in dom q; then reconsider s = u as bag of n; consider t being FinSequence of the carrier of L such that A2: q9.s = Sum t and A3: len t = len decomp s and A4: for k being Element of NAT st k in dom t ex b1, b2 being bag of n st (decomp s)/.k = <*b1, b2*> & t/.k = m.b1*p.b2 by POLYNOM1:def 10; A5: dom t = Seg(len(decomp s)) by A3,FINSEQ_1:def 3 .= dom(decomp s) by FINSEQ_1:def 3; A6: term(Monom(a,b)) = b by POLYNOM7:10; now per cases; case A7: b divides s; A8: q.s = a * (b*'p).s by POLYNOM7:def 9 .= a * p.(s-'b) by A7,Def1; consider s9 being bag of n such that A9: b + s9 = s by A7,TERMORD:1; consider i being Element of NAT such that A10: i in dom decomp s and A11: (decomp s)/.i = <*b,s9*> by A9,PRE_POLY:69; consider b1,b2 being bag of n such that A12: (decomp s)/.i = <*b1, b2*> and A13: t/.i = m.b1*p.b2 by A4,A5,A10; A14: b2 = <*b,s9*>.2 by A11,A12,FINSEQ_1:44 .= s9 by FINSEQ_1:44; A15: s -' b = s9 by A9,PRE_POLY:48; A16: now let i9 be Element of NAT; assume that A17: i9 in dom t and A18: i9 <> i; consider b19,b29 being bag of n such that A19: (decomp s)/.i9 = <*b19,b29*> and A20: t/.i9 = m.b19*p.b29 by A4,A17; consider h1, h2 being bag of n such that A21: (decomp s)/.i9 = <*h1, h2*> and A22: s = h1 + h2 by A5,A17,PRE_POLY:68; A23: s -' h1 = h2 by A22,PRE_POLY:48; A24: h1 = <*b19,b29*>.1 by A19,A21,FINSEQ_1:44 .= b19 by FINSEQ_1:44; now assume m.b19 <> 0.L; then b19 = b by A6,POLYNOM7:def 5; then (decomp s).i9 = (decomp s)/.i by A5,A11,A15,A17,A21,A24,A23, PARTFUN1:def 6 .= (decomp s).i by A10,PARTFUN1:def 6; hence contradiction by A5,A10,A17,A18,FUNCT_1:def 4; end; hence t/.i9 = 0.L by A20; end; b1 = <*b,s9*>.1 by A11,A12,FINSEQ_1:44 .= b by FINSEQ_1:44; then Sum t = coefficient(m) * p.(s-'b) by A6,A5,A10,A15,A13,A14,A16,POLYNOM2:3 .= a * p.(s-'b) by POLYNOM7:9; hence q.s = q9.s by A2,A8; end; case A25: not b divides s; consider t being FinSequence of the carrier of L such that A26: q9.s = Sum t and A27: len t = len decomp s and A28: for k being Element of NAT st k in dom t ex b1, b2 being bag of n st (decomp s)/.k = <*b1, b2*> & t/.k = m.b1*p.b2 by POLYNOM1:def 10; A29: now let k be Nat; assume A30: k in dom t; then consider b19,b29 being bag of n such that A31: (decomp s)/.k = <*b19,b29*> and A32: t/.k = m.b19*p.b29 by A28; A33: dom t = Seg(len(decomp s)) by A27,FINSEQ_1:def 3 .= dom(decomp s) by FINSEQ_1:def 3; now per cases; case A34: b19 = term(m); consider h1,h2 being bag of n such that A35: (decomp s)/.k = <*h1,h2*> and A36: s = h1 + h2 by A30,A33,PRE_POLY:68; h1 = <*b19,b29*>.1 by A31,A35,FINSEQ_1:44 .= b19 by FINSEQ_1:44; hence contradiction by A6,A25,A34,A36,TERMORD:1; end; case b19 <> term(m); hence m.b19 = 0.L by Lm8; end; end; hence t/.k = 0.L by A32; end; q.s = a * (b*'p).s by POLYNOM7:def 9 .= a * 0.L by A25,Def1 .= 0.L; hence q.u = q9.u by A26,A29,MATRLIN:11; end; end; hence q.u = q9.u; end; dom q = Bags n by FUNCT_2:def 1 .= dom q9 by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; suppose A37: a = 0.L; A38: now let u be object; assume u in dom m; then reconsider u9 = u as Element of Bags n; now per cases; case A39: u9 = term(m); coefficient(m) = 0.L by A37,POLYNOM7:8; hence m.u = (0_(n,L)).u by A39,POLYNOM1:22; end; case u9 <> term(m); then m.u9 = 0.L by Lm8 .= (0_(n,L)).u9 by POLYNOM1:22; hence m.u = (0_(n,L)).u; end; end; hence m.u = (0_(n,L)).u; end; dom m = Bags n by FUNCT_2:def 1 .= dom 0_(n,L) by FUNCT_2:def 1; then A40: m = 0_(n,L) by A38,FUNCT_1:2; A41: now let u be object; assume u in dom q; then reconsider u9 = u as bag of n; q.u9 = 0.L * (b*'p).u9 by A37,POLYNOM7:def 9 .= 0.L .= (0_(n,L)).u9 by POLYNOM1:22; hence q.u = (0_(n,L)).u; end; dom q = Bags n by FUNCT_2:def 1 .= dom 0_(n,L) by FUNCT_2:def 1; then q = 0_(n,L) by A41,FUNCT_1:2; hence thesis by A40,Th5; end; end; theorem for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p being non-zero Polynomial of n,L, q being Polynomial of n,L, m being non-zero Monomial of n,L holds HT(p,T) in Support q implies HT(m*'p,T) in Support(m*'q) proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n,L, q be Polynomial of n,L, m be non-zero Monomial of n,L; set a = coefficient(m), b = term(m); assume HT(p,T) in Support q; then A1: q.(HT(p,T)) <> 0.L by POLYNOM1:def 4; A2: HC(m,T) <> 0.L; then reconsider a as non zero Element of L by TERMORD:23; m = Monom(a,b) by POLYNOM7:11; then m *' p = a * (b *' p) by Th22; then HT(m*'p,T) = HT(b*'p,T) by Th21 .= b + HT(p,T) by Th15; then A3: (m*'q).(HT(m*'p,T)) = m.term(m) * q.(HT(p,T)) by Th7; m.(HT(m,T)) <> 0.L by A2,TERMORD:def 7; then m.term(m) <> 0.L by POLYNOM7:def 5; then (m*'q).(HT(m*'p,T)) <> 0.L by A1,A3,VECTSP_2:def 1; hence thesis by POLYNOM1:def 4; end; begin :: Orders on Polynomials registration let n be Ordinal, T be connected TermOrder of n; cluster RelStr(#Bags n, T#) -> connected; coherence proof set L = RelStr(# Bags n, T #); now let x,y be Element of L; reconsider x9 = x as bag of n; reconsider y9 = y as bag of n; y9 <= y9,T by TERMORD:6; then [y9,y9] in T by TERMORD:def 2; then A1: y in field T by RELAT_1:15; x9 <= x9,T by TERMORD:6; then [x9,x9] in T by TERMORD:def 2; then A2: T is_connected_in field T & x in field T by RELAT_1:15,RELAT_2:def 14; now per cases; case x <> y; then [x,y] in the InternalRel of L or [y,x] in the InternalRel of L by A2,A1,RELAT_2:def 6; hence x <= y or y <= x by ORDERS_2:def 5; end; case x = y; then x9 <= y9,T by TERMORD:6; then [x9,y9] in the InternalRel of L by TERMORD:def 2; hence x <= y or y <= x by ORDERS_2:def 5; end; end; hence x <= y or y <= x; end; hence thesis by WAYBEL_0:def 29; end; end; registration let n be Nat, T be admissible TermOrder of n; cluster RelStr (#Bags n, T#) -> well_founded; coherence proof set R = RelStr(# Bags n, T #), X = the carrier of R; now let Y be set; assume that A1: Y c= X and A2: Y <> {}; now let u be object; assume u in Y; then reconsider u9 = u as bag of n by A1; u9 <= u9,T by TERMORD:6; then [u9,u9] in T by TERMORD:def 2; hence u in field T by RELAT_1:15; end; then Y c= field T by TARSKI:def 3; hence ex a being object st a in Y & T-Seg a misses Y by A2,WELLORD1:def 2; end; then T is_well_founded_in the carrier of R by WELLORD1:def 3; hence thesis by WELLFND1:def 2; end; end; Lm11: for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds Support p in Fin the carrier of RelStr (# Bags n, T#) proof let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; set sp = Support p; sp is finite by POLYNOM1:def 5; hence thesis by FINSUB_1:def 5; end; definition :: according to p. 193 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p <= q,T means [Support p, Support q] in FinOrd RelStr(# Bags n, T#); end; definition let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p < q,T means p <= q,T & Support p <> Support q; end; definition let n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L; func Support(p,T) -> Element of Fin the carrier of RelStr(#Bags n,T#) equals Support(p); coherence by Lm11; end; theorem Th24: :: according to definition 5.15, p. 194 for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being non-zero Polynomial of n,L holds PosetMax(Support( p,T)) = HT(p,T) proof let n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n,L; set htp = HT(p,T), R = RelStr(#Bags n,T#), sp = Support(p,T); p <> 0_(n,L) by POLYNOM7:def 1; then Support(p) <> {} by POLYNOM7:1; then A1: htp in Support(p) by TERMORD:def 6; now assume ex y being set st y in sp & y <> htp & [htp,y] in the InternalRel of R; then consider y being set such that A2: y in sp and A3: y <> htp and A4: [htp,y] in the InternalRel of R; y is Element of Bags n by A2; then reconsider y9 = y as bag of n; y9 <= htp,T & htp <= y9,T by A2,A4,TERMORD:def 2,def 6; hence contradiction by A3,TERMORD:7; end; then htp is_maximal_wrt Support(p,T),the InternalRel of R by A1, WAYBEL_4:def 23; hence thesis by A1,BAGORDER:def 13; end; theorem Th25: :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p being Polynomial of n,L holds p <= p,T by Lm11,ORDERS_1:3; Lm12: for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T proof let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; set sp0 = Support 0_(n,L), sp = Support p, R = RelStr(#Bags n,T#); A1: sp is Element of Fin the carrier of R by Lm11; sp0 = {} & sp0 is Element of Fin the carrier of R by Lm11,POLYNOM7:1; then [sp0,sp] in {[x,y] where x, y is Element of Fin the carrier of R : x = {} or (x<>{} & y <> {} & PosetMax x <> PosetMax y & [PosetMax x,PosetMax y] in the InternalRel of R)} by A1; then A2: [sp0,sp] in (FinOrd-Approx R).0 by BAGORDER:def 14; dom (FinOrd-Approx R) = NAT by BAGORDER:def 14; then (FinOrd-Approx R).0 in rng FinOrd-Approx R by FUNCT_1:3; then [sp0,sp] in union rng FinOrd-Approx R by A2,TARSKI:def 4; then [sp0,sp] in FinOrd R by BAGORDER:def 15; hence thesis; end; theorem Th26: :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T & q <= p,T iff Support p = Support q proof let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q being Polynomial of n,L; set O = FinOrd RelStr(# Bags n, T#); A1: now assume p <= q,T & q <= p,T; then A2: [Support p, Support q] in O & [Support q, Support p] in O; Support p in Fin the carrier of RelStr(# Bags n, T#) & Support q in Fin the carrier of RelStr(# Bags n, T#) by Lm11; hence Support p = Support q by A2,ORDERS_1:4; end; Support p = Support q implies p <= q,T & q <= p,T by Lm11,ORDERS_1:3; hence thesis by A1; end; theorem Th27: :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q,r being Polynomial of n,L holds p <= q,T & q <= r,T implies p <= r,T proof let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q,r be Polynomial of n,L; set O = FinOrd RelStr(# Bags n, T#); A1: Support r in Fin the carrier of RelStr(# Bags n, T#) by Lm11; assume p <= q,T & q <= r,T; then A2: [Support p, Support q] in O & [Support q, Support r] in O; Support p in Fin the carrier of RelStr(# Bags n, T#) & Support q in Fin the carrier of RelStr(# Bags n, T#) by Lm11; then [Support p, Support r] in O by A2,A1,ORDERS_1:5; hence thesis; end; theorem Th28: for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T or q <= p,T proof let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n,L; set R = RelStr(# Bags n, T#), O = RelStr (# Fin the carrier of R, FinOrd R #); reconsider sp = Support p, sq = Support q as Element of O by Lm11; FinPoset R is connected; then O is connected by BAGORDER:def 16; then sp <= sq or sq <= sp by WAYBEL_0:def 29; then [Support p, Support q] in FinOrd R or [Support q, Support p] in FinOrd R by ORDERS_2:def 5; hence thesis; end; theorem Th29: for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T iff not q < p, T proof let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q being Polynomial of n,L; A1: not q < p,T implies p <= q,T proof assume A2: not q < p,T; now per cases by A2; case not Support q <> Support p; hence thesis by Th26; end; case not q <= p,T; hence thesis by Th28; end; end; hence thesis; end; p <= q,T implies not q < p,T by Th26; hence thesis by A1; end; Lm13: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being Polynomial of n,L, b being bag of n holds [HT(p,T),b] in T & b <> HT(p,T) implies p.b = 0.L proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n,L, b be bag of n; A1: b is Element of Bags n by PRE_POLY:def 12; assume A2: [HT(p,T),b] in T & b <> HT(p,T); now assume b in Support p; then b <= HT(p,T),T by TERMORD:def 6; then [b,HT(p,T)] in T by TERMORD:def 2; hence contradiction by A2,A1,ORDERS_1:4; end; hence thesis by A1,POLYNOM1:def 4; end; Lm14: for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr , p being Polynomial of n,L st HT(p,T) = EmptyBag n holds Red(p,T) = 0_(n,L) proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n,L; set red = Red(p,T), e = 0_(n,L); assume A1: HT(p,T) = EmptyBag n; A2: now let b be bag of n; A3: [EmptyBag n,b] in T by BAGORDER:def 5; assume b <> EmptyBag n; hence p.b = 0.L by A1,A3,Lm13; end; A4: now let b be object; assume b in dom red; then reconsider b9 = b as Element of Bags n; A5: red.b9 = (p-HM(p,T)).b9 by TERMORD:def 9 .= (p+(-(HM(p,T)))).b9 by POLYNOM1:def 7 .= p.b9 + (-HM(p,T)).b9 by POLYNOM1:15 .= p.b9 + -(HM(p,T).b9) by POLYNOM1:17; now per cases; case b9 = EmptyBag n; hence red.b9 = p.(HT(p,T)) + -(p.(HT(p,T))) by A1,A5,TERMORD:18 .= 0.L by RLVECT_1:5 .= e.b9 by POLYNOM1:22; end; case A6: b9 <> EmptyBag n; hence red.b9 = 0.L + -(HM(p,T).b9) by A2,A5 .= 0.L + -(0.L) by A1,A6,TERMORD:19 .= 0.L by RLVECT_1:5 .= e.b9 by POLYNOM1:22; end; end; hence red.b = e.b; end; dom red = Bags n by FUNCT_2:def 1 .= dom e by FUNCT_2:def 1; hence thesis by A4,FUNCT_1:2; end; Lm15: for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr , p,q being Polynomial of n,L holds p < q,T iff (p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T) proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n,L; set R = RelStr(#Bags n,T#), sp = Support p, sq = Support q, x = Support(p,T) , y = Support(q,T); A1: now assume A2: p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT (q,T) & Red(p,T) < Red(q,T),T; now per cases by A2; case A3: p = 0_(n,L) & q <> 0_(n,L); then Support p = {} by POLYNOM7:1; then A4: Support p <> Support q by A3,POLYNOM7:1; p <= q,T by A3,Lm12; hence p < q,T by A4; end; case A5: HT(p,T) < HT(q,T),T; then A6: HT(p,T) <> HT(q,T) by TERMORD:def 3; A7: HT(p,T) <= HT(q,T),T by A5,TERMORD:def 3; then A8: [HT(p,T),HT(q,T)] in T by TERMORD:def 2; now per cases; case A9: sp = {}; then A10: p = 0_(n,L) by POLYNOM7:1; A11: now assume sp = sq; then HT(p,T) = HT(q,T) by A9,A10,POLYNOM7:1; hence contradiction by A5,TERMORD:def 3; end; p <= q,T by A10,Lm12; hence p < q,T by A11; end; case A12: sp <> {}; A13: now assume sq = {}; then HT(q,T) = EmptyBag n by TERMORD:def 6; then [HT(q,T),HT(p,T)] in T by BAGORDER:def 5; then HT(q,T) <= HT(p,T),T by TERMORD:def 2; hence contradiction by A7,A6,TERMORD:7; end; A14: now assume A15: sp = sq; HT(q,T) in sq by A13,TERMORD:def 6; then A16: HT(q,T) <= HT(p,T),T by A15,TERMORD:def 6; HT(p,T) in sp by A12,TERMORD:def 6; then HT(p,T) <= HT(q,T),T by A15,TERMORD:def 6; hence contradiction by A6,A16,TERMORD:7; end; p <> 0_(n,L) by A12,POLYNOM7:1; then p is non-zero; then A17: PosetMax(Support(p,T)) = HT(p,T) by Th24; q <> 0_(n,L) by A13,POLYNOM7:1; then q is non-zero; then PosetMax(Support(q,T)) = HT(q,T) by Th24; then [x,y] in union rng FinOrd-Approx R by A6,A8,A12,A13,A17,BAGORDER:35; then [sp,sq] in FinOrd R by BAGORDER:def 15; then p <= q,T; hence p < q,T by A14; end; end; hence p < q,T; end; case A18: HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T; then Red(p,T) <= Red(q,T),T; then A19: [Support(Red(p,T)),Support(Red(q,T))] in FinOrd R; now per cases; case sp = {}; then A20: HT(p,T) = EmptyBag n by TERMORD:def 6; then Red(p,T) = 0_(n,L) by Lm14; then Support(Red(q,T)) = Support(Red(p,T)) by A18,A20,Lm14; hence contradiction by A18; end; case A21: sp <> {}; now per cases; case sq = {}; then A22: HT(q,T) = EmptyBag n by TERMORD:def 6; then Red(q,T) = 0_(n,L) by Lm14; then Support(Red(p,T)) = Support(Red(q,T)) by A18,A22,Lm14; hence contradiction by A18; end; case A23: sq <> {}; A24: now assume sp = sq; then Support(Red(p,T)) = sq \ {HT(q,T)} by A18,TERMORD:36 .= Support(Red(q,T)) by TERMORD:36; hence contradiction by A18; end; set rp = Red(p,T), rq = Red(q,T); p <> 0_(n,L) by A21,POLYNOM7:1; then A25: p is non-zero; q <> 0_(n,L) by A23,POLYNOM7:1; then A26: q is non-zero; then A27: PosetMax(Support(q,T)) = HT(q,T) by Th24; A28: Support rq = Support q \ {HT(q,T)} by TERMORD:36 .= y\{PosetMax y} by A26,Th24; Support rp = Support p \ {HT(p,T)} by TERMORD:36 .= x\{PosetMax x} by A25,Th24; then A29: [x\{PosetMax x},y\{PosetMax y}] in union rng FinOrd-Approx R by A19,A28,BAGORDER:def 15; PosetMax(Support(p,T)) = HT(p,T) by A25,Th24; then [x,y] in union rng FinOrd-Approx R by A18,A21,A23,A27,A29, BAGORDER:35; then [sp,sq] in FinOrd R by BAGORDER:def 15; then p <= q,T; hence p < q,T by A24; end; end; hence p < q,T; end; end; hence p < q,T; end; end; hence p < q,T; end; now assume A30: p < q,T; then p <= q,T; then [sp,sq] in FinOrd R; then A31: [sp,sq] in union rng FinOrd-Approx R by BAGORDER:def 15; A32: Support p <> Support q by A30; now per cases by A31,BAGORDER:35; case x = {}; hence p = 0_(n,L) & q <> 0_(n,L) by A32,POLYNOM7:1; end; case A33: x <> {} & y <> {} & PosetMax x <> PosetMax y & [PosetMax x, PosetMax y] in the InternalRel of R; then q <> 0_(n,L) by POLYNOM7:1; then q is non-zero; then A34: PosetMax(Support(q,T)) = HT(q,T) by Th24; p <> 0_(n,L) by A33,POLYNOM7:1; then p is non-zero; then A35: PosetMax(Support(p,T)) = HT(p,T) by Th24; then HT(p,T) <= HT(q,T),T by A33,A34,TERMORD:def 2; hence HT(p,T) < HT(q,T),T by A33,A35,A34,TERMORD:def 3; end; case A36: x <> {} & y <> {} & PosetMax x = PosetMax y & [x\{PosetMax x} ,y\{PosetMax y}] in union rng FinOrd-Approx R; set rp = Red(p,T), rq = Red(q,T); p <> 0_(n,L) by A36,POLYNOM7:1; then A37: p is non-zero; then A38: PosetMax(Support(p,T)) = HT(p,T) by Th24; q <> 0_(n,L) by A36,POLYNOM7:1; then A39: q is non-zero; then A40: PosetMax(Support(q,T)) = HT(q,T) by Th24; A41: now HT(q,T) in sq by A36,TERMORD:def 6; then for u being object holds u in {HT(q,T)} implies u in sq by TARSKI:def 1; then A42: {HT(q,T)} c= sq by TARSKI:def 3; Support(rq) = sq \ {HT(q,T)} by TERMORD:36; then A43: Support(rq) \/ {HT(q,T)} = sq \/ {HT(q,T)} by XBOOLE_1:39 .= sq by A42,XBOOLE_1:12; HT(p,T) in sp by A36,TERMORD:def 6; then for u being object holds u in {HT(p,T)} implies u in sp by TARSKI:def 1; then A44: {HT(p,T)} c= sp by TARSKI:def 3; Support(rp) = sp \ {HT(p,T)} by TERMORD:36; then A45: Support(rp) \/ {HT(p,T)} = sp \/ {HT(p,T)} by XBOOLE_1:39 .= sp by A44,XBOOLE_1:12; assume Support Red(p,T) = Support Red(q,T); hence contradiction by A30,A36,A38,A40,A45,A43; end; A46: Support(rp,T) = Support p \ {HT(p,T)} by TERMORD:36 .= x\{PosetMax x} by A37,Th24; Support(rq,T) = Support q \ {HT(q,T)} by TERMORD:36 .= y\{PosetMax y} by A39,Th24; then [Support(rp,T),Support(rq,T)] in FinOrd R by A36,A46, BAGORDER:def 15; then Red(p,T) <= Red(q,T),T; hence HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T by A36,A39,A38,A41,Th24 ; end; end; hence p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT(q,T ) & Red(p,T) < Red(q,T),T; end; hence thesis by A1; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T by Lm12; Lm16: for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr , p,q being Polynomial of n,L st q <> 0_(n,L) holds HT(p,T) = HT(q,T) & Red(p, T) <= Red(q,T),T implies p <= q,T proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n,L; assume A1: q <> 0_(n,L); set x = Support(p,T), y = Support(q,T); set rp = Red(p,T), rq = Red(q,T); set R = RelStr(# Bags n, T#); assume that A2: HT(p,T) = HT(q,T) and A3: Red(p,T) <= Red(q,T),T; [Support Red(p,T), Support Red(q,T)] in FinOrd R by A3; then A4: [Support Red(p,T), Support Red(q,T)] in union rng FinOrd-Approx R by BAGORDER:def 15; now per cases; case p = 0_(n,L); hence thesis by Lm12; end; case A5: p <> 0_(n,L); then A6: x <> {} by POLYNOM7:1; A7: q is non-zero by A1; A8: p is non-zero by A5; A9: Support rp = Support p \ {HT(p,T)} by TERMORD:36 .= x\{PosetMax x} by A8,Th24; A10: y <> {} by A1,POLYNOM7:1; A11: Support rq = Support q \ {HT(q,T)} by TERMORD:36 .= y\{PosetMax y} by A7,Th24; PosetMax x = HT(q,T) by A2,A8,Th24 .= PosetMax y by A7,Th24; then [x,y] in union rng FinOrd-Approx R by A4,A6,A10,A9,A11,BAGORDER:35; then [x,y] in FinOrd R by BAGORDER:def 15; hence thesis; end; end; hence thesis; end; theorem Th31: :: according to p. 193 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L) holds ex p being Polynomial of n,L st p in P & for q being Polynomial of n,L st q in P holds p <= q,T proof let n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, P be non empty Subset of Polynom-Ring(n,L); set P9 = { Support(p,T) where p is Polynomial of n,L : p in P}; set p = the Element of P; reconsider p as Polynomial of n,L by POLYNOM1:def 11; Support(p,T) in P9; then reconsider P9 as non empty set; set R = RelStr(#Bags n, T#), FR = FinPoset R; set m = MinElement(P9,FR); A1: FR = RelStr (# Fin the carrier of R, FinOrd R #) by BAGORDER:def 16; now let u be object; assume u in P9; then ex p being Polynomial of n,L st u = Support(p,T) & p in P; hence u in the carrier of FR by A1; end; then A2: P9 c= the carrier of FR by TARSKI:def 3; A3: FR is well_founded by BAGORDER:41; then m in P9 by A2,BAGORDER:def 17; then consider p being Polynomial of n,L such that A4: Support(p,T) = m and A5: p in P; take p; A6: m is_minimal_wrt P9,the InternalRel of FR by A2,A3,BAGORDER:def 17; now let q be Polynomial of n,L; set sq = Support(q,T); assume q in P; then A7: sq in P9; now per cases; case Support p = Support q; hence p <= q,T by Th26; end; case Support p <> Support q; then not([Support(q,T),m]) in the InternalRel of FR by A6,A4,A7, WAYBEL_4:def 25; then not q <= p,T by A1,A4; hence p <= q,T by Th28; end; end; hence p <= q,T; end; hence thesis by A5; end; theorem for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr , p,q being Polynomial of n,L holds p < q,T iff (p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T) by Lm15; theorem Th33: :: exercise 5.16, p. 194 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < HM(p,T),T proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n,L; set red = Red(p,T), htp = HT(p,T); set sred = Support red, sp = Support HM(p,T), R = RelStr(#Bags n, T#); p <> 0_(n,L) by POLYNOM7:def 1; then A1: Support p <> {} by POLYNOM7:1; per cases; suppose red = 0_(n,L); then A2: sred = {} by POLYNOM7:1; htp in Support p by A1,TERMORD:def 6; then p.htp <> 0.L by POLYNOM1:def 4; then HM(p,T).htp <> 0.L by TERMORD:18; then A3: htp in Support HM(p,T) by POLYNOM1:def 4; dom (FinOrd-Approx R) = NAT by BAGORDER:def 14; then A4: (FinOrd-Approx R).0 in rng FinOrd-Approx R by FUNCT_1:3; sred is Element of Fin the carrier of R & sp is Element of Fin the carrier of R by Lm11; then [sred,sp] in {[x,y] where x, y is Element of Fin the carrier of R : x = {} or (x<>{} & y <> {} & PosetMax x <> PosetMax y & [PosetMax x,PosetMax y] in the InternalRel of R)} by A2; then [sred,sp] in (FinOrd-Approx R).0 by BAGORDER:def 14; then [sred,sp] in union rng FinOrd-Approx R by A4,TARSKI:def 4; then [sred,sp] in FinOrd R by BAGORDER:def 15; then red <= HM(p,T),T; hence thesis by A2,A3; end; suppose red <> 0_(n,L); then Support red <> {} by POLYNOM7:1; then A5: HT(red,T) in Support red by TERMORD:def 6; A6: now assume HT(red,T) = htp; then red.(HT(red,T)) = 0.L by TERMORD:39; hence contradiction by A5,POLYNOM1:def 4; end; Support(red) c= Support(p) by TERMORD:35; then HT(red,T) <= htp,T by A5,TERMORD:def 6; then HT(red,T) < htp,T by A6,TERMORD:def 3; then HT(red,T) < HT(HM(p,T),T),T by TERMORD:26; hence thesis by Lm15; end; end; theorem Th34: :: exercise 5.16, p. 194 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being Polynomial of n,L holds HM(p,T) <= p,T proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p9 be Polynomial of n,L; per cases; suppose A1: p9 = 0_(n,L); now assume Support(HM(p9,T)) <> {}; then consider u being bag of n such that A2: Support(HM(p9,T)) = {u} by POLYNOM7:6; A3: u in Support(HM(p9,T)) by A2,TARSKI:def 1; now let v be bag of n; assume v in Support(HM(p9,T)); then u = v by A2,TARSKI:def 1; hence v <= u,T by TERMORD:6; end; then A4: HT(HM(p9,T),T) = u by A3,TERMORD:def 6; 0.L = p9.(HT(p9,T)) by A1,POLYNOM1:22 .= HC(p9,T) by TERMORD:def 7 .= HC(HM(p9,T),T) by TERMORD:27 .= HM(p9,T).u by A4,TERMORD:def 7; hence contradiction by A3,POLYNOM1:def 4; end; then HM(p9,T) = 0_(n,L) by POLYNOM7:1; hence thesis by A1,Th25; end; suppose p9 <> 0_(n,L); then reconsider p = p9 as non-zero Polynomial of n,L by POLYNOM7:def 1; set hmp = HM(p,T), R = RelStr(#Bags n,T#); set x = Support(hmp,T), y = Support(p,T); A5: x\{PosetMax x} is Element of Fin the carrier of R & y\{PosetMax y} is Element of Fin the carrier of R by BAGORDER:37; A6: PosetMax(x) = HT(hmp,T) by Th24 .= HT(p,T) by TERMORD:26; p <> 0_(n,L) by POLYNOM7:def 1; then A7: Support p <> {} by POLYNOM7:1; hmp.(HT(p,T)) = p.(HT(p,T)) by TERMORD:18 .= HC(p,T) by TERMORD:def 7; then A8: hmp.(HT(p,T)) <> 0.L; then A9: x <> {} by POLYNOM1:def 4; HT(p,T) in Support(hmp) by A8,POLYNOM1:def 4; then Support hmp = {HT(p,T)} by TERMORD:21; then x\{PosetMax x} = {} by A6,XBOOLE_1:37; then A10: [x\{PosetMax x},y\{PosetMax y}] in union rng FinOrd-Approx R by A5, BAGORDER:35; PosetMax(x) = PosetMax(y) by A6,Th24; then [x,y] in union rng FinOrd-Approx R by A7,A9,A10,BAGORDER:35; then [x,y] in FinOrd R by BAGORDER:def 15; hence thesis; end; end; theorem Th35: for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < p,T proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n,L; (Red(p,T)).(HT(p,T)) = 0.L by TERMORD:39; then A1: not HT(p,T) in Support(Red(p,T)) by POLYNOM1:def 4; p <> 0_(n,L) by POLYNOM7:def 1; then Support p <> {} by POLYNOM7:1; then A2: HT(p,T) in Support p by TERMORD:def 6; Red(p,T) < HM(p,T),T by Th33; then A3: Red(p,T) <= HM(p,T),T; HM(p,T) <= p,T by Th34; then Red(p,T) <= p,T by A3,Th27; hence thesis by A2,A1; end; begin :: Polynomial Reduction definition :: definition 5.18 (i), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L, b be bag of n; pred f reduces_to g,p,b,T means f <> 0_(n,L) & p <> 0_(n,L) & b in Support f & ex s being bag of n st s + HT(p,T) = b & g = f - (f.b/HC(p,T)) * (s *' p); end; definition :: definition 5.18 (ii), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L; pred f reduces_to g,p,T means ex b being bag of n st f reduces_to g,p ,b,T; end; definition :: definition 5.18 (iii), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f reduces_to g,P,T means ex p being Polynomial of n,L st p in P & f reduces_to g,p,T; end; definition :: definition 5.18 (iv), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; pred f is_reducible_wrt p,T means ex g being Polynomial of n,L st f reduces_to g,p,T; end; notation :: definition 5.18 (iv), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T; antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T; end; definition :: definition 5.18 (v), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_reducible_wrt P,T means ex g being Polynomial of n,L st f reduces_to g,P,T; end; notation :: definition 5.18 (v), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T; antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L; pred f top_reduces_to g,p,T means f reduces_to g,p,HT(f,T),T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; pred f is_top_reducible_wrt p,T means ex g being Polynomial of n,L st f top_reduces_to g,p,T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_top_reducible_wrt P,T means ex p being Polynomial of n,L st p in P & f is_top_reducible_wrt p,T; end; theorem :: lemma 5.20 (i), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f being Polynomial of n,L, p being non-zero Polynomial of n,L holds f is_reducible_wrt p,T iff ex b being bag of n st b in Support f & HT(p,T) divides b proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, p be non-zero Polynomial of n,L; A1: now A2: p <> 0_(n,L) by POLYNOM7:def 1; assume ex b being bag of n st b in Support f & HT(p,T) divides b; then consider b being bag of n such that A3: b in Support f and A4: HT(p,T) divides b; consider s being bag of n such that A5: b = HT(p,T) + s by A4,TERMORD:1; set g = f - ((f.b)/HC(p,T)) * (s *' p); f <> 0_(n,L) by A3,POLYNOM7:1; then f reduces_to g,p,b,T by A3,A5,A2; then f reduces_to g,p,T; hence f is_reducible_wrt p,T; end; now assume f is_reducible_wrt p,T; then consider g being Polynomial of n,L such that A6: f reduces_to g,p,T; consider b being bag of n such that A7: f reduces_to g,p,b,T by A6; ex s being bag of n st s + HT(p,T) = b & g = f - (f.b)/HC(p,T) * (s *' p ) by A7; then A8: HT(p,T) divides b by TERMORD:1; b in Support f by A7; hence ex b being bag of n st b in Support f & HT(p,T) divides b by A8; end; hence thesis by A1; end; Lm17: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f, p,g being Polynomial of n,L, b being bag of n holds f reduces_to g,p,b,T implies not(b in Support g) proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L, b be bag of n; assume A1: f reduces_to g,p,b,T; then b in Support f & ex s being bag of n st s + HT(p,T) = b & g = f - (f.b)/ HC(p,T) * (s *' p ); then consider s being bag of n such that b in Support f and A2: s + HT(p,T) = b and A3: g = f - (f.b)/HC(p,T) * (s *' p); p <> 0_(n,L) by A1; then A4: HC(p,T) <> 0.L by TERMORD:17; set q = (f.b)/HC(p,T) * (s *' p); A5: q.b = (f.b)/HC(p,T) * (s *' p).b by POLYNOM7:def 9 .= (f.b)/HC(p,T) * p.HT(p,T) by A2,Lm9 .= ((f.b)/HC(p,T)) * HC(p,T) by TERMORD:def 7 .= ((f.b) * HC(p,T)") * HC(p,T) .= (f.b) * (HC(p,T)" * HC(p,T)) by GROUP_1:def 3 .= f.b * 1.L by A4,VECTSP_1:def 10 .= f.b; g = f + (-q) by A3,POLYNOM1:def 7; then g.b = f.b + (-q).b by POLYNOM1:15 .= f.b + (-q.b) by POLYNOM1:17 .= 0.L by A5,RLVECT_1:5; hence thesis by POLYNOM1:def 4; end; theorem Th37: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p being Polynomial of n,L holds 0_(n,L) is_irreducible_wrt p,T proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n,L; assume 0_(n,L) is_reducible_wrt p,T; then consider g being Polynomial of n,L such that A1: 0_(n,L) reduces_to g,p,T; ex b being bag of n st 0_(n,L) reduces_to g,p,b,T by A1; hence thesis; end; theorem :: lemma 5.20 (ii), p. 197 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to f-m*'p,p,T implies HT(m*'p,T) in Support f proof let n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p be Polynomial of n,L, m be non-zero Monomial of n,L; assume f reduces_to f-m*'p,p,T; then consider b being bag of n such that A1: f reduces_to f-m*'p,p,b,T; A2: p <> 0_(n,L) by A1; then A3: p is non-zero; A4: HC(p,T) <> 0.L by A2,TERMORD:17; A5: now assume (HC(p,T))" = 0.L; then 0.L = HC(p,T) * (HC(p,T))" .= 1.L by A4,VECTSP_1:def 10; hence contradiction; end; b in Support f by A1; then f.b <> 0.L by POLYNOM1:def 4; then f.b * (HC(p,T))" <> 0.L by A5,VECTSP_2:def 1; then (f.b)/HC(p,T) <> 0.L; then A6: (f.b)/HC(p,T) is non zero; consider s being bag of n such that A7: s + HT(p,T) = b and A8: f-m*'p = f-(((f.b)/HC(p,T)) * (s *' p)) by A1; A9: (f.b)/HC(p,T) * (s *' p) = -- ((f.b)/HC(p,T) * (s *' p)) by POLYNOM1:19; f = f + 0_(n,L) by POLYNOM1:23 .= f + (m*'p - m*' p) by POLYNOM1:24 .= f + (m*'p + -(m*'p)) by POLYNOM1:def 7 .= (f + -(m*'p)) + m*'p by POLYNOM1:21 .= m*'p + (f -(f.b)/HC(p,T) * (s *' p)) by A8,POLYNOM1:def 7; then 0_(n,L) = f - (m*'p + (f -(f.b)/HC(p,T) * (s *' p))) by POLYNOM1:24 .= f + -((m*'p) + (f -(f.b)/HC(p,T) * (s *' p))) by POLYNOM1:def 7 .= f + (-(m*'p) + -(f -(f.b)/HC(p,T) * (s *' p))) by Th1 .= f + (-(m*'p) + -(f + -(f.b)/HC(p,T) * (s *' p))) by POLYNOM1:def 7 .= f + (-(m*'p) + (-f + -(-((f.b)/HC(p,T) * (s *' p))))) by Th1 .= f + (-f + (-(m*'p) + (f.b)/HC(p,T) * (s *' p))) by A9,POLYNOM1:21 .= (f + -f) + (-(m*'p) + (f.b)/HC(p,T) * (s *' p)) by POLYNOM1:21 .= (f - f) + (-(m*'p) + (f.b)/HC(p,T) * (s *' p)) by POLYNOM1:def 7 .= 0_(n,L) + (-(m*'p) + (f.b)/HC(p,T) * (s *' p)) by POLYNOM1:24 .= -(m*'p) + (f.b)/HC(p,T) * (s *' p) by Th2; then m*'p = m*'p + (- m*'p + (f.b)/HC(p,T) * (s *' p)) by POLYNOM1:23 .= (m*'p + - m*'p) + (f.b)/HC(p,T) * (s *' p) by POLYNOM1:21 .= (m*'p - m*'p) + (f.b)/HC(p,T) * (s *' p) by POLYNOM1:def 7 .= 0_(n,L) + (f.b)/HC(p,T) * (s *' p) by POLYNOM1:24 .= (f.b)/HC(p,T) * (s *' p) by Th2; then HT(m*'p,T) = HT(s*'p,T) by A6,Th21 .= b by A7,A3,Th15; hence thesis by A1; end; theorem :: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L, b being bag of n holds f reduces_to g,p,b,T implies not(b in Support g) by Lm17; theorem Th40: :: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T holds f reduces_to g,p,b,T implies (b9 in Support g iff b9 in Support f) proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f, p,g be Polynomial of n,L, b,b9 be bag of n; assume A1: b < b9,T; assume f reduces_to g,p,b,T; then consider s being bag of n such that A2: s + HT(p,T) = b and A3: g = f - (f.b/HC(p,T)) * (s *' p); A4: b9 is Element of Bags n by PRE_POLY:def 12; A5: now assume b9 in Support(s*'p); then A6: b9 <= b,T by A2,Th16; b <= b9,T by A1,TERMORD:def 3; then b = b9 by A6,TERMORD:7; hence contradiction by A1,TERMORD:def 3; end; A7: now A8: ((f.b/HC(p,T)) * (s *' p)).b9 = (f.b/HC(p,T)) * (s *' p).b9 by POLYNOM7:def 9 .= (f.b/HC(p,T)) * 0.L by A4,A5,POLYNOM1:def 4 .= 0.L; assume A9: b9 in Support f; (f - (f.b/HC(p,T)) * (s *' p)).b9 = (f + -((f.b/HC(p,T)) * (s *' p))) .b9 by POLYNOM1:def 7 .= f.b9 + (-(f.b/HC(p,T) * (s *' p))).b9 by POLYNOM1:15 .= f.b9 + -0.L by A8,POLYNOM1:17 .= f.b9 + 0.L by RLVECT_1:12 .= f.b9 by RLVECT_1:def 4; then g.b9 <> 0.L by A3,A9,POLYNOM1:def 4; hence b9 in Support g by A4,POLYNOM1:def 4; end; now A10: ((f.b/HC(p,T)) * (s *' p)).b9 = (f.b/HC(p,T)) * (s *' p).b9 by POLYNOM7:def 9 .= (f.b/HC(p,T)) * 0.L by A4,A5,POLYNOM1:def 4 .= 0.L; assume A11: b9 in Support g; (f - (f.b/HC(p,T)) * (s *' p)).b9 = (f + -((f.b/HC(p,T)) * (s *' p))) .b9 by POLYNOM1:def 7 .= f.b9 + (-(f.b/HC(p,T) * (s *' p))).b9 by POLYNOM1:15 .= f.b9 + -0.L by A10,POLYNOM1:17 .= f.b9 + 0.L by RLVECT_1:12 .= f.b9 by RLVECT_1:def 4; then f.b9 <> 0.L by A3,A11,POLYNOM1:def 4; hence b9 in Support f by A4,POLYNOM1:def 4; end; hence thesis by A7; end; theorem Th41: for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T holds f reduces_to g,p,b,T implies f.b9 = g.b9 proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f, p,g be Polynomial of n,L, b,b9 be bag of n; assume A1: b < b9,T; assume f reduces_to g,p,b,T; then consider s being bag of n such that A2: s + HT(p,T) = b and A3: g = f - (f.b/HC(p,T)) * (s *' p); A4: now assume b9 in Support(s*'p); then A5: b9 <= b,T by A2,Th16; b <= b9,T by A1,TERMORD:def 3; then b = b9 by A5,TERMORD:7; hence contradiction by A1,TERMORD:def 3; end; A6: b9 is Element of Bags n by PRE_POLY:def 12; A7: ((f.b/HC(p,T)) * (s *' p)).b9 = (f.b/HC(p,T)) * (s *' p).b9 by POLYNOM7:def 9 .= (f.b/HC(p,T)) * 0.L by A6,A4,POLYNOM1:def 4 .= 0.L; (f - (f.b/HC(p,T)) * (s *' p)).b9 = (f + -((f.b/HC(p,T)) * (s *' p))). b9 by POLYNOM1:def 7 .= f.b9 + (-(f.b/HC(p,T) * (s *' p))).b9 by POLYNOM1:15 .= f.b9 + -0.L by A7,POLYNOM1:17 .= f.b9 + 0.L by RLVECT_1:12 .= f.b9 by RLVECT_1:def 4; hence thesis by A3; end; theorem Th42: for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p, T implies for b being bag of n st b in Support g holds b <= HT(f,T),T proof let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n,L; A1: T is_connected_in field T by RELAT_2:def 14; assume f reduces_to g,p,T; then consider b being bag of n such that A2: f reduces_to g,p,b,T; b in Support f by A2; then A3: b <= HT(f,T),T by TERMORD:def 6; now let u be bag of n; assume A4: u in Support g; now per cases; case u = b; hence contradiction by A2,A4,Lm17; end; case A5: u <> b; b <= b,T by TERMORD:6; then [b,b] in T by TERMORD:def 2; then A6: b in field T by RELAT_1:15; u <= u,T by TERMORD:6; then [u,u] in T by TERMORD:def 2; then u in field T by RELAT_1:15; then A7: [u,b] in T or [b,u] in T by A1,A5,A6,RELAT_2:def 6; now per cases by A7,TERMORD:def 2; case u <= b,T; hence u <= HT(f,T),T by A3,TERMORD:8; end; case b <= u,T; then b < u,T by A5,TERMORD:def 3; then u in Support f iff u in Support g by A2,Th40; hence u <= HT(f,T),T by A4,TERMORD:def 6; end; end; hence u <= HT(f,T),T; end; end; hence u <= HT(f,T),T; end; hence thesis; end; theorem Th43: :: lemma 5.20 (iv), p. 197 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p, T implies g < f,T proof let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n,L; set R = RelStr(#Bags n, T#); defpred P[Nat] means for f,p,g being Polynomial of n,L holds card(Support f) = \$1 & f reduces_to g,p,T implies [Support g,Support f] in FinOrd R; A1: ex k being Nat st card(Support f) = k; assume A2: f reduces_to g,p,T; then consider b being bag of n such that A3: f reduces_to g,p,b,T; A4: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: for f,p,g being Polynomial of n,L holds card(Support f) = k & f reduces_to g,p,T implies [Support g,Support f] in FinOrd R; now A6: T is_connected_in field T by RELAT_2:def 14; let f,p,g be Polynomial of n,L; assume that A7: card(Support f) = k+1 and A8: f reduces_to g,p,T; consider b being bag of n such that A9: f reduces_to g,p,b,T by A8; consider s being bag of n such that A10: s + HT(p,T) = b and A11: g = f - (f.b/HC(p,T)) * (s *' p) by A9; A12: b in Support f by A9; A13: f <> 0_(n,L) by A9; now per cases; case A14: HT(f,T) <> HT(g,T); HT(g,T) <= HT(g,T),T by TERMORD:6; then [HT(g,T),HT(g,T)] in T by TERMORD:def 2; then A15: HT(g,T) in field T by RELAT_1:15; HT(f,T) <= HT(f,T),T by TERMORD:6; then [HT(f,T),HT(f,T)] in T by TERMORD:def 2; then HT(f,T) in field T by RELAT_1:15; then A16: [HT(f,T),HT(g,T)] in T or [HT(g,T),HT(f,T)] in T by A6,A14,A15, RELAT_2:def 6; now per cases by A16,TERMORD:def 2; case A17: HT(f,T) <= HT(g,T),T; now assume not HT(g,T) in Support g; then HT(g,T) = EmptyBag n by TERMORD:def 6; then [HT(g,T),HT(f,T)] in T by BAGORDER:def 5; then HT(g,T) <= HT(f,T),T by TERMORD:def 2; hence contradiction by A14,A17,TERMORD:7; end; then HT(g,T) <= HT(f,T),T by A8,Th42; hence [Support g,Support f] in FinOrd R by A14,A17,TERMORD:7; end; case HT(g,T) <= HT(f,T),T; then HT(g,T) < HT(f,T),T by A14,TERMORD:def 3; then g < f,T by Lm15; then g <= f,T; hence [Support g,Support f] in FinOrd R; end; end; hence [Support g,Support f] in FinOrd R; end; case A18: HT(g,T) = HT(f,T); now per cases; case b = HT(f,T); then not HT(g,T) in Support g by A9,A18,Lm17; then Support g = {} by TERMORD:def 6; then g = 0_(n,L) by POLYNOM7:1; then g <= f,T by Lm12; hence [Support g,Support f] in FinOrd R; end; case A19: b <> HT(f,T); HT(f,T) in Support f by A12,TERMORD:def 6; then for u being object holds u in {HT(f,T)} implies u in Support f by TARSKI:def 1; then A20: {HT(f,T)} c= Support f by TARSKI:def 3; A21: Support(Red(f,T)) = Support(f) \ {HT(f,T)} by TERMORD:36; not b in {HT(f,T)} by A19,TARSKI:def 1; then A22: b in Support Red(f,T) by A12,A21,XBOOLE_0:def 5; then Red(f,T) <> 0_(n,L) by POLYNOM7:1; then reconsider rf = Red(f,T) as non-zero Polynomial of n,L by POLYNOM7:def 1; A23: rf <> 0_(n,L) & p <> 0_(n,L) by A9,POLYNOM7:def 1; b <= HT(f,T),T by A12,TERMORD:def 6; then b < HT(f,T),T by A19,TERMORD:def 3; then f.(HT(f,T)) = g.(HT(g,T)) by A9,A18,Th41; then HC(f,T) = g.(HT(g,T)) by TERMORD:def 7 .= HC(g,T) by TERMORD:def 7; then HM(f,T) = Monom(HC(g,T),HT(g,T)) by A18,TERMORD:def 8 .= HM(g,T) by TERMORD:def 8; then Red(g,T) = (f - (f.b/HC(p,T)) * (s *' p)) - HM(f,T) by A11, TERMORD:def 9 .= ((HM(f,T) + rf) - (f.b/HC(p,T)) * (s *' p)) - HM(f,T) by TERMORD:38 .= ((HM(f,T) + rf) - (rf.b/HC(p,T)) * (s *' p)) - HM(f,T) by A12,A19,TERMORD:40 .= ((HM(f,T) + rf) + -((rf.b/HC(p,T)) * (s *' p))) - HM(f,T) by POLYNOM1:def 7 .= (HM(f,T) + (rf + -(rf.b/HC(p,T)) * (s *' p))) - HM(f,T) by POLYNOM1:21 .= (HM(f,T) + (rf + -(rf.b/HC(p,T)) * (s *' p))) + -HM(f,T) by POLYNOM1:def 7 .= (rf + -(rf.b/HC(p,T)) * (s *' p)) + (HM(f,T) + - HM(f,T)) by POLYNOM1:21 .= (rf - (rf.b/HC(p,T)) * (s *' p)) + (HM(f,T) + - HM(f,T)) by POLYNOM1:def 7 .= (rf - (rf.b/HC(p,T)) * (s *' p)) + (HM(f,T) - HM(f,T)) by POLYNOM1:def 7 .= (rf - (rf.b/HC(p,T)) * (s *' p)) + 0_(n,L) by POLYNOM1:24 .= rf - (rf.b/HC(p,T)) * (s *' p) by POLYNOM1:23; then rf reduces_to Red(g,T),p,b,T by A10,A22,A23; then A24: rf reduces_to Red(g,T),p,T; HT(f,T) in {HT(f,T)} by TARSKI:def 1; then A25: not HT(f,T) in Support Red(f,T) by A21,XBOOLE_0:def 5; Support(Red(f,T)) \/ {HT(f,T)} = Support f \/ {HT(f,T)} by A21, XBOOLE_1:39 .= Support f by A20,XBOOLE_1:12; then card(Support(Red(f,T))) + 1 = k + 1 by A7,A25,CARD_2:41; then [Support Red(g,T),Support rf] in FinOrd R by A5,A24, XCMPLX_1:2; then Red(g,T) <= Red(f,T),T; then g <= f,T by A13,A18,Lm16; hence [Support g,Support f] in FinOrd R; end; end; hence [Support g,Support f] in FinOrd R; end; end; hence [Support g,Support f] in FinOrd R; end; hence thesis; end; A26: P[0] proof let f,p,g be Polynomial of n,L; assume that A27: card(Support f) = 0 and A28: f reduces_to g,p,T; Support f = {} by A27; then f = 0_(n,L) by POLYNOM7:1; then f is_irreducible_wrt p,T by Th37; hence thesis by A28; end; for k being Nat holds P[k] from NAT_1:sch 2(A26,A4); then [Support g,Support f] in FinOrd R by A2,A1; then A29: g <= f,T; Support f <> Support g by A3,Lm17; hence thesis by A29; end; begin :: Polynomial Reduction Relation definition let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L); func PolyRedRel(P,T) -> Relation of NonZero Polynom-Ring(n,L), the carrier of Polynom-Ring(n,L) means :Def13: for p,q being Polynomial of n,L holds [p,q] in it iff p reduces_to q,P,T; existence proof defpred P[object,object] means ex p,q being Polynomial of n,L st p = \$1 & q = \$2 & p reduces_to q,P,T; set A = NonZero Polynom-Ring(n,L), B = the carrier of Polynom-Ring(n,L); consider R being Relation of A,B such that A1: for x,y being object holds [x,y] in R iff x in A & y in B & P[x,y] from RELSET_1:sch 1; take R; now let p,q be Polynomial of n,L; A2: now assume A3: p reduces_to q,P,T; then consider pp being Polynomial of n,L such that pp in P and A4: p reduces_to q,pp,T; ex b being bag of n st p reduces_to q,pp,b,T by A4; then p <> 0_(n,L); then A5: not p in {0_(n,L)} by TARSKI:def 1; A6: q in B by POLYNOM1:def 11; 0_(n,L) = 0.Polynom-Ring(n,L) & p in the carrier of Polynom-Ring( n,L) by POLYNOM1:def 11; then p in A by A5,XBOOLE_0:def 5; hence [p,q] in R by A1,A3,A6; end; now assume [p,q] in R; then P[p,q] by A1; hence p reduces_to q,P,T; end; hence [p,q] in R iff p reduces_to q,P,T by A2; end; hence thesis; end; uniqueness proof set A = NonZero Polynom-Ring(n,L), B = the carrier of Polynom-Ring(n,L); let R1,R2 be Relation of NonZero Polynom-Ring(n,L), the carrier of Polynom-Ring(n,L) such that A7: for p,q being Polynomial of n,L holds [p,q] in R1 iff p reduces_to q,P,T and A8: for p,q being Polynomial of n,L holds [p,q] in R2 iff p reduces_to q,P,T; for p,q being object holds [p,q] in R1 iff [p,q] in R2 proof let p,q be object; A9: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; A10: now assume A11: [p,q] in R2; then consider p9,q9 being object such that A12: [p,q] = [p9,q9] and A13: p9 in A and A14: q9 in B by RELSET_1:2; reconsider p9,q9 as Polynomial of n,L by A13,A14,POLYNOM1:def 11; not p9 in {0_(n,L)} by A9,A13,XBOOLE_0:def 5; then p9 <> 0_(n,L) by TARSKI:def 1; then reconsider p9 as non-zero Polynomial of n,L by POLYNOM7:def 1; A15: p = p9 by A12,XTUPLE_0:1; A16: q = q9 by A12,XTUPLE_0:1; p9 reduces_to q9,P,T by A8,A11,A12; hence [p,q] in R1 by A7,A15,A16; end; now assume A17: [p,q] in R1; then consider p9,q9 being object such that A18: [p,q] = [p9,q9] and A19: p9 in A and A20: q9 in B by RELSET_1:2; reconsider p9,q9 as Polynomial of n,L by A19,A20,POLYNOM1:def 11; not p9 in {0_(n,L)} by A9,A19,XBOOLE_0:def 5; then p9 <> 0_(n,L) by TARSKI:def 1; then reconsider p9 as non-zero Polynomial of n,L by POLYNOM7:def 1; A21: p = p9 by A18,XTUPLE_0:1; A22: q = q9 by A18,XTUPLE_0:1; p9 reduces_to q9,P,T by A7,A17,A18; hence [p,q] in R2 by A8,A21,A22; end; hence thesis by A10; end; hence thesis by RELAT_1:def 2; end; end; Lm18: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f, g,p being Polynomial of n,L st f reduces_to g,p,T holds f <> 0_(n,L) & p <> 0_( n,L) proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g,p be Polynomial of n,L; assume f reduces_to g,p,T; then ex b being bag of n st f reduces_to g,p,b,T; hence thesis; end; theorem :: lemma 5.20 (v), p. 197 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,g being Polynomial of n,L, P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies g <= f,T & (g = 0_( n,L) or HT(g,T) <= HT(f,T),T) proof let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,g be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); set R = PolyRedRel(P,T); defpred P[Nat] means for f,g being Polynomial of n,L st PolyRedRel(P,T) reduces f,g for p being RedSequence of R st p.1 = f & p.len p = g & len p = \$1 holds g <= f,T; assume A1: PolyRedRel(P,T) reduces f,g; then consider p being RedSequence of R such that A2: p.1 = f & p.len p = g by REWRITE1:def 3; A3: now let k be Nat; assume A4: 1 <= k; thus P[k] implies P[k+1] proof assume A5: P[k]; now let f,g be Polynomial of n,L; assume PolyRedRel(P,T) reduces f,g; let p be RedSequence of R; assume that A6: p.1 = f and A7: p.len p = g and A8: len p = k+1; A9: dom p = Seg(k+1) by A8,FINSEQ_1:def 3; then A10: k+1 in dom p by FINSEQ_1:4; set q = p|(Seg k); reconsider q as FinSequence by FINSEQ_1:15; A11: k <= k+1 by NAT_1:11; then A12: dom q = Seg k by A8,FINSEQ_1:17; then A13: k in dom q by A4,FINSEQ_1:1; set h = q.len q; A14: len q = k by A8,A11,FINSEQ_1:17; k in dom p by A4,A9,A11,FINSEQ_1:1; then [p.k,p.(k+1)] in R by A10,REWRITE1:def 2; then A15: [h,g] in R by A7,A8,A14,A13,FUNCT_1:47; then consider h9,g9 being object such that A16: [h,g] = [h9,g9] and A17: h9 in NonZero Polynom-Ring(n,L) and g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; A18: h = h9 by A16,XTUPLE_0:1; A19: now let i be Nat; assume that A20: i in dom q and A21: i+1 in dom q; i+1 <= k by A12,A21,FINSEQ_1:1; then A22: i+1 <= k+1 by A11,XXREAL_0:2; i <= k by A12,A20,FINSEQ_1:1; then A23: i <= k+1 by A11,XXREAL_0:2; 1 <= i+1 by A12,A21,FINSEQ_1:1; then A24: i+1 in dom p by A9,A22,FINSEQ_1:1; 1 <= i by A12,A20,FINSEQ_1:1; then i in dom p by A9,A23,FINSEQ_1:1; then A25: [p.i, p.(i+1)] in R by A24,REWRITE1:def 2; p.i = q.i by A20,FUNCT_1:47; hence [q.i, q.(i+1)] in R by A21,A25,FUNCT_1:47; end; 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; then not h9 in {0_(n,L)} by A17,XBOOLE_0:def 5; then h9 <> 0_(n,L) by TARSKI:def 1; then reconsider h as non-zero Polynomial of n,L by A17,A18, POLYNOM1:def 11,POLYNOM7:def 1; reconsider q as RedSequence of R by A4,A14,A19,REWRITE1:def 2; 1 in dom q by A4,A12,FINSEQ_1:1; then A26: q.1 = f by A6,FUNCT_1:47; then PolyRedRel(P,T) reduces f,h by REWRITE1:def 3; then A27: h <= f,T by A5,A8,A11,A26,FINSEQ_1:17; h reduces_to g,P,T by A15,Def13; then A28: ex r being Polynomial of n,L st r in P & h reduces_to g, r,T; reconsider h as non-zero Polynomial of n,L; g < h,T by A28,Th43; then g <= h,T; hence g <= f,T by A27,Th27; end; hence thesis; end; end; A29: P[1] by Th25; A30: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A29,A3); consider k being Nat such that A31: len p = k; 1 <= k by A31,NAT_1:14; hence A32: g <= f,T by A1,A30,A2,A31; now assume g <> 0_(n,L); then Support g <> {} by POLYNOM7:1; then A33: HT(g,T) in Support g by TERMORD:def 6; assume A34: not HT(g,T) <= HT(f,T),T; now per cases; case HT(f,T) = HT(g,T); hence contradiction by A34,TERMORD:6; end; case A35: HT(f,T) <> HT(g,T); HT(g,T) <= HT(g,T),T by TERMORD:6; then [HT(g,T),HT(g,T)] in T by TERMORD:def 2; then A36: HT(g,T) in field T by RELAT_1:15; HT(f,T) <= HT(f,T),T by TERMORD:6; then [HT(f,T),HT(f,T)] in T by TERMORD:def 2; then T is_connected_in field T & HT(f,T) in field T by RELAT_1:15 ,RELAT_2:def 14; then [HT(f,T),HT(g,T)] in T or [HT(g,T),HT(f,T)] in T by A35,A36, RELAT_2:def 6; then HT(f,T) <= HT(g,T),T by A34,TERMORD:def 2; then A37: HT(f,T) < HT(g,T),T by A35,TERMORD:def 3; then f < g,T by Lm15; then f <= g,T; then Support f = Support g by A32,Th26; then HT(g,T) <= HT(f,T),T by A33,TERMORD:def 6; hence contradiction by A37,TERMORD:5; end; end; hence contradiction; end; hence thesis; end; registration :: theorem 5.21, p. 198 let n be Nat, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L); cluster PolyRedRel(P,T) -> strongly-normalizing; coherence proof set BT = RelStr(#Bags n,T#), X = the InternalRel of (FinPoset BT); set R = PolyRedRel(P,T); A1: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; FinPoset BT is well_founded by BAGORDER:41; then A2: the InternalRel of (FinPoset BT) is_well_founded_in the carrier of ( FinPoset BT) by WELLFND1:def 2; now let Y be set; assume that A3: Y c= field (R~) and A4: Y <> {}; set z = the Element of Y; z in Y by A4; then z in field(R~) by A3; then A5: z in dom(R~) \/ rng(R~) by RELAT_1:def 6; now per cases by A5,XBOOLE_0:def 3; case z in dom(R~); hence z in the carrier of Polynom-Ring(n,L); end; case z in rng(R~); hence z in the carrier of Polynom-Ring(n,L) by XBOOLE_0:def 5; end; end; then reconsider z9 = z as Polynomial of n,L by POLYNOM1:def 11; set M = { Support y9 where y9 is Polynomial of n,L : ex y being set st y in Y & y9 = y }; Support z9 in M by A4; then reconsider M as non empty set; now let u be object; assume u in M; then A6: ex p being Polynomial of n,L st Support p = u & ex y being set st y in Y & p = y; FinPoset BT = RelStr(#Fin(the carrier of BT),FinOrd BT#) by BAGORDER:def 16; hence u in the carrier of (FinPoset BT) by A6,FINSUB_1:def 5; end; then M c= the carrier of (FinPoset BT) by TARSKI:def 3; then consider a being object such that A7: a in M and A8: X-Seg a misses M by A2,WELLORD1:def 3; consider p being Polynomial of n,L such that A9: Support p = a and A10: ex y being set st y in Y & p = y by A7; (R~)-Seg p /\ Y = {} proof set b = the Element of (R~)-Seg p /\ Y; A11: FinPoset BT = RelStr (# Fin(the carrier of BT),FinOrd BT #) by BAGORDER:def 16; assume A12: (R~)-Seg p /\ Y <> {}; then b in (R~)-Seg p by XBOOLE_0:def 4; then [b,p] in R~ by WELLORD1:1; then A13: [p,b] in R by RELAT_1:def 7; then consider h9,g9 being object such that A14: [p,b] = [h9,g9] and A15: h9 in NonZero Polynom-Ring(n,L) and A16: g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; b = g9 by A14,XTUPLE_0:1; then reconsider b9 = b as Polynomial of n,L by A16,POLYNOM1:def 11; A17: p = h9 by A14,XTUPLE_0:1; not h9 in {0_(n,L)} by A1,A15,XBOOLE_0:def 5; then h9 <> 0_(n,L) by TARSKI:def 1; then reconsider p as non-zero Polynomial of n,L by A17,POLYNOM7:def 1; p reduces_to b9,P,T by A13,Def13; then A18: ex u being Polynomial of n,L st u in P & p reduces_to b9,u,T; reconsider p as non-zero Polynomial of n,L; A19: b9 < p,T by A18,Th43; then A20: Support b9 <> Support p; b in Y by A12,XBOOLE_0:def 4; then A21: (Support b9) in M; b9 <= p,T by A19; then [Support b9,Support p] in X by A11; then (Support b9) in X-Seg (Support p) by A20,WELLORD1:1; then (Support b9) in X-Seg a /\ M by A9,A21,XBOOLE_0:def 4; hence contradiction by A8,XBOOLE_0:def 7; end; then (R~)-Seg p misses Y by XBOOLE_0:def 7; hence ex p being object st p in Y & (R~)-Seg p misses Y by A10; end; then R~ is well_founded by WELLORD1:def 2; then A22: R is co-well_founded by REWRITE1:def 13; now set A = (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}, B = the carrier of Polynom-Ring(n,L); let x be object; assume x in field R; then A23: x in dom R \/ rng R by RELAT_1:def 6; now per cases by A23,XBOOLE_0:def 3; case x in dom R; then x in B by XBOOLE_0:def 5; hence x is Polynomial of n,L by POLYNOM1:def 11; end; case x in rng R; hence x is Polynomial of n,L by POLYNOM1:def 11; end; end; then reconsider x9 = x as Polynomial of n,L; now assume A24: [x,x] in R; then consider x1,y1 being object such that A25: [x,x] = [x1,y1] and A26: x1 in A and y1 in B by A1,RELSET_1:2; x = x1 by A25,XTUPLE_0:1; then not x9 in {0_(n,L)} by A26,XBOOLE_0:def 5; then x9 <> 0_(n,L) by TARSKI:def 1; then reconsider x9 as non-zero Polynomial of n,L by POLYNOM7:def 1; x9 reduces_to x9,P,T by A24,Def13; then ex p being Polynomial of n,L st p in P & x9 reduces_to x9,p,T; then x9 < x9,T by Th43; then Support x9 <> Support x9; hence contradiction; end; hence not [x,x] in R; end; then R is_irreflexive_in field R by RELAT_2:def 2; then R is irreflexive by RELAT_2:def 10; hence thesis by A22; end; end; theorem Th45: :: lemma 5.24 (i), p. 200 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable left_zeroed right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,h being Polynomial of n,L holds f in P implies PolyRedRel(P,T) reduces h*'f,0_(n,L) proof let n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed left_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f9,h9 be Polynomial of n,L; assume A1: f9 in P; per cases; suppose h9 = 0_(n,L); then h9*'f9 = 0_(n,L) by Th5; hence thesis by REWRITE1:12; end; suppose h9 <> 0_(n,L); then reconsider h = h9 as non-zero Polynomial of n,L by POLYNOM7:def 1; set H = { g where g is Polynomial of n,L : not(PolyRedRel(P,T) reduces g*' f9,0_(n,L)) }; now per cases; case f9 = 0_(n,L); then h9*'f9 = 0_(n,L) by POLYNOM1:28; hence thesis by REWRITE1:12; end; case f9 <> 0_(n,L); then reconsider f = f9 as non-zero Polynomial of n,L by POLYNOM7:def 1; A2: now let u be object; assume u in H; then ex g9 being Polynomial of n,L st u = g9 & not PolyRedRel (P,T) reduces g9*'f,0_(n,L); hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11; end; assume not PolyRedRel(P,T) reduces h9*'f9,0_(n,L); then h in H; then reconsider H as non empty Subset of Polynom-Ring(n,L) by A2, TARSKI:def 3; now assume H <> {}; reconsider H as non empty set; consider m being Polynomial of n,L such that A3: m in H and A4: for m9 being Polynomial of n,L st m9 in H holds m <= m9,T by Th31; m <> 0_(n,L) proof assume m = 0_(n,L); then A5: m*'f = 0_(n,L) by Th5; ex g9 being Polynomial of n,L st m = g9 & not PolyRedRel (P,T) reduces g9*'f,0_(n,L) by A3; hence contradiction by A5,REWRITE1:12; end; then reconsider m as non-zero Polynomial of n,L by POLYNOM7:def 1; Red(m,T) < m,T by Th35; then not m <= Red(m,T),T by Th29; then not Red(m,T) in H by A4; then A6: PolyRedRel(P,T) reduces Red(m,T)*'f,0_(n,L); set g = (m*'f) - ((m*'f).(HT(m*'f,T)))/HC(f,T) * (HT(m,T) *' f); A7: m*'f <> 0_(n,L) by POLYNOM7:def 1; A8: HC(f,T) <> 0.L; m*'f <> 0_(n,L) by POLYNOM7:def 1; then Support(m*'f) <> {} by POLYNOM7:1; then A9: HT(m*'f,T) in Support(m*'f) by TERMORD:def 6; (m*'f).(HT(m*'f,T))/HC(f,T) * (HT(m,T) *' f) = HC(m*'f,T)/HC(f, T) * (HT(m,T) *' f) by TERMORD:def 7 .= (HC(m,T) * HC(f,T))/HC(f,T) * (HT(m,T) *' f) by TERMORD:32 .= (HC(m,T) * HC(f,T))*(HC(f,T)") * (HT(m,T) *' f) .= HC(m,T) * (HC(f,T)*(HC(f,T)")) * (HT(m,T) *' f) by GROUP_1:def 3 .= (HC(m,T) * 1.L) * (HT(m,T) *' f) by A8,VECTSP_1:def 10 .= HC(m,T) * (HT(m,T) *' f) .= Monom(HC(m,T),HT(m,T)) *' f by Th22 .= HM(m,T) *'f by TERMORD:def 8; then A10: g = m *' f + -(HM(m,T) *' f) by POLYNOM1:def 7 .= f *' m + (f *' -HM(m,T) ) by Th6 .= (m + -HM(m,T)) *' f by POLYNOM1:26 .= (m - HM(m,T)) *' f by POLYNOM1:def 7 .= Red(m,T) *' f by TERMORD:def 9; HT(m*'f,T) = HT(m,T) + HT(f,T) & f <> 0_(n,L) by POLYNOM7:def 1 ,TERMORD:31; then m*'f reduces_to g,f,HT(m*'f,T),T by A9,A7; then m*'f reduces_to Red(m,T)*'f,f,T by A10; then m*'f reduces_to Red(m,T)*'f,P,T by A1; then [m*'f,Red(m,T)*'f] in PolyRedRel(P,T) by Def13; then A11: PolyRedRel(P,T) reduces m*'f,Red(m,T)*'f by REWRITE1:15; ex u being Polynomial of n,L st m = u & not PolyRedRel(P,T) reduces u*'f,0_(n,L) by A3; hence contradiction by A11,A6,REWRITE1:16; end; hence thesis; end; end; hence thesis; end; end; theorem Th46: :: lemma 5.24 (ii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to g,P,T implies m*'f reduces_to m*'g,P,T proof let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L, m be non-zero Monomial of n,L; assume f reduces_to g,P,T; then consider p being Polynomial of n,L such that A1: p in P and A2: f reduces_to g,p,T; consider b being bag of n such that A3: f reduces_to g,p,b,T by A2; set b9 = b + HT(m,T); A4: b in Support f by A3; A5: now m <> 0_(n,L) by POLYNOM7:def 1; then Support m <> {} by POLYNOM7:1; then A6: m.term(m) <> 0.L by POLYNOM7:def 5; assume A7: (m*'f).b9 = 0.L; (m*'f).b9 = (m*'f).(term(m)+b) by TERMORD:23 .= m.term(m) * f.b by Th7; then f.b = 0.L by A7,A6,VECTSP_2:def 1; hence contradiction by A4,POLYNOM1:def 4; end; b9 is Element of Bags n by PRE_POLY:def 12; then A8: b9 in Support(m*'f) by A5,POLYNOM1:def 4; A9: p <> 0_(n,L) by A2,Lm18; consider s being bag of n such that A10: s + HT(p,T) = b and A11: g = f - (f.b/HC(p,T)) * (s *' p) by A3; reconsider p as non-zero Polynomial of n,L by A9,POLYNOM7:def 1; A12: (s + HT(m,T)) + HT(p,T) = b9 by A10,PRE_POLY:35; set t = s + HT(m,T); set h = (m*'f) - ((m*'f).b9/HC(p,T)) * (t *' p); f <> 0_(n,L) by A3; then reconsider f as non-zero Polynomial of n,L by POLYNOM7:def 1; m*'f <> 0_(n,L) & p <> 0_(n,L) by POLYNOM7:def 1; then (m*'f) reduces_to h,p,b9,T by A8,A12; then A13: (m*'f) reduces_to h,p,T; A14: m.term(m) * (f.b/HC(p,T)) = m.term(m) * (f.b * (HC(p,T)")) .= (m.term(m) * f.b) * (HC(p,T)") by GROUP_1:def 3 .= (m.term(m) * f.b)/HC(p,T); (m*'f).b9 = (m*'f).(term(m)+b) by TERMORD:23 .= m.term(m) * f.b by Th7; then h = (m*'f) - (m.term(m) * (f.b/HC(p,T))) * (HT(m,T) *'(s *' p)) by A14 ,Th18 .= (m*'f) - (f.b/HC(p,T)) * (m.term(m) * (HT(m,T) *'(s *' p))) by Th11 .= (m*'f) - (f.b/HC(p,T)) * (Monom(m.(term(m)),HT(m,T)) *'(s *' p)) by Th22 .= (m*'f) - (f.b/HC(p,T)) * (Monom(coefficient(m),term(m)) *'(s *' p)) by TERMORD:23 .= (m*'f) - (f.b/HC(p,T) * (m *'(s *' p))) by POLYNOM7:11 .= (m*'f) - (m *' (f.b/HC(p,T) * (s *' p))) by Th12 .= (m*'f) + -(m *' (f.b/HC(p,T) * (s *' p))) by POLYNOM1:def 7 .= (m*'f) + (m *' -(f.b/HC(p,T) * (s *' p))) by Th6 .= m *' (f + -(f.b/HC(p,T)) * (s *' p)) by POLYNOM1:26 .= m *' (f - (f.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7; hence thesis by A1,A11,A13; end; theorem Th47: :: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,g implies PolyRedRel(P,T) reduces m*'f,m*'g proof let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L, m be Monomial of n,L; assume A1: PolyRedRel(P,T) reduces f,g; set R = PolyRedRel(P,T); per cases; suppose A2: m = 0_(n,L); then m*'f = 0_(n,L) by Th5 .= m*'g by A2,Th5; hence thesis by REWRITE1:12; end; suppose m <> 0_(n,L); then reconsider m as non-zero Monomial of n,L by POLYNOM7:def 1; defpred P[Nat] means for f,g being Polynomial of n,L st PolyRedRel(P,T) reduces f,g for p being RedSequence of R st p.1 = f & p.len p = g & len p = \$1 holds PolyRedRel(P,T) reduces m*'f,m*'g; consider p being RedSequence of R such that A3: p.1 = f & p.len p = g by A1,REWRITE1:def 3; consider k being Nat such that A4: len p = k; A5: now let k be Nat; assume A6: 1 <= k; thus P[k] implies P[k+1] proof assume A7: P[k]; now let f,g be Polynomial of n,L; assume PolyRedRel(P,T) reduces f,g; let p be RedSequence of R; assume that A8: p.1 = f and A9: p.len p = g and A10: len p = k+1; A11: dom p = Seg(k+1) by A10,FINSEQ_1:def 3; then A12: k+1 in dom p by FINSEQ_1:4; set q = p|(Seg k); reconsider q as FinSequence by FINSEQ_1:15; A13: k <= k+1 by NAT_1:11; then A14: dom q = Seg k by A10,FINSEQ_1:17; then A15: k in dom q by A6,FINSEQ_1:1; set h = q.len q; A16: len q = k by A10,A13,FINSEQ_1:17; k in dom p by A6,A11,A13,FINSEQ_1:1; then [p.k,p.(k+1)] in R by A12,REWRITE1:def 2; then A17: [h,g] in R by A9,A10,A16,A15,FUNCT_1:47; then consider h9,g9 being object such that A18: [h,g] = [h9,g9] and A19: h9 in NonZero Polynom-Ring(n,L) and g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; A20: h = h9 by A18,XTUPLE_0:1; A21: now let i be Nat; assume that A22: i in dom q and A23: i+1 in dom q; i+1 <= k by A14,A23,FINSEQ_1:1; then A24: i+1 <= k+1 by A13,XXREAL_0:2; i <= k by A14,A22,FINSEQ_1:1; then A25: i <= k+1 by A13,XXREAL_0:2; 1 <= i+1 by A14,A23,FINSEQ_1:1; then A26: i+1 in dom p by A11,A24,FINSEQ_1:1; 1 <= i by A14,A22,FINSEQ_1:1; then i in dom p by A11,A25,FINSEQ_1:1; then A27: [p.i, p.(i+1)] in R by A26,REWRITE1:def 2; p.i = q.i by A22,FUNCT_1:47; hence [q.i, q.(i+1)] in R by A23,A27,FUNCT_1:47; end; 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; then not h9 in {0_(n,L)} by A19,XBOOLE_0:def 5; then h9 <> 0_(n,L) by TARSKI:def 1; then reconsider h as non-zero Polynomial of n,L by A19,A20, POLYNOM1:def 11,POLYNOM7:def 1; h reduces_to g,P,T by A17,Def13; then m*'h reduces_to m*'g,P,T by Th46; then [m*'h,m*'g] in PolyRedRel(P,T) by Def13; then A28: PolyRedRel(P,T) reduces m*'h,m*'g by REWRITE1:15; reconsider q as RedSequence of R by A6,A16,A21,REWRITE1:def 2; 1 in dom q by A6,A14,FINSEQ_1:1; then A29: q.1 = f by A8,FUNCT_1:47; then PolyRedRel(P,T) reduces f,h by REWRITE1:def 3; then PolyRedRel(P,T) reduces m*'f,m*'h by A7,A10,A13,A29,FINSEQ_1:17; hence PolyRedRel(P,T) reduces m*'f,m*'g by A28,REWRITE1:16; end; hence thesis; end; end; A30: P[1] by REWRITE1:12; A31: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A30,A5); 1 <= k by A4,NAT_1:14; hence thesis by A1,A31,A3,A4; end; end; theorem :: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,0_(n ,L) implies PolyRedRel(P,T) reduces m*'f,0_(n,L) proof let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L), f be Polynomial of n,L, m be Monomial of n,L; assume PolyRedRel(P,T) reduces f,0_(n,L); then PolyRedRel(P,T) reduces m*'f,m*'0_(n,L) by Th47; hence thesis by POLYNOM1:28; end; theorem Th49: :: lemma 5.25 (i), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies ex f1,g1 being Polynomial of n,L st f1 - g1 = h1 & PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P ,T) reduces g,g1 proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g,h,h1 be Polynomial of n,L; assume that A1: f - g = h and A2: PolyRedRel(P,T) reduces h,h1; consider p being RedSequence of PolyRedRel(P,T) such that A3: p.1 = h & p.len p = h1 by A2,REWRITE1:def 3; defpred P[Nat] means for f,g,h being Polynomial of n,L st f - g = h for h1 being Polynomial of n,L for p being RedSequence of PolyRedRel(P,T) st p.1 = h & p.len p = h1 & len p = \$1 holds ex f1,g1 being Polynomial of n,L st f1 - g1 = h1 & PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P,T) reduces g,g1; A4: now let k be Nat; assume A5: 1 <= k; assume A6: P[k]; thus P[k+1] proof let f,g,h be Polynomial of n,L; assume A7: f - g = h; let h1 be Polynomial of n,L; let r be RedSequence of PolyRedRel(P,T); assume that A8: r.1 = h and A9: r.len r = h1 and A10: len r = k+1; set h2 = r.k; A11: dom r = Seg(k+1) by A10,FINSEQ_1:def 3; 1 <= k + 1 by NAT_1:11; then A12: k + 1 in dom r by A11,FINSEQ_1:1; k <= k+1 by NAT_1:11; then k in dom r by A5,A11,FINSEQ_1:1; then A13: [r.k,r.(k+1)] in PolyRedRel(P,T) by A12,REWRITE1:def 2; then consider x,y being object such that A14: x in NonZero Polynom-Ring(n,L) and y in the carrier of Polynom-Ring(n,L) and A15: [r.k,r.(k+1)] = [x,y] by ZFMISC_1:def 2; A16: r.k = x by A15,XTUPLE_0:1; then reconsider h2 as Polynomial of n,L by A14,POLYNOM1:def 11; 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; then not r.k in {0_(n,L)} by A14,A16,XBOOLE_0:def 5; then r.k <> 0_(n,L) by TARSKI:def 1; then reconsider h2 as non-zero Polynomial of n,L by POLYNOM7:def 1; h2 reduces_to h1,P,T by A9,A10,A13,Def13; then consider p being Polynomial of n,L such that A17: p in P and A18: h2 reduces_to h1,p,T; consider b being bag of n such that A19: h2 reduces_to h1,p,b,T by A18; set q = r|(Seg k); reconsider q as FinSequence by FINSEQ_1:15; A20: k <= k+1 by NAT_1:11; then A21: dom q = Seg k by A10,FINSEQ_1:17; A22: dom r = Seg(k+1) by A10,FINSEQ_1:def 3; A23: now let i be Nat; assume that A24: i in dom q and A25: i+1 in dom q; i+1 <= k by A21,A25,FINSEQ_1:1; then A26: i+1 <= k+1 by A20,XXREAL_0:2; i <= k by A21,A24,FINSEQ_1:1; then A27: i <= k+1 by A20,XXREAL_0:2; 1 <= i+1 by A21,A25,FINSEQ_1:1; then A28: i+1 in dom r by A22,A26,FINSEQ_1:1; 1 <= i by A21,A24,FINSEQ_1:1; then i in dom r by A22,A27,FINSEQ_1:1; then A29: [r.i, r.(i+1)] in PolyRedRel(P,T) by A28,REWRITE1:def 2; r.i = q.i by A24,FUNCT_1:47; hence [q.i, q.(i+1)] in PolyRedRel(P,T) by A25,A29,FUNCT_1:47; end; len q = k by A10,A20,FINSEQ_1:17; then reconsider q as RedSequence of PolyRedRel(P,T) by A5,A23, REWRITE1:def 2; A30: k in dom q by A5,A21,FINSEQ_1:1; 1 in dom q by A5,A21,FINSEQ_1:1; then A31: q.1 = h by A8,FUNCT_1:47; q.(len q) = q.k by A10,A20,FINSEQ_1:17 .= h2 by A30,FUNCT_1:47; then consider f2,g2 being Polynomial of n,L such that A32: f2 - g2 = h2 and A33: PolyRedRel(P,T) reduces f,f2 and A34: PolyRedRel(P,T) reduces g,g2 by A6,A7,A10,A20,A31,FINSEQ_1:17; consider s being bag of n such that A35: s + HT(p,T) = b and A36: h1 = h2 - (h2.b/HC(p,T)) * (s *' p) by A19; set f1 = f2 - (f2.b/HC(p,T)) * (s *' p), g1 = g2 - (g2.b/HC(p,T)) * (s *' p); A37: (f2.b/HC(p,T)) + -g2.b/HC(p,T) = (f2.b * (HC(p,T))") + -g2.b/HC(p,T) .= (f2.b * (HC(p,T))") + -(g2.b * (HC(p,T)")) .= (f2.b * (HC(p,T))") + ((-g2.b) * (HC(p,T)")) by VECTSP_1:9 .= (f2.b + (-g2.b)) * (HC(p,T)") by VECTSP_1:def 7 .= (f2.b + (-g2).b) * (HC(p,T)") by POLYNOM1:17 .= (f2 + (-g2)).b * (HC(p,T)") by POLYNOM1:15 .= (f2-g2).b * (HC(p,T)") by POLYNOM1:def 7 .= (f2-g2).b / HC(p,T); A38: now per cases; case A39: not b in Support g2; b is Element of Bags n by PRE_POLY:def 12; then g2.b = 0.L by A39,POLYNOM1:def 4; then g1 = g2 - (0.L*(HC(p,T)")) * (s *' p) .= g2 - (0.L * (s *' p)) .= g2 - 0_(n,L) by Th8 .= g2 by Th4; hence PolyRedRel(P,T) reduces g,g1 by A34; end; case A40: b in Support g2; then g2 <> 0_(n,L) by POLYNOM7:1; then reconsider g2 as non-zero Polynomial of n,L by POLYNOM7:def 1; g2 <> 0_(n,L) & p <> 0_(n,L) by A18,Lm18,POLYNOM7:def 1; then g2 reduces_to g1,p,b,T by A35,A40; then g2 reduces_to g1,p,T; then g2 reduces_to g1,P,T by A17; then [g2,g1] in PolyRedRel(P,T) by Def13; then PolyRedRel(P,T) reduces g2,g1 by REWRITE1:15; hence PolyRedRel(P,T) reduces g,g1 by A34,REWRITE1:16; end; end; A41: now per cases; case A42: not b in Support f2; b is Element of Bags n by PRE_POLY:def 12; then f2.b = 0.L by A42,POLYNOM1:def 4; then f1 = f2 - (0.L*(HC(p,T)")) * (s *' p) .= f2 - (0.L * (s *' p)) .= f2 - 0_(n,L) by Th8 .= f2 by Th4; hence PolyRedRel(P,T) reduces f,f1 by A33; end; case A43: b in Support f2; then f2 <> 0_(n,L) by POLYNOM7:1; then reconsider f2 as non-zero Polynomial of n,L by POLYNOM7:def 1; f2 <> 0_(n,L) & p <> 0_(n,L) by A18,Lm18,POLYNOM7:def 1; then f2 reduces_to f1,p,b,T by A35,A43; then f2 reduces_to f1,p,T; then f2 reduces_to f1,P,T by A17; then [f2,f1] in PolyRedRel(P,T) by Def13; then PolyRedRel(P,T) reduces f2,f1 by REWRITE1:15; hence PolyRedRel(P,T) reduces f,f1 by A33,REWRITE1:16; end; end; A44: --((g2.b/HC(p,T)) * (s *' p)) = (g2.b/HC(p,T)) * (s *' p) by POLYNOM1:19 ; A45: ((-(f2.b/HC(p,T))) * (s *' p) + (g2.b/HC(p,T)) * (s *' p)) = ((-(f2.b/HC(p,T))) + (g2.b/HC(p,T))) * (s *' p) by Th10 .= - -(-(f2.b/HC(p,T)) + g2.b/HC(p,T)) * (s *' p) by POLYNOM1:19; f1 - g1 = (f2 - (f2.b/HC(p,T)) * (s *' p)) + -(g2 - (g2.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7 .= (f2 + -(f2.b/HC(p,T)) * (s *' p)) + -(g2 - (g2.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7 .= (f2 + -(f2.b/HC(p,T)) * (s *' p)) + -(g2 + -((g2.b/HC(p,T)) * (s *' p))) by POLYNOM1:def 7 .= (f2 + -(f2.b/HC(p,T)) * (s *' p)) + (-g2 + --((g2.b/HC(p,T)) * (s *' p))) by Th1 .= ((f2 + -(f2.b/HC(p,T)) * (s *' p)) + -g2) + (g2.b/HC(p,T)) * (s *' p) by A44,POLYNOM1:21 .= (-(f2.b/HC(p,T)) * (s *' p) + (f2 + -g2)) + (g2.b/HC(p,T)) * (s *' p) by POLYNOM1:21 .= (f2 + -g2) + (-(f2.b/HC(p,T)) * (s *' p) + (g2.b/HC(p,T)) * (s *' p)) by POLYNOM1:21 .= (f2 - g2) + ((-(f2.b/HC(p,T)) * (s *' p)) + (g2.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7 .= (f2 - g2) + ((-(f2.b/HC(p,T))) * (s *' p) + (g2.b/HC(p,T)) * (s *' p)) by Th9 .= (f2 - g2) + -(-(-(f2.b/HC(p,T)) + g2.b/HC(p,T))) * (s *' p) by A45,Th9 .= (f2 - g2) - (-(-(f2.b/HC(p,T)) + g2.b/HC(p,T))) * (s *' p) by POLYNOM1:def 7 .= (f2 - g2) - (-(-(f2.b/HC(p,T))) + -g2.b/HC(p,T)) * (s *' p) by RLVECT_1:31 .= h1 by A32,A36,A37,RLVECT_1:17; hence thesis by A41,A38; end; end; A46: P[1] proof let f,g,h be Polynomial of n,L; assume A47: f - g = h; let h1 be Polynomial of n,L; let p being RedSequence of PolyRedRel(P,T); assume A48: p.1 = h & p.len p = h1 & len p = 1; take f,g; thus thesis by A47,A48,REWRITE1:12; end; A49: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A46,A4); consider k being Nat such that A50: len p = k; 1 <= k by A50,NAT_1:14; hence thesis by A1,A49,A3,A50; end; theorem Th50: :: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convergent_wrt PolyRedRel(P,T) proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L; assume PolyRedRel(P,T) reduces f-g,0_(n,L); then consider f1,g1 being Polynomial of n,L such that A1: f1 - g1 = 0_(n,L) and A2: PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P,T) reduces g,g1 by Th49; g1 = (f1 - g1) + g1 by A1,Th2 .= (f1 + -g1) + g1 by POLYNOM1:def 7 .= f1 + (-g1 + g1) by POLYNOM1:21 .= f1 + 0_(n,L) by Th3 .= f1 by POLYNOM1:23; hence thesis by A2,REWRITE1:def 7; end; theorem Th51: :: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convertible_wrt PolyRedRel(P,T) proof let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L; set R = PolyRedRel(P,T); assume PolyRedRel(P,T) reduces f-g,0_(n,L); then f,g are_convergent_wrt R by Th50; then consider h being object such that A1: R reduces f,h and A2: R reduces g,h by REWRITE1:def 7; R~ reduces h,g by A2,REWRITE1:24; then A3: R \/ R~ reduces h,g by REWRITE1:22,XBOOLE_1:7; R \/ R~ reduces f,h by A1,REWRITE1:22,XBOOLE_1:7; then R \/ R~ reduces f,g by A3,REWRITE1:16; hence thesis by REWRITE1:def 4; end; definition let R be non empty addLoopStr, I be Subset of R, a,b be Element of R; pred a,b are_congruent_mod I means a - b in I; end; theorem for R being add-associative left_zeroed right_zeroed right_complementable right-distributive non empty doubleLoopStr, I being right-ideal non empty Subset of R, a being Element of R holds a,a are_congruent_mod I proof let R be add-associative left_zeroed right_zeroed right_complementable right-distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a be Element of R; a - a = 0.R & 0.R in I by IDEAL_1:3,RLVECT_1:15; hence thesis; end; theorem Th53: for R being add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, I being right-ideal non empty Subset of R, a,b being Element of R holds a,b are_congruent_mod I implies b,a are_congruent_mod I proof let R be add-associative right_zeroed right_complementable right-distributive well-unital non empty doubleLoopStr, I be right-ideal non empty Subset of R, a,b be Element of R; assume a,b are_congruent_mod I; then a - b in I; then A1: -(a - b) in I by IDEAL_1:14; b - a - (-(a - b)) = b - a + -(-(a - b)) .= b - a + (a - b) by RLVECT_1:17 .= b + -a + (a - b) .= b + (-a + (a - b)) by RLVECT_1:def 3 .= b + (-a + (a + -b)) .= b + ((-a + a) + -b) by RLVECT_1:def 3 .= b + (0.R + -b) by RLVECT_1:5 .= b + -b by ALGSTR_1:def 2 .= 0.R by RLVECT_1:5; then b - a = -(a - b) by RLVECT_1:21; hence thesis by A1; end; theorem Th54: for R being add-associative right_zeroed right_complementable non empty addLoopStr, I being add-closed non empty Subset of R, a,b,c being Element of R holds a,b are_congruent_mod I & b,c are_congruent_mod I implies a, c are_congruent_mod I proof let R be add-associative right_zeroed right_complementable non empty addLoopStr, I be add-closed non empty Subset of R, a,b,c be Element of R; assume a,b are_congruent_mod I & b,c are_congruent_mod I; then a - b in I & b - c in I; then A1: a - b + (b - c) in I by IDEAL_1:def 1; a - b + (b - c) = a + -b + (b - c) .= a + (-b + (b - c)) by RLVECT_1:def 3 .= a + (-b + (b + -c)) .= a + ((-b + b) + -c) by RLVECT_1:def 3 .= a + (0.R + -c) by RLVECT_1:5 .= a + -c by ALGSTR_1:def 2 .= a - c; hence thesis by A1; end; theorem for R being Abelian add-associative right_zeroed right_complementable well-unital distributive associative non trivial doubleLoopStr, I being add-closed non empty Subset of R, a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a+c,b+d are_congruent_mod I proof let R be Abelian add-associative right_zeroed right_complementable well-unital distributive associative non trivial doubleLoopStr, I be add-closed non empty Subset of R, a,b,c,d be Element of R; assume a,b are_congruent_mod I & c,d are_congruent_mod I; then a - b in I & c - d in I; then A1: (a - b) + (c - d) in I by IDEAL_1:def 1; (a + c) - (b + d) = (a + c) + (-(b + d)) .= (a + c) + (-d + -b) by RLVECT_1:31 .= a + (c + (-d + -b)) by RLVECT_1:def 3 .= a + ((c + -d) + -b) by RLVECT_1:def 3 .= (a + -b) + (c + -d) by RLVECT_1:def 3 .= (a - b) + (c + -d) .= (a - b) + (c - d); hence thesis by A1; end; theorem for R being add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr, I being add-closed right-ideal non empty Subset of R, a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a*c,b*d are_congruent_mod I proof let R be add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, a,b,c,d be Element of R; assume that A1: a,b are_congruent_mod I and A2: c,d are_congruent_mod I; c - d in I by A2; then A3: (c - d) * b in I by IDEAL_1:def 3; A4: (c - d) * b = (c + -d) * b .= c * b + (-d) * b by VECTSP_1:def 3; (a - b) * c = (a + -b) * c .= a * c + (-b) * c by VECTSP_1:def 3; then A5: ((a - b) * c) + ((c - d) * b) = a * c + ((-b) * c + (c * b + (-d) * b)) by A4,RLVECT_1:def 3 .= a * c + (((-b) * c + c * b) + (-d) * b) by RLVECT_1:def 3 .= a * c + ((-(b * c) + c * b) + (-d) * b) by VECTSP_1:9 .= a * c + (0.R + (-d) * b) by RLVECT_1:5 .= a * c + (-d) * b by ALGSTR_1:def 2 .= a * c + -(d * b) by VECTSP_1:9 .= a * c - b * d; a - b in I by A1; then (a - b) * c in I by IDEAL_1:def 3; then ((a - b) * c) + ((c - d) * b) in I by A3,IDEAL_1:def 1; hence thesis by A5; end; Lm19: for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being non-zero Polynomial of n,L, g being Polynomial of n,L, f9,g9 being Element of Polynom-Ring(n,L) st f = f9 & g = g9 holds f reduces_to g,P,T implies f9,g9 are_congruent_mod P-Ideal proof let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f be non-zero Polynomial of n,L, g be Polynomial of n,L, f9,g9 be Element of Polynom-Ring(n,L); assume that A1: f = f9 and A2: g = g9; set R = Polynom-Ring(n,L); reconsider x = -g as Element of R by POLYNOM1:def 11; reconsider x as Element of R; x + g9 = -g + g by A2,POLYNOM1:def 11 .= 0_(n,L) by Th3 .= 0.R by POLYNOM1:def 11; then A3: -g9 = -g by RLVECT_1:6; assume f reduces_to g,P,T; then consider p being Polynomial of n,L such that A4: p in P and A5: f reduces_to g,p,T; consider b being bag of n such that A6: f reduces_to g,p,b,T by A5; consider s being bag of n such that s + HT(p,T) = b and A7: g = f - (f.b/HC(p,T)) * (s *' p) by A6; reconsider P as non empty Subset of Polynom-Ring(n,L) by A4; set q = (f.b/HC(p,T)) * (s *' p), q9 = Monom((f.b/HC(p,T)),s) *' p; set r = <* q9 *>; now let u be object; A8: rng r = {q9} by FINSEQ_1:39; assume u in rng r; then u = q9 by A8,TARSKI:def 1; hence u in the carrier of R by POLYNOM1:def 11; end; then rng r c= the carrier of R by TARSKI:def 3; then reconsider r as FinSequence of the carrier of R by FINSEQ_1:def 4; now reconsider p9 = p as Element of R by POLYNOM1:def 11; reconsider m = Monom((f.b/HC(p,T)),s) as Element of R by POLYNOM1:def 11; let i be set; assume A9: i in dom r; reconsider p9 as Element of R; reconsider m as Element of R; A10: m * p9 * 1.R = m * p9 .= q9 by POLYNOM1:def 11; dom r = Seg 1 by FINSEQ_1:38; then i = 1 by A9,FINSEQ_1:2,TARSKI:def 1; then r.i = q9 by FINSEQ_1:40; hence ex u,v being Element of R, a being Element of P st r/.i = u*a*v by A4,A9 ,A10,PARTFUN1:def 6; end; then reconsider r as LinearCombination of P by IDEAL_1:def 8; q9 is Element of R by POLYNOM1:def 11; then A11: Sum r = q9 by BINOM:3; q9 = q by Th22; then A12: q in P-Ideal by A11,IDEAL_1:60; A13: f - g = f + (-g) by POLYNOM1:def 7 .= f9 + (-g9) by A1,A3,POLYNOM1:def 11 .= f9 - g9; A14: --((f.b/HC(p,T)) * (s *' p)) = (f.b/HC(p,T)) * (s *' p) by POLYNOM1:19; f - g = f + -(f - (f.b/HC(p,T)) * (s *' p)) by A7,POLYNOM1:def 7 .= f + -(f + -(f.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7 .= f + (-f + -(-(f.b/HC(p,T)) * (s *' p))) by Th1 .= (f + -f) + (f.b/HC(p,T)) * (s *' p) by A14,POLYNOM1:21 .= 0_(n,L) + (f.b/HC(p,T)) * (s *' p) by Th3 .= (f.b/HC(p,T)) * (s *' p) by Th2; hence thesis by A12,A13; end; theorem Th57: :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_convertible_wrt PolyRedRel(P,T) implies f,g are_congruent_mod P-Ideal proof let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Element of Polynom-Ring(n,L); set R = PolyRedRel(P,T), PR = Polynom-Ring(n,L); defpred P[Nat] means for f,g being Element of Polynom-Ring(n,L) st R \/ R~ reduces f,g for p being RedSequence of R \/ R~ st p.1 = f & p.len p = g & len p = \$1 holds f,g are_congruent_mod P-Ideal; assume f,g are_convertible_wrt PolyRedRel(P,T); then A1: R \/ R~ reduces f,g by REWRITE1:def 4; then consider p being RedSequence of R \/ R~ such that A2: p.1 = f & p.len p = g by REWRITE1:def 3; A3: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11; A4: now let k be Nat; assume A5: 1 <= k; thus P[k] implies P[k+1] proof assume A6: P[k]; now let f,g be Element of Polynom-Ring(n,L); assume R \/ R~ reduces f,g; let p be RedSequence of R \/ R~; assume that A7: p.1 = f and A8: p.len p = g and A9: len p = k+1; A10: dom p = Seg(k+1) by A9,FINSEQ_1:def 3; then A11: k+1 in dom p by FINSEQ_1:4; set q = p|(Seg k); reconsider q as FinSequence by FINSEQ_1:15; A12: k <= k+1 by NAT_1:11; then A13: dom q = Seg k by A9,FINSEQ_1:17; then A14: k in dom q by A5,FINSEQ_1:1; set h = q.len q; A15: len q = k by A9,A12,FINSEQ_1:17; k in dom p by A5,A10,A12,FINSEQ_1:1; then [p.k,p.(k+1)] in R \/ R~ by A11,REWRITE1:def 2; then [h,g] in R \/ R~ by A8,A9,A15,A14,FUNCT_1:47; then A16: [h,g] in R or [h,g] in R~ by XBOOLE_0:def 3; A17: now per cases by A16,RELAT_1:def 7; case [h,g] in R; then consider h9,g9 being object such that A18: [h,g] = [h9,g9] and A19: h9 in NonZero Polynom-Ring(n,L) and g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; h = h9 by A18,XTUPLE_0:1; hence h in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} & h in ( the carrier of Polynom-Ring(n,L)) & g in (the carrier of Polynom-Ring(n,L)) by A19,POLYNOM1:def 11; end; case [g,h] in R; then consider h9,g9 being object such that A20: [g,h] = [h9,g9] and A21: h9 in NonZero Polynom-Ring(n,L) & g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; A22: h = g9 by A20,XTUPLE_0:1; g = h9 by A20,XTUPLE_0:1; hence g in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} & g in ( the carrier of Polynom-Ring(n,L)) & h in (the carrier of Polynom-Ring(n,L)) by A21,A22,POLYNOM1:def 11; end; end; now let i be Nat; assume that A23: i in dom q and A24: i+1 in dom q; i+1 <= k by A13,A24,FINSEQ_1:1; then A25: i+1 <= k+1 by A12,XXREAL_0:2; i <= k by A13,A23,FINSEQ_1:1; then A26: i <= k+1 by A12,XXREAL_0:2; 1 <= i+1 by A13,A24,FINSEQ_1:1; then A27: i+1 in dom p by A10,A25,FINSEQ_1:1; 1 <= i by A13,A23,FINSEQ_1:1; then i in dom p by A10,A26,FINSEQ_1:1; then A28: [p.i, p.(i+1)] in R \/ R~ by A27,REWRITE1:def 2; p.i = q.i by A23,FUNCT_1:47; hence [q.i, q.(i+1)] in R \/ R~ by A24,A28,FUNCT_1:47; end; then reconsider q as RedSequence of R \/ R~ by A5,A15,REWRITE1:def 2; reconsider h as Polynomial of n,L by A17,POLYNOM1:def 11; reconsider h9 = h as Element of Polynom-Ring(n,L) by POLYNOM1:def 11; reconsider h9 as Element of Polynom-Ring(n,L); 1 in dom q by A5,A13,FINSEQ_1:1; then A29: q.1 = f by A7,FUNCT_1:47; then R \/ R~ reduces f,h by REWRITE1:def 3; then A30: f,h9 are_congruent_mod P-Ideal by A6,A9,A12,A29,FINSEQ_1:17; now per cases by A16,RELAT_1:def 7; case A31: [h,g] in R; then consider h9,g9 being object such that A32: [h,g] = [h9,g9] and A33: h9 in NonZero Polynom-Ring(n,L) and A34: g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; A35: h = h9 by A32,XTUPLE_0:1; not h9 in {0_(n,L)} by A3,A33,XBOOLE_0:def 5; then h9 <> 0_(n,L) by TARSKI:def 1; then reconsider h as non-zero Polynomial of n,L by A35, POLYNOM7:def 1; A36: g = g9 by A32,XTUPLE_0:1; reconsider g9 as Polynomial of n,L by A34,POLYNOM1:def 11; reconsider h9 = h as Element of Polynom-Ring(n,L) by POLYNOM1:def 11; reconsider h9 as Element of Polynom-Ring(n,L); h reduces_to g9,P,T by A31,A36,Def13; then h9,g are_congruent_mod P-Ideal by A36,Lm19; then f,g are_congruent_mod P-Ideal by A30,Th54; hence f-g in P-Ideal; end; case A37: [g,h] in R; then consider g9,h9 being object such that A38: [g,h] = [g9,h9] and A39: g9 in NonZero Polynom-Ring(n,L) and A40: h9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2; A41: g = g9 by A38,XTUPLE_0:1; not g9 in {0_(n,L)} by A3,A39,XBOOLE_0:def 5; then A42: g9 <> 0_(n,L) by TARSKI:def 1; A43: h = h9 by A38,XTUPLE_0:1; then reconsider h as Element of Polynom-Ring(n,L) by A40; reconsider h9 as Polynomial of n,L by A43; reconsider g9 = g as non-zero Polynomial of n,L by A41,A42, POLYNOM1:def 11,POLYNOM7:def 1; reconsider gg = g9 as Element of Polynom-Ring(n,L); reconsider gg as Element of Polynom-Ring(n,L); reconsider h as Element of Polynom-Ring(n,L); g9 reduces_to h9,P,T by A37,A43,Def13; then h,gg are_congruent_mod P-Ideal by A43,Lm19,Th53; then f,gg are_congruent_mod P-Ideal by A30,Th54; hence f-g in P-Ideal; end; end; hence f,g are_congruent_mod P-Ideal; end; hence thesis; end; end; A44: P[1] proof let f,g be Element of Polynom-Ring(n,L); assume R \/ R~ reduces f,g; let p be RedSequence of R \/ R~; assume p.1 = f & p.len p = g & len p = 1; then A45: f - g = 0.PR by RLVECT_1:15; 0.PR in P-Ideal by IDEAL_1:3; hence thesis by A45; end; A46: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A44,A4); consider k being Nat such that A47: len p = k; 1 <= k by A47,NAT_1:14; hence thesis by A46,A1,A2,A47; end; Lm20: for n being Nat, T being admissible connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,p,h being Element of Polynom-Ring(n,L) st p in P & p <> 0_(n,L) & h <> 0_(n,L) holds f,f+h*p are_convertible_wrt PolyRedRel(P,T) proof let n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of Polynom-Ring(n,L), f,p,h be Element of Polynom-Ring(n,L); assume that A1: p in P and A2: p <> 0_(n,L) and A3: h <> 0_(n,L); set PR = Polynom-Ring(n,L); reconsider f9 = f, h9 = h, p9 = p as Element of PR; reconsider f9,p9,h9 as Polynomial of n,L by POLYNOM1:def 11; reconsider h9,p9 as non-zero Polynomial of n,L by A2,A3,POLYNOM7:def 1; A4: PolyRedRel(P,T) reduces h9*'p9,0_(n,L) by A1,Th45; now per cases; case f9 = 0_(n,L); then PolyRedRel(P,T) reduces f9+h9*'p9,f9 by A4,Th2; then A5: f9,f9+h9*'p9 are_convertible_wrt PolyRedRel(P,T) by REWRITE1:25; h9 *' p9 = h * p by POLYNOM1:def 11; hence thesis by A5,POLYNOM1:def 11; end; case f9 <> 0_(n,L); then reconsider f9 as non-zero Polynomial of n,L by POLYNOM7:def 1; (f9 + h9*'p9) - f9 = (f9 + h9*'p9) + -f9 by POLYNOM1:def 7 .= h9*'p9 + (f9 + -f9) by POLYNOM1:21 .= 0_(n,L) + h9*'p9 by Th3 .= h9*'p9 by Th2; then A6: PolyRedRel(P,T) reduces (f9 + h9*'p9) - f9,0_(n,L) by A1,Th45; now per cases; case f9 + h9*'p9 <> 0_(n,L); then reconsider g9 = f9 + h9*'p9 as non-zero Polynomial of n,L by POLYNOM7:def 1; h9 *' p9 = h * p by POLYNOM1:def 11; then g9 = f + h * p by POLYNOM1:def 11; hence thesis by A6,Th51,REWRITE1:31; end; case A7: f9 + h9*'p9 = 0_(n,L); now assume A8: -(h9) = 0_(n,L); A9: now let u be object; assume u in dom h9; then reconsider u9 = u as bag of n; -(h9.u9) = (-h9).u9 by POLYNOM1:17 .= 0.L by A8,POLYNOM1:22; then h9.u9 = - 0.L by RLVECT_1:17 .= 0.L by RLVECT_1:12 .= (0_(n,L)).u9 by POLYNOM1:22; hence h9.u = (0_(n,L)).u; end; dom h9 = Bags n by FUNCT_2:def 1 .= dom 0_(n,L) by FUNCT_2:def 1; hence contradiction by A3,A9,FUNCT_1:2; end; then reconsider mh9 = -(h9) as non-zero Polynomial of n,L by POLYNOM7:def 1; reconsider x = mh9 as Element of PR by POLYNOM1:def 11; reconsider x as Element of PR; h + x = mh9 + h9 by POLYNOM1:def 11 .= 0_(n,L) by Th3 .= 0.PR by POLYNOM1:def 11; then -h = mh9 by RLVECT_1:6; then A10: (-h) * p = mh9 *' p9 by POLYNOM1:def 11; PolyRedRel(P,T) reduces mh9*'p9,0_(n,L) by A1,Th45; then A11: mh9*'p9,0_(n,L) are_convertible_wrt PolyRedRel(P,T) by REWRITE1:25; h9 *' p9 = h * p by POLYNOM1:def 11; then A12: f + h * p = 0_(n,L) by A7,POLYNOM1:def 11 .= 0.PR by POLYNOM1:def 11; then f = - h * p by RLVECT_1:6 .= (-h)*p by VECTSP_1:9; hence thesis by A12,A11,A10,POLYNOM1:def 11; end; end; hence thesis; end; end; hence thesis; end; theorem :: lemma 5.26, p. 202 for n being Nat, T being admissible connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_congruent_mod P-Ideal implies f,g are_convertible_wrt PolyRedRel(P,T) proof let n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of Polynom-Ring(n,L), f,g be Element of Polynom-Ring(n,L); set PR = Polynom-Ring(n,L); defpred P[Nat] means for f,g being Element of Polynom-Ring(n,L), p being LeftLinearCombination of P st Sum p = g - f & len p = \$1 holds f,g are_convertible_wrt PolyRedRel(P,T); now let k be Nat; assume A1: P[k]; now let f,g be Element of Polynom-Ring(n,L), p be LeftLinearCombination of P; assume that A2: Sum p = g - f and A3: len p = k + 1; now set h = f + p/.(k+1); set q = p|(Seg k); reconsider q as FinSequence by FINSEQ_1:15; dom p = Seg(k+1) by A3,FINSEQ_1:def 3; then consider u being Element of PR,a being Element of P such that A4: p/.(k+1) = u*a by FINSEQ_1:4,IDEAL_1:def 9; reconsider u9 = u, a9 = a as Element of PR; reconsider u9,a9 as Polynomial of n,L by POLYNOM1:def 11; A5: p/.(k+1) = u9 *' a9 by A4,POLYNOM1:def 11; k <= k+1 by NAT_1:11; then A6: len q = k by A3,FINSEQ_1:17; reconsider q as LeftLinearCombination of P by IDEAL_1:42; A7: Sum p = Sum q + p/.(k+1) by A3,Lm6; then Sum p - p/.(k+1) = (Sum q + p/.(k+1)) + -(p/.(k+1)) .= Sum q + (p/.(k+1) + -(p/.(k+1))) by RLVECT_1:def 3 .= Sum q + 0.PR by RLVECT_1:5 .= Sum q by RLVECT_1:4; then Sum q = (g - f) + -(p/.(k+1)) by A2 .= (g + -f) + -(p/.(k+1)) .= g + (-f + -(p/.(k+1))) by RLVECT_1:def 3 .= g + -h by RLVECT_1:31 .= g - h; then A8: h,g are_convertible_wrt PolyRedRel(P,T) by A1,A6; now per cases; case a <> 0_(n,L) & u <> 0_(n,L); then f,h are_convertible_wrt PolyRedRel(P,T) by A4,Lm20; hence f,g are_convertible_wrt PolyRedRel(P,T) by A8,REWRITE1:30; end; case A9: a = 0_(n,L) or u = 0_(n,L); reconsider sumq = Sum q as Polynomial of n,L by POLYNOM1:def 11; now per cases by A9; case a = 0_(n,L); hence p/.(k+1) = 0_(n,L) by A5,POLYNOM1:28; end; case u = 0_(n,L); hence p/.(k+1) = 0_(n,L) by A5,Th5; end; end; then Sum p = sumq + 0_(n,L) by A7,POLYNOM1:def 11 .= Sum q by POLYNOM1:23; hence f,g are_convertible_wrt PolyRedRel(P,T) by A1,A2,A6; end; end; hence f,g are_convertible_wrt PolyRedRel(P,T); end; hence f,g are_convertible_wrt PolyRedRel(P,T); end; hence P[k+1]; end; then A10: for k being Nat holds P[k] implies P[k+1]; A11: P[0] proof let f,g be Element of Polynom-Ring(n,L), p be LeftLinearCombination of P; assume that A12: Sum p = g - f and A13: len p = 0; p = <*>(the carrier of PR) by A13; then Sum p = 0.PR by RLVECT_1:43; then f = g by A12,RLVECT_1:21; hence thesis by REWRITE1:26; end; A14: for k being Nat holds P[k] from NAT_1:sch 2(A11,A10); assume f,g are_congruent_mod P-Ideal; then g,f are_congruent_mod P-Ideal by Th53; then g - f in P-Ideal; then g - f in P-LeftIdeal by IDEAL_1:63; then consider p being LeftLinearCombination of P such that A15: Sum p = g - f by IDEAL_1:61; ex k being Nat st len p = k; hence thesis by A14,A15; end; theorem Th59: :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f,g implies f-g in P-Ideal proof let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L; reconsider f9 = f, g9 = g as Element of Polynom-Ring(n,L) by POLYNOM1:def 11; reconsider f9,g9 as Element of Polynom-Ring(n,L); set R = Polynom-Ring(n,L); reconsider x = -g as Element of R by POLYNOM1:def 11; reconsider x as Element of R; x + g9 = -g + g by POLYNOM1:def 11 .= 0_(n,L) by Th3 .= 0.R by POLYNOM1:def 11; then A1: -g9 = -g by RLVECT_1:6; assume PolyRedRel(P,T) reduces f,g; then f,g are_convertible_wrt PolyRedRel(P,T) by REWRITE1:25; then A2: f9,g9 are_congruent_mod P-Ideal by Th57; f - g = f + (-g) by POLYNOM1:def 7 .= f9 + (-g9) by A1,POLYNOM1:def 11 .= f9 - g9; hence thesis by A2; end; theorem :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L holds PolyRedRel(P ,T) reduces f,0_(n,L) implies f in P-Ideal proof let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f be Polynomial of n,L; assume PolyRedRel(P,T) reduces f,0_(n,L); then f-0_(n,L) in P-Ideal by Th59; hence thesis by Th4; end;