:: 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;