:: Construction of {G}r\"obner bases. S-Polynomials and Standard
:: Representations
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, SUBSET_1,
RELAT_1, XXREAL_0, FUNCT_1, SUPINF_2, CARD_3, ARYTM_3, TARSKI, ORDINAL4,
PARTFUN1, CARD_1, FUNCT_7, ARYTM_1, RFINSEQ, PRE_POLY, PBOOLE, RELAT_2,
BAGORDER, ORDERS_2, WAYBEL_4, ZFMISC_1, XCMPLX_0, ALGSTR_1, LATTICES,
POLYNOM7, POLYNOM1, ORDINAL1, VECTSP_2, VALUED_0, VECTSP_1, BINOP_1,
POLYRED, REWRITE1, STRUCT_0, MCART_1, TERMORD, GROEB_1, BROUWER,
MESFUNC1, CAT_3, GROUP_1, IDEAL_1, FINSET_1, NAT_1, GROEB_2;
notations TARSKI, RELAT_1, XBOOLE_0, SUBSET_1, RELAT_2, RELSET_1, FUNCT_1,
ORDINAL1, XCMPLX_0, PARTFUN1, FINSET_1, XTUPLE_0, MCART_1, XXREAL_0,
FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_1, VECTSP_2, POLYNOM7, PBOOLE,
ORDERS_2, REWRITE1, BAGORDER, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1,
POLYNOM1, TERMORD, IDEAL_1, POLYRED, GROUP_1, NAT_D, NUMBERS, NAT_1,
GROEB_1, RFINSEQ, FINSEQ_7, WAYBEL_4, RECDEF_1;
constructors RFINSEQ, REWRITE1, FINSEQ_7, VECTSP_2, WAYBEL_4, WELLFND1,
IDEAL_1, BAGORDER, TERMORD, POLYRED, GROEB_1, RECDEF_1, REAL_1, RELSET_1,
PBOOLE, BINOP_2, VFUNCT_1, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, FINSEQ_1,
REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, GCD_1, POLYNOM1,
POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, TERMORD, POLYRED, VALUED_0,
ALGSTR_0, PRE_POLY, CARD_1, VFUNCT_1, FUNCT_1, FUNCT_2, RELSET_1,
XTUPLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, ALGSTR_0;
expansions STRUCT_0;
theorems TARSKI, RELSET_1, FINSEQ_1, ZFMISC_1, VECTSP_1, POLYNOM1, FINSEQ_4,
RLVECT_1, NAT_1, POLYNOM7, REWRITE1, XBOOLE_0, IDEAL_1, TERMORD, INT_1,
FUNCT_1, FINSET_1, XBOOLE_1, VECTSP_2, POLYRED, FUNCT_2, BINOM, FINSEQ_3,
RELAT_1, RELAT_2, WAYBEL_4, BAGORDER, RFINSEQ, FINSEQ_5, ALGSTR_1,
FINSEQ_7, GROEB_1, GROUP_1, XREAL_1, XXREAL_0, PARTFUN1, VALUED_0,
STRUCT_0, NAT_D, PRE_POLY, XTUPLE_0, ORDINAL1;
schemes NAT_1, CLASSES1;
begin :: Preliminaries
theorem
for L being add-associative right_zeroed right_complementable non
empty addLoopStr, p being FinSequence of L, n being Element of NAT st for k
being Element of NAT st k in dom p & k > n holds p.k = 0.L holds Sum p = Sum(p|
n)
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr, p be FinSequence of L, n be Element of NAT;
defpred P[Nat] means for p being FinSequence of L, n being
Element of NAT st len p = $1 & for k being Element of NAT st k in dom p & k > n
holds p.k = 0.L holds Sum p = Sum(p|n);
A1: now
let k be Nat;
assume
A2: P[k];
now
let p be FinSequence of L, n be Element of NAT;
assume that
A3: len p = k+1 and
A4: for l being Element of NAT st l in dom p & l > n holds p.l = 0.L;
A5: dom p = Seg(k+1) by A3,FINSEQ_1:def 3;
set q = p|(Seg k);
reconsider q as FinSequence of L by FINSEQ_1:18;
A6: k <= len p by A3,NAT_1:11;
then
A7: len q = k by FINSEQ_1:17;
k <= k + 1 & dom q = Seg(k) by A6,FINSEQ_1:17,NAT_1:11;
then
A8: dom q c= dom p by A5,FINSEQ_1:5;
A9: q = p|k by FINSEQ_1:def 16;
A10: q^<*p/.(k+1)*> = q^<*p.(k+1)*> by A5,FINSEQ_1:4,PARTFUN1:def 6
.= p by A3,FINSEQ_3:55;
now
per cases;
case
A11: k < n;
A12: dom(p|n) = dom(p|(Seg n)) by FINSEQ_1:def 16;
A13: k + 1 <= n by A11,NAT_1:13;
A14: now
let u be object;
assume
A15: u in dom p;
then reconsider u9 = u as Element of NAT;
A16: u in Seg(k+1) by A3,A15,FINSEQ_1:def 3;
then u9 <= k + 1 by FINSEQ_1:1;
then
A17: u9 <= n by A13,XXREAL_0:2;
1 <= u9 by A16,FINSEQ_1:1;
then u9 in Seg n by A17,FINSEQ_1:1;
then u9 in dom(p) /\ (Seg n) by A15,XBOOLE_0:def 4;
hence u in dom(p|n) by A12,RELAT_1:61;
end;
A18: for x being object st x in dom(p|(Seg n)) holds (p|(Seg n)).x = p.
x by FUNCT_1:47;
now
let u be object;
assume u in dom(p|n);
then
A19: u in dom(p|(Seg n)) by FINSEQ_1:def 16;
dom(p|(Seg n)) c= dom p by RELAT_1:60;
hence u in dom p by A19;
end;
then dom(p|n) = dom p by A14,TARSKI:2;
then p|(Seg n) = p by A12,A18,FUNCT_1:2;
hence Sum(p|n) = Sum p by FINSEQ_1:def 16;
end;
case
A20: n <= k;
A21: now
let l be Element of NAT;
assume that
A22: l in dom q and
A23: l > n;
A24: p.l = 0.L by A4,A8,A22,A23;
thus q.l = q/.l by A22,PARTFUN1:def 6
.= p/.l by A9,A22,FINSEQ_4:70
.= 0.L by A8,A22,A24,PARTFUN1:def 6;
end;
k + 1 > n by A20,NAT_1:13;
then
A25: 0.L = p.(k+1) by A4,A5,FINSEQ_1:4
.= p/.(k+1) by A5,FINSEQ_1:4,PARTFUN1:def 6;
thus Sum p = Sum q + Sum(<*p/.(k+1)*>) by A10,RLVECT_1:41
.= Sum q + p/.(k+1) by RLVECT_1:44
.= Sum q by A25,RLVECT_1:def 4
.= Sum(q|n) by A2,A7,A21
.= Sum(p|n) by A9,A20,FINSEQ_1:82;
end;
end;
hence Sum p = Sum(p|n);
end;
hence P[k+1];
end;
A26: P[ 0 ] by FINSEQ_1:58;
A27: for k being Nat holds P[k] from NAT_1:sch 2(A26,A1);
A28: ex k being Element of NAT st len p = k;
assume for k being Element of NAT st k in dom p & k > n holds p.k = 0.L;
hence thesis by A27,A28;
end;
theorem
for L being add-associative right_zeroed Abelian non empty addLoopStr
, f being FinSequence of L, i,j being Element of NAT holds Sum Swap(f,i,j) =
Sum f
proof
let L be add-associative right_zeroed Abelian non empty addLoopStr, f be
FinSequence of L, i,j be Element of NAT;
per cases;
suppose
not(1 <= i & i <= len f & 1 <= j & j <= len f);
hence thesis by FINSEQ_7:def 2;
end;
suppose
A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
then j in Seg(len f) by FINSEQ_1:1;
then
A2: j in dom f by FINSEQ_1:def 3;
i in Seg(len f) by A1,FINSEQ_1:1;
then
A3: i in dom f by FINSEQ_1:def 3;
now
per cases by XXREAL_0:1;
case
i = j;
hence thesis by FINSEQ_7:19;
end;
case
A4: i < j;
then Swap(f, i, j) = (f|(i-'1))^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f
/^j) by A1,FINSEQ_7:27;
then
A5: Sum(Swap(f, i, j)) = Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1 )^<*f
/.i*>) + Sum(f/^j) by RLVECT_1:41
.= (Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1)) + Sum(<*f/.i*>)) + Sum
(f/^j) by RLVECT_1:41
.= ((Sum(f|(i-'1)^<*f/.j*>) + Sum((f/^i)|(j-'i-'1))) + Sum(<*f/.i
*>)) + Sum(f/^j) by RLVECT_1:41
.= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum((f/^i)|(j-'i-'1))) +
Sum(<*f/.i*>)) + Sum(f/^j) by RLVECT_1:41
.= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>)) + Sum((f/^i)
|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 3
.= (((Sum(f|(i-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>)) + Sum((f/^i)
|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 3
.= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum(<*f/.j*>)) + Sum((f/^i)|(j-'
i-'1))) + Sum(f/^j) by RLVECT_1:41
.= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum((f/^i)|(j-'i-'1))) + Sum(<*f
/.j*>)) + Sum(f/^j) by RLVECT_1:def 3
.= (Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))) + Sum(<*f/.j*>))
+ Sum(f/^j) by RLVECT_1:41
.= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)) + Sum(
f/^j) by RLVECT_1:41
.= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j))
by RLVECT_1:41;
(f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j) = (f|(
i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j) by A3,PARTFUN1:def 6
.= (f|(i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f.j*>)^(f/^j) by A2,
PARTFUN1:def 6
.= f by A1,A4,FINSEQ_7:1;
hence thesis by A5;
end;
case
A6: i > j;
then Swap(f, j, i) = (f|(j-'1))^<*f/.i*>^(f/^j)|(i-'j-'1)^<*f/.j*>^(f
/^i) by A1,FINSEQ_7:27;
then
A7: Sum(Swap(f, j, i)) = Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1 )^<*f
/.j*>) + Sum(f/^i) by RLVECT_1:41
.= (Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1)) + Sum(<*f/.j*>)) + Sum
(f/^i) by RLVECT_1:41
.= ((Sum(f|(j-'1)^<*f/.i*>) + Sum((f/^j)|(i-'j-'1))) + Sum(<*f/.j
*>)) + Sum(f/^i) by RLVECT_1:41
.= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum((f/^j)|(i-'j-'1))) +
Sum(<*f/.j*>)) + Sum(f/^i) by RLVECT_1:41
.= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>)) + Sum((f/^j)
|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 3
.= (((Sum(f|(j-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>)) + Sum((f/^j)
|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 3
.= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum(<*f/.i*>)) + Sum((f/^j)|(i-'
j-'1))) + Sum(f/^i) by RLVECT_1:41
.= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum((f/^j)|(i-'j-'1))) + Sum(<*f
/.i*>)) + Sum(f/^i) by RLVECT_1:def 3
.= (Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))) + Sum(<*f/.i*>))
+ Sum(f/^i) by RLVECT_1:41
.= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)) + Sum(
f/^i) by RLVECT_1:41
.= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i))
by RLVECT_1:41;
(f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i) = (f|(
j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i) by A2,PARTFUN1:def 6
.= (f|(j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f.i*>)^(f/^i) by A3,
PARTFUN1:def 6
.= f by A1,A6,FINSEQ_7:1;
hence thesis by A7,FINSEQ_7:21;
end;
end;
hence thesis;
end;
end;
definition
let X be set, b1,b2 be bag of X;
assume
A1: b2 divides b1;
func b1 / b2 -> bag of X means
:Def1:
b2 + it = b1;
existence by A1,TERMORD:1;
uniqueness
proof
let b3,b4 be bag of X;
assume
A2: b2 + b3 = b1;
assume
A3: b2 + b4 = b1;
A4: now
let x be object;
assume x in dom b3;
thus b3.x = (b2.x + b3.x) -' b2.x by NAT_D:34
.= b1.x -' b2.x by A2,PRE_POLY:def 5
.= (b2.x + b4.x) -' b2.x by A3,PRE_POLY:def 5
.= b4.x by NAT_D:34;
end;
dom b3 = X by PARTFUN1:def 2
.= dom b4 by PARTFUN1:def 2;
hence thesis by A4,FUNCT_1:2;
end;
end;
definition
let X be set, b1,b2 be bag of X;
func lcm(b1,b2) -> bag of X means
:Def2:
for k being object holds it.k = max(b1 .k,b2.k);
existence
proof
defpred Q[object,object] means $2 = max(b1.$1,b2.$1);
A1: for x being object st x in X ex y being object st Q[x,y];
consider b being Function such that
A2: dom b = X & for x being object st x in X holds Q[x,b.x] from CLASSES1
:sch 1(A1);
reconsider b as ManySortedSet of X by A2,PARTFUN1:def 2,RELAT_1:def 18;
now
let u be object;
assume u in rng b;
then consider x being object such that
A3: x in dom b & u = b.x by FUNCT_1:def 3;
u = max(b1.x,b2.x) by A2,A3;
hence u in NAT by ORDINAL1:def 12;
end;
then
A4: rng b c= NAT by TARSKI:def 3;
now
let u be object;
A5: support b c= dom b by PRE_POLY:37;
assume
A6: u in support b;
then
A7: b.u <> 0 by PRE_POLY:def 7;
now
assume
A8: not u in support(b1) \/ support(b2);
then not u in support(b2) by XBOOLE_0:def 3;
then
A9: b2.u = 0 by PRE_POLY:def 7;
not u in support(b1) by A8,XBOOLE_0:def 3;
then b1.u = 0 by PRE_POLY:def 7;
then max(b1.u,b2.u) = 0 by A9;
hence contradiction by A2,A6,A7,A5;
end;
hence u in support(b1) \/ support(b2);
end;
then support b c= (support(b1) \/ support(b2)) by TARSKI:def 3;
then reconsider b as bag of X by A4,PRE_POLY:def 8,VALUED_0:def 6;
A10: dom b = X by PARTFUN1:def 2
.= dom b2 by PARTFUN1:def 2;
take b;
A11: dom b = X by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2;
now
let k be object;
now
per cases;
case
k in dom b;
hence b.k = max(b1.k,b2.k) by A2;
end;
case
A12: not k in dom b;
then b1.k = 0 & b2.k = 0 by A11,A10,FUNCT_1:def 2;
hence b.k = max(b1.k,b2.k) by A12,FUNCT_1:def 2;
end;
end;
hence b.k = max(b1.k,b2.k);
end;
hence thesis;
end;
uniqueness
proof
let b3,b4 be bag of X;
assume
A13: for k being object holds b3.k = max(b1.k,b2.k);
assume
A14: for k being object holds b4.k = max(b1.k,b2.k);
A15: now
let u be object;
assume u in dom b3;
thus b3.u = max(b1.u,b2.u) by A13
.= b4.u by A14;
end;
dom b3 = X by PARTFUN1:def 2
.= dom b4 by PARTFUN1:def 2;
hence thesis by A15,FUNCT_1:2;
end;
commutativity;
idempotence;
end;
notation
let X be set, b1,b2 be bag of X;
synonym b1 lcm b2 for lcm(b1,b2);
end;
:: exercise 5.45, p. 211
definition
let X be set, b1,b2 be bag of X;
pred b1,b2 are_disjoint means
for i being object holds b1.i = 0 or b2.i = 0;
end;
notation
let X be set, b1,b2 be bag of X;
antonym b1,b2 are_non_disjoint for b1,b2 are_disjoint;
end;
theorem Th3:
for X being set, b1,b2 being bag of X holds b1 divides lcm(b1,b2)
& b2 divides lcm(b1,b2)
proof
let X be set, b1,b2 be bag of X;
set bb = lcm(b1,b2);
now
let k be object;
b1.k <= max(b1.k,b2.k) by XXREAL_0:25;
hence b1.k <= bb.k by Def2;
end;
hence b1 divides lcm(b1,b2) by PRE_POLY:def 11;
now
let k be object;
b2.k <= max(b1.k,b2.k) by XXREAL_0:25;
hence b2.k <= bb.k by Def2;
end;
hence thesis by PRE_POLY:def 11;
end;
:: exercise 5.45, p. 211
theorem Th4:
for X being set, b1,b2,b3 be bag of X holds b1 divides b3 & b2
divides b3 implies lcm(b1,b2) divides b3
proof
let X being set, b1,b2,b3 be bag of X;
assume that
A1: b1 divides b3 and
A2: b2 divides b3;
now
let k be object;
assume k in X;
now
per cases by XXREAL_0:16;
case
max(b1.k,b2.k) = b1.k;
hence max(b1.k,b2.k) <= b3.k by A1,PRE_POLY:def 11;
end;
case
max(b1.k,b2.k) = b2.k;
hence max(b1.k,b2.k) <= b3.k by A2,PRE_POLY:def 11;
end;
end;
hence lcm(b1,b2).k <= b3.k by Def2;
end;
hence thesis by PRE_POLY:46;
end;
:: exercise 5.45, p. 211
theorem
for X being set, b1,b2 being bag of X holds b1,b2 are_disjoint iff lcm
(b1,b2) = b1 + b2
proof
let X be set, b1,b2 be bag of X;
A1: now
assume
A2: lcm(b1,b2) = b1 + b2;
now
let k be object;
A3: lcm(b1,b2).k = max(b1.k,b2.k) by Def2;
now
per cases by A2,A3,XXREAL_0:16;
case
(b1 + b2).k = b1.k;
then b1.k + b2.k = b1.k + 0 by PRE_POLY:def 5;
hence b2.k = 0;
end;
case
(b1 + b2).k = b2.k;
then b1.k + b2.k = 0 + b2.k by PRE_POLY:def 5;
hence b1.k = 0;
end;
end;
hence b1.k = 0 or b2.k = 0;
end;
hence b1,b2 are_disjoint;
end;
now
assume
A4: b1,b2 are_disjoint;
now
let k be object;
now
per cases by A4;
case
A5: b1.k = 0;
hence (b1+b2).k = 0 + b2.k by PRE_POLY:def 5
.= max(b1.k,b2.k) by A5,XXREAL_0:def 10;
end;
case
A6: b2.k = 0;
hence (b1+b2).k = b1.k + 0 by PRE_POLY:def 5
.= max(b1.k,b2.k) by A6,XXREAL_0:def 10;
end;
end;
hence (b1+b2).k = max(b1.k,b2.k);
end;
hence lcm(b1,b2) = b1 + b2 by Def2;
end;
hence thesis by A1;
end;
theorem Th6:
for X being set, b being bag of X holds b/b = EmptyBag X
proof
let X be set, b be bag of X;
b + EmptyBag X = b by PRE_POLY:53;
hence thesis by Def1;
end;
theorem Th7:
for X being set, b1,b2 be bag of X holds b2 divides b1 iff lcm( b1,b2) = b1
proof
let X being set, b1,b2 be bag of X;
now
assume
A1: b2 divides b1;
for k being object holds b1.k = max(b1.k,b2.k)
by XXREAL_0:def 10,A1,PRE_POLY:def 11;
hence lcm(b1,b2) = b1 by Def2;
end;
hence thesis by Th3;
end;
theorem
for X being set, b1,b2,b3 being bag of X holds b1 divides lcm(b2,b3)
implies lcm(b2,b1) divides lcm(b2,b3)
proof
let X being set, b1,b2,b3 be bag of X;
assume
A1: b1 divides lcm(b2,b3);
for k being object st k in X holds lcm(b2,b1).k <= lcm(b2,b3).k
proof
let k be object;
assume k in X;
b1.k <= lcm(b2,b3).k by A1,PRE_POLY:def 11;
then
A2: b1.k <= max(b2.k,b3.k) by Def2;
b2.k <= max(b2.k,b3.k) by XXREAL_0:25;
then max(b2.k,b1.k) <= max(b2.k,b3.k) by A2,XXREAL_0:28;
then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
hence thesis by Def2;
end;
hence thesis by PRE_POLY:46;
end;
:: exercise 5.69 (i) ==> (ii), p. 223
theorem
for X being set, b1,b2,b3 being bag of X holds lcm(b2,b1) divides lcm(
b2,b3) implies lcm(b1,b3) divides lcm(b2,b3)
proof
let X be set, b1,b2,b3 be bag of X;
assume
A1: lcm(b2,b1) divides lcm(b2,b3);
for k being object st k in X holds lcm(b1,b3).k <= lcm(b2,b3).k
proof
let k be object;
assume k in X;
A2: b3.k <= max(b2.k,b3.k) by XXREAL_0:25;
lcm(b2,b1).k <= lcm(b2,b3).k by A1,PRE_POLY:def 11;
then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
then
A3: max(b2.k,b1.k) <= max(b2.k,b3.k) by Def2;
b1.k <= max(b2.k,b1.k) by XXREAL_0:25;
then b1.k <= max(b2.k,b3.k) by A3,XXREAL_0:2;
then max(b1.k,b3.k) <= max(b2.k,b3.k) by A2,XXREAL_0:28;
then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
hence thesis by Def2;
end;
hence thesis by PRE_POLY:46;
end;
:: exercise 5.69 (ii) ==> (iii), p. 223
theorem
for n being set, b1,b2,b3 being bag of n holds lcm(b1,b3) divides lcm(
b2,b3) implies b1 divides lcm(b2,b3)
proof
let X be set, b1,b2,b3 be bag of X;
assume
A1: lcm(b1,b3) divides lcm(b2,b3);
for k being object st k in X holds b1.k <= lcm(b2,b3).k
proof
let k be object;
assume k in X;
lcm(b1,b3).k <= lcm(b2,b3).k by A1,PRE_POLY:def 11;
then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
then
A2: max(b1.k,b3.k) <= max(b2.k,b3.k) by Def2;
b1.k <= max(b1.k,b3.k) by XXREAL_0:25;
then b1.k <= max(b2.k,b3.k) by A2,XXREAL_0:2;
hence thesis by Def2;
end;
hence thesis by PRE_POLY:46;
end;
:: exercise 5.69 (iii) ==> (i), p. 223
theorem
for n being Element of NAT, T being connected admissible TermOrder of
n, P being non empty Subset of Bags n ex b being bag of n st b in P & for b9
being bag of n st b9 in P holds b <= b9,T
proof
let n be Element of NAT, T be connected admissible TermOrder of n, P be non
empty Subset of Bags n;
set R = RelStr(#Bags n, T#), m = MinElement(P,R);
A1: T is_connected_in field T by RELAT_2:def 14;
reconsider b = m as bag of n;
A2: m is_minimal_wrt P,the InternalRel of R by BAGORDER:def 17;
A3: now
let b9 be bag of n;
b <= b,T by TERMORD:6;
then [b,b] in T by TERMORD:def 2;
then
A4: b in field T by RELAT_1:15;
b9 <= b9,T by TERMORD:6;
then [b9,b9] in T by TERMORD:def 2;
then
A5: b9 in field T by RELAT_1:15;
assume
A6: b9 in P;
now
per cases;
case
b9 = b;
hence b <= b9,T by TERMORD:6;
end;
case
A7: b9 <> b;
then not [b9,b] in T by A2,A6,WAYBEL_4:def 25;
then [b,b9] in T by A1,A4,A5,A7,RELAT_2:def 6;
hence b <= b9,T by TERMORD:def 2;
end;
end;
hence b <= b9,T;
end;
m in P by BAGORDER:def 17;
hence thesis by A3;
end;
registration
let L be add-associative right_zeroed right_complementable non trivial
addLoopStr, a be non zero Element of L;
cluster -a -> non zero;
coherence
proof
now
assume -a = 0.L;
then --a = 0.L by RLVECT_1:12;
hence contradiction by RLVECT_1:17;
end;
hence thesis;
end;
end;
registration
let X be set, L be left_zeroed right_zeroed add-cancelable distributive non
empty doubleLoopStr, m be Monomial of X,L, a be Element of L;
cluster a * m -> monomial-like;
coherence
proof
set p = a * m;
now
per cases by POLYNOM7:6;
case
A1: Support m = {};
now
set b = the Element of Support p;
assume
A2: Support p <> {};
then b in Support p;
then reconsider b as Element of Bags X;
p.b = a * m.b by POLYNOM7:def 9
.= a * 0.L by A1,POLYNOM1:def 4
.= 0.L by BINOM:2;
hence contradiction by A2,POLYNOM1:def 4;
end;
hence thesis by POLYNOM7:6;
end;
case
ex b being bag of X st Support m = {b};
then consider b being bag of X such that
A3: Support m = {b};
reconsider b as Element of Bags X by PRE_POLY:def 12;
now
per cases;
case
A4: a = 0.L;
now
set b = the Element of Support p;
assume
A5: Support p <> {};
then b in Support p;
then reconsider b as Element of Bags X;
p.b = a * m.b by POLYNOM7:def 9
.= 0.L by A4,BINOM:1;
hence contradiction by A5,POLYNOM1:def 4;
end;
hence Support p = {};
end;
case
a <> 0.L;
A6: now
let b9 be Element of Bags X;
assume b9 <> b;
then not b9 in Support m by A3,TARSKI:def 1;
then
A7: m.b9 = 0.L by POLYNOM1:def 4;
p.b9 = a * m.b9 by POLYNOM7:def 9;
hence p.b9 = 0.L by A7,BINOM:2;
end;
now
per cases;
case
A8: a * m.b = 0.L;
now
set b9 = the Element of Support p;
assume
A9: Support p <> {};
then b9 in Support p;
then reconsider b9 as Element of Bags X;
A10: p.b9 <> 0.L by A9,POLYNOM1:def 4;
then b9 = b by A6;
hence contradiction by A8,A10,POLYNOM7:def 9;
end;
hence Support p = {};
end;
case
A11: a * m.b <> 0.L;
A12: now
let u be object;
assume
A13: u in Support p;
then reconsider u9 = u as Element of Bags X;
p.u9 <> 0.L by A13,POLYNOM1:def 4;
then u9 = b by A6;
hence u in {b} by TARSKI:def 1;
end;
now
let u be object;
assume u in {b};
then
A14: u = b by TARSKI:def 1;
p.b <> 0.L by A11,POLYNOM7:def 9;
hence u in Support p by A14,POLYNOM1:def 4;
end;
hence Support p = {b} by A12,TARSKI:2;
end;
end;
hence thesis by POLYNOM7:6;
end;
end;
hence thesis by POLYNOM7:6;
end;
end;
hence thesis;
end;
end;
registration
let n be Ordinal, L be left_zeroed right_zeroed add-cancelable distributive
domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n,L, a be
non zero Element of L;
cluster a * p -> non-zero;
coherence
proof
set b = the Element of Support p;
set ap = a * p;
p <> 0_(n,L) by POLYNOM7:def 1;
then
A1: Support p <> {} by POLYNOM7:1;
then b in Support p;
then reconsider b as Element of Bags n;
p.b <> 0.L by A1,POLYNOM1:def 4;
then a * p.b <> 0.L by VECTSP_2:def 1;
then ap.b <> 0.L by POLYNOM7:def 9;
then b in Support ap by POLYNOM1:def 4;
then ap <> 0_(n,L) by POLYNOM7:1;
hence thesis by POLYNOM7:def 1;
end;
end;
theorem Th12:
for n being Ordinal, L being right_zeroed right-distributive
non empty doubleLoopStr, p,q being Series of n,L, b being bag of n holds b *'
(p + q) = b *' p + b *' q
proof
let n be Ordinal, L be right_zeroed right-distributive non empty
doubleLoopStr, p1,p2 be Series of n,L, b be bag of n;
set q1 = b *' (p1 + p2), q2 = b *' p1 + b *' p2;
A1: now
let x be object;
assume x in dom q1;
then reconsider u = x as bag of n;
now
per cases;
case
A2: b divides u;
hence q1.u = (p1+p2).(u -' b) by POLYRED:def 1
.= p1.(u -' b) + p2.(u -' b) by POLYNOM1:15
.= (b*'p1).u + p2.(u -' b) by A2,POLYRED:def 1
.= (b*'p1).u + (b*'p2).u by A2,POLYRED:def 1
.= q2.u by POLYNOM1:15;
end;
case
A3: not b divides u;
hence q1.u = 0.L by POLYRED:def 1
.= 0.L + 0.L by RLVECT_1:def 4
.= (b*'p1).u + 0.L by A3,POLYRED:def 1
.= (b*'p1).u + (b*'p2).u by A3,POLYRED:def 1
.= q2.u by POLYNOM1:15;
end;
end;
hence q1.x = q2.x;
end;
dom q1 = Bags n by FUNCT_2:def 1
.= dom q2 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th13:
for n being Ordinal, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being Series of n,L, b being bag
of n holds b *' (-p) = -(b *' p)
proof
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Series of n,L, b be bag of n;
set q1 = b *' (-p), q2 = -(b *' p);
A1: now
let x be object;
assume x in dom q1;
then reconsider u = x as bag of n;
now
per cases;
case
A2: b divides u;
then
A3: (b*'p).u = p.(u-'b) by POLYRED:def 1;
thus q1.u = (-p).(u-'b) by A2,POLYRED:def 1
.= -(p.(u-'b)) by POLYNOM1:17
.= (-(b*'p)).u by A3,POLYNOM1:17;
end;
case
A4: not b divides u;
then
A5: (b*'p).u = 0.L by POLYRED:def 1;
thus q1.u = 0.L by A4,POLYRED:def 1
.= -0.L by RLVECT_1:12
.= q2.u by A5,POLYNOM1:17;
end;
end;
hence q1.x = q2.x;
end;
dom q1 = Bags n by FUNCT_2:def 1
.= dom q2 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th14:
for n being Ordinal, L being left_zeroed right_add-cancelable
right-distributive non empty doubleLoopStr, p being Series of n,L, b being
bag of n, a being Element of L holds b *' (a * p) = a * (b *' p)
proof
let n be Ordinal, L be left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr, p be Series of n,L, b be bag of n, a be Element of L;
set q1 = b *' (a * p), q2 = a * (b *' p);
A1: now
let x be object;
assume x in dom q1;
then reconsider u = x as bag of n;
now
per cases;
case
A2: b divides u;
hence q1.u = (a*p).(u-'b) by POLYRED:def 1
.= a * p.(u-'b) by POLYNOM7:def 9
.= a * (b*'p).u by A2,POLYRED:def 1
.= q2.u by POLYNOM7:def 9;
end;
case
A3: not b divides u;
hence q1.u = 0.L by POLYRED:def 1
.= a * 0.L by BINOM:2
.= a * (b*'p).u by A3,POLYRED:def 1
.= q2.u by POLYNOM7:def 9;
end;
end;
hence q1.x = q2.x;
end;
dom q1 = Bags n by FUNCT_2:def 1
.= dom q2 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th15:
for n being Ordinal, L being right-distributive non empty
doubleLoopStr, p,q being Series of n,L, a being Element of L holds a * (p + q)
= a * p + a * q
proof
let n be Ordinal, L be right-distributive non empty doubleLoopStr, p1,p2
be Series of n,L, b be Element of L;
set q1 = b * (p1 + p2), q2 = b * p1 + b * p2;
A1: now
let x be object;
assume x in dom q1;
then reconsider u = x as bag of n;
q1.u = b * (p1+p2).u by POLYNOM7:def 9
.= b * (p1.u + p2.u) by POLYNOM1:15
.= b * p1.u + b * p2.u by VECTSP_1:def 2
.= (b*p1).u + b * p2.u by POLYNOM7:def 9
.= (b*p1).u + (b*p2).u by POLYNOM7:def 9
.= (b*p1 + b*p2).u by POLYNOM1:15;
hence q1.x = q2.x;
end;
dom q1 = Bags n by FUNCT_2:def 1
.= dom q2 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th16:
for X being set, L being add-associative right_zeroed
right_complementable non empty doubleLoopStr, a being Element of L holds -(a
|(X,L)) = (-a) |(X,L)
proof
let n be set, L be add-associative right_zeroed right_complementable non
empty doubleLoopStr, a be Element of L;
A1: now
let u be object;
assume u in dom((-a) |(n,L));
then reconsider u9 = u as Element of Bags n;
now
per cases;
case
A2: u9 = EmptyBag n;
hence -((a |(n,L)).u9) = - a by POLYNOM7:18
.= ((-a) |(n,L)).u9 by A2,POLYNOM7:18;
end;
case
A3: u9 <> EmptyBag n;
-0.L = 0.L by RLVECT_1:12;
hence -((a |(n,L)).u9) = 0.L by A3,POLYNOM7:18
.= ((-a) |(n,L)).u9 by A3,POLYNOM7:18;
end;
end;
hence ((-a) |(n,L)).u = (- (a |(n,L))).u by POLYNOM1:17;
end;
dom(- (a |(n,L))) = Bags n by FUNCT_2:def 1
.= dom((-a) |(n,L)) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
Lm1: 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, g being object, P being Subset of Polynom-Ring(n,L)
holds
PolyRedRel(P,T) reduces f,g implies g is Polynomial of 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 be
Polynomial of n,L, g be object, P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume R reduces f,g;
then consider p being RedSequence of R such that
A1: p.1 = f and
A2: p.len p = g by REWRITE1:def 3;
A3: 1 <= len(p) by NAT_1:14;
reconsider l = len p - 1 as Element of NAT by INT_1:5,NAT_1:14;
set h = p.l;
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg(len p) by FINSEQ_1:1;
then
A4: l + 1 in dom p by FINSEQ_1:def 3;
per cases;
suppose
len p = 1;
hence thesis by A1,A2;
end;
suppose
len p <> 1;
then 0 + 1 < l + 1 by A3,XXREAL_0:1;
then
A5: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg(len p) by A5,FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A2,A4,REWRITE1:def 2;
then consider h9,g9 being object such that
A6: [h,g] = [h9,g9] and
h9 in NonZero Polynom-Ring(n,L) and
A7: g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
g = g9 by A6,XTUPLE_0:1;
hence thesis by A7,POLYNOM1:def 11;
end;
end;
begin :: S-Polynomials
theorem Th17:
for n being Element of NAT, T being connected admissible
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, P being Subset of Polynom-Ring(n,L)
holds (for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P for m1
,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T) holds PolyRedRel(P,T
) reduces m1 *' p1 - m2 *' p2, 0_(n,L)) implies P is_Groebner_basis_wrt T
proof
let n be Element of NAT, 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, P be Subset of Polynom-Ring(n,L);
assume
A1: for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P
for m1,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T) holds
PolyRedRel(P,T) reduces m1 *' p1 - m2 *' p2, 0_(n,L);
set R = PolyRedRel(P,T);
A2: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
now
let a,b,c being object;
assume that
A3: [a,b] in R and
A4: [a,c] in R;
consider f,f1 being object such that
A5: f in NonZero Polynom-Ring(n,L) and
A6: f1 in the carrier of Polynom-Ring(n,L) and
A7: [a,b] = [f,f1] by A3,ZFMISC_1:def 2;
A8: not f in {0_(n,L)} by A2,A5,XBOOLE_0:def 5;
reconsider f as Polynomial of n,L by A5,POLYNOM1:def 11;
f <> 0_(n,L) by A8,TARSKI:def 1;
then reconsider f as non-zero Polynomial of n,L by POLYNOM7:def 1;
reconsider f1 as Polynomial of n,L by A6,POLYNOM1:def 11;
f reduces_to f1,P,T by A3,A7,POLYRED:def 13;
then consider g1 being Polynomial of n,L such that
A9: g1 in P and
A10: f reduces_to f1,g1,T by POLYRED:def 7;
ex b1 being bag of n st f reduces_to f1,g1,b1,T by A10,POLYRED:def 6;
then
A11: g1 <> 0_(n,L) by POLYRED:def 5;
consider f9,f2 being object such that
f9 in NonZero Polynom-Ring(n,L) and
A12: f2 in the carrier of Polynom-Ring(n,L) and
A13: [a,c] = [f9,f2] by A4,ZFMISC_1:def 2;
reconsider f2 as Polynomial of n,L by A12,POLYNOM1:def 11;
A14: f2 = c by A13,XTUPLE_0:1;
reconsider g1 as non-zero Polynomial of n,L by A11,POLYNOM7:def 1;
consider m1 being Monomial of n,L such that
A15: f1 = f - m1 *' g1 and
A16: not HT(m1*'g1,T) in Support f1 and
HT(m1*'g1,T) <= HT(f,T),T by A10,GROEB_1:2;
A17: f9 = a by A13,XTUPLE_0:1;
A18: f9 = a by A13,XTUPLE_0:1
.= f by A7,XTUPLE_0:1;
then f reduces_to f2,P,T by A4,A13,POLYRED:def 13;
then consider g2 being Polynomial of n,L such that
A19: g2 in P and
A20: f reduces_to f2,g2,T by POLYRED:def 7;
ex b2 being bag of n st f reduces_to f2,g2,b2,T by A20,POLYRED:def 6;
then
A21: g2 <> 0_(n,L) by POLYRED:def 5;
then reconsider g2 as non-zero Polynomial of n,L by POLYNOM7:def 1;
consider m2 being Monomial of n,L such that
A22: f2 = f - m2 *' g2 and
A23: not HT(m2*'g2,T) in Support f2 and
HT(m2*'g2,T) <= HT(f,T),T by A20,GROEB_1:2;
set mg1 = m1 *' g1, mg2 = m2 *' g2;
A24: f1 = b by A7,XTUPLE_0:1;
now
per cases;
case
m1 = 0_(n,L);
then f1 = f - 0_(n,L) by A15,POLYRED:5
.= f by POLYRED:4;
then
A25: R reduces b,c by A4,A18,A24,A17,REWRITE1:15;
R reduces c,c by REWRITE1:12;
hence b,c are_convergent_wrt R by A25,REWRITE1:def 7;
end;
case
m2 = 0_(n,L);
then f2 = f - 0_(n,L) by A22,POLYRED:5
.= f by POLYRED:4;
then
A26: R reduces c,b by A3,A18,A14,A17,REWRITE1:15;
R reduces b,b by REWRITE1:12;
hence b,c are_convergent_wrt R by A26,REWRITE1:def 7;
end;
case
m1 <> 0_(n,L) & m2 <> 0_(n,L);
then reconsider m1,m2 as non-zero Monomial of n,L by POLYNOM7:def 1;
HT(m1,T) + HT(g1,T) in Support mg1 by TERMORD:29;
then
A27: mg1 <> 0_(n,L) by POLYNOM7:1;
HT(m2,T) + HT(g2,T) in Support mg2 by TERMORD:29;
then
A28: mg2 <> 0_(n,L) by POLYNOM7:1;
A29: HC(g2,T) <> 0.L;
A30: --(m1 *' g1) = m1 *' g1 by POLYNOM1:19;
A31: f2 - f1 = (f + -(m2 *' g2)) - (f - m1 *' g1) by A15,A22,POLYNOM1:def 7
.= (f + -(m2 *' g2)) - (f + -(m1 *' g1)) by POLYNOM1:def 7
.= (f + -(m2 *' g2)) + -(f + -(m1 *' g1)) by POLYNOM1:def 7
.= (f + -(m2 *' g2)) + (-f + --(m1 *' g1)) by POLYRED:1
.= f + (-(m2 *' g2) + (-f + (m1 *' g1))) by A30,POLYNOM1:21
.= f + (-f + (-(m2 *' g2) + (m1 *' g1))) by POLYNOM1:21
.= (f + -f) + (-(m2 *' g2) + (m1 *' g1)) by POLYNOM1:21
.= 0_(n,L) + (-(m2 *' g2) + (m1 *' g1)) by POLYRED:3
.= (m1 *' g1) + -(m2 *' g2) by POLYRED:2
.= mg1 - mg2 by POLYNOM1:def 7;
A32: HC(g1,T) <> 0.L;
A33: --mg1 = mg1 by POLYNOM1:19;
PolyRedRel(P,T) reduces f2-f1,0_(n,L)
proof
now
per cases;
case
mg1 - mg2 = 0_(n,L);
hence thesis by A31,REWRITE1:12;
end;
case
A34: mg1 - mg2 <> 0_(n,L);
now
per cases;
case
g1 = g2;
then f2 - f1 = m1 *' g1 + -(m2 *' g1) by A31,POLYNOM1:def 7
.= g1 *' m1 + (-m2) *' g1 by POLYRED:6
.= (m1 + -m2) *' g1 by POLYNOM1:26;
hence thesis by A9,POLYRED:45;
end;
case
A35: g1 <> g2;
now
per cases;
case
A36: HT(mg1,T) <> HT(mg2,T);
now
per cases;
case
HT(mg2,T) < HT(mg1,T),T;
then not HT(mg1,T) <= HT(mg2,T),T by TERMORD:5;
then not(HT(mg1,T)) in Support(mg2) by TERMORD:def 6;
then
A37: mg2.(HT(mg1,T)) = 0.L by POLYNOM1:def 4;
A38: (mg1-mg2).(HT(mg1,T)) = (mg1+-mg2).(HT(mg1,T))
by POLYNOM1:def 7
.= mg1.(HT(mg1,T))+(-mg2).(HT(mg1,T)) by
POLYNOM1:15
.= mg1.(HT(mg1,T))+-(mg2).(HT(mg1,T)) by
POLYNOM1:17
.= mg1.(HT(mg1,T))+0.L by A37,RLVECT_1:12
.= mg1.(HT(mg1,T)) by RLVECT_1:def 4
.= HC(mg1,T) by TERMORD:def 7;
then (mg1-mg2).(HT(mg1,T)) <> 0.L by A27,TERMORD:17;
then
A39: HT(mg1,T) in Support( mg1 - mg2) by POLYNOM1:def 4;
A40: HT(m1,T) + HT(g1,T) = HT(mg1,T) by TERMORD:31;
(mg1 - mg2) - ((mg1-mg2).HT(mg1,T)/HC(g1,T)) *
(HT(m1,T) *' g1) = (mg1 - mg2) - ((HC(m1,T)*HC(g1,T))/HC(g1,T)) * (HT(m1,T) *'
g1) by A38,TERMORD:32
.= (mg1 - mg2) - ((HC(m1,T)*HC(g1,T))*(HC(g1,T)"
)) * (HT(m1,T) *' g1)
.= (mg1 - mg2) - (HC(m1,T)*(HC(g1,T)*(HC(g1,T)")
)) * (HT(m1,T) *' g1) by GROUP_1:def 3
.= (mg1 - mg2) - (HC(m1,T)*1.L) * (HT(m1,T) *'
g1) by A32,VECTSP_1:def 10
.= (mg1 - mg2) - HC(m1,T) * (HT(m1,T) *' g1)
.= (mg1 - mg2) - Monom(HC(m1,T),HT(m1,T)) *' g1
by POLYRED:22
.= (mg1 - mg2) - Monom(coefficient(m1),HT(m1,T))
*'g1 by TERMORD:23
.= (mg1 - mg2) - Monom(coefficient(m1),term(m1))
*'g1 by TERMORD:23
.= (mg1 - mg2) - mg1 by POLYNOM7:11
.= (mg1+-mg2)-mg1 by POLYNOM1:def 7
.= (mg1+-mg2)+-mg1 by POLYNOM1:def 7
.= (mg1+-mg1)+-mg2 by POLYNOM1:21
.= 0_(n,L)+-mg2 by POLYRED:3
.= -mg2 by POLYRED:2;
then mg1-mg2 reduces_to -mg2,g1,HT(mg1,T),T by A11
,A34,A39,A40,POLYRED:def 5;
then mg1-mg2 reduces_to -mg2,g1,T by POLYRED:def 6;
then mg1-mg2 reduces_to -mg2,P,T by A9,POLYRED:def 7;
then [mg1-mg2,-mg2] in R by POLYRED:def 13;
then
A41: R reduces mg1-mg2,-mg2 by REWRITE1:15;
R reduces (-m2)*'g2,0_(n,L) by A19,POLYRED:45;
then R reduces -mg2,0_(n,L) by POLYRED:6;
hence thesis by A31,A41,REWRITE1:16;
end;
case
not HT(mg2,T) < HT(mg1,T),T;
then HT(mg1,T) <= HT(mg2,T),T by TERMORD:5;
then HT(mg1,T) < HT(mg2,T),T by A36,TERMORD:def 3;
then not HT(mg2,T) <= HT(mg1,T),T by TERMORD:5;
then not(HT(mg2,T)) in Support(mg1) by TERMORD:def 6;
then
A42: mg1.(HT(mg2,T)) = 0.L by POLYNOM1:def 4;
A43: (mg2-mg1).(HT(mg2,T)) = (mg2+-mg1).(HT(mg2,T))
by POLYNOM1:def 7
.= mg2.(HT(mg2,T))+(-mg1).(HT(mg2,T)) by
POLYNOM1:15
.= mg2.(HT(mg2,T))+-(mg1).(HT(mg2,T)) by
POLYNOM1:17
.= mg2.(HT(mg2,T))+0.L by A42,RLVECT_1:12
.= mg2.(HT(mg2,T)) by RLVECT_1:def 4
.= HC(mg2,T) by TERMORD:def 7;
then (mg2-mg1).(HT(mg2,T)) <> 0.L by A28,TERMORD:17;
then
A44: HT(mg2,T) in Support( mg2 - mg1) by POLYNOM1:def 4;
reconsider x = -0_(n,L) as Element of Polynom-Ring(n
,L) by POLYNOM1:def 11;
A45: HT(m2,T) + HT(g2,T) = HT(mg2,T) by TERMORD:31;
reconsider x as Element of Polynom-Ring(n,L);
0.Polynom-Ring(n,L) = 0_(n,L) by POLYNOM1:def 11;
then
A46: x + (0.Polynom-Ring(n, L)) = -0_(n,L) + 0_(n,L)
by POLYNOM1:def 11
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
A47: now
assume mg2 - mg1 = 0_(n,L);
then -(mg2 + -mg1) = - 0_(n,L) by POLYNOM1:def 7;
then -mg2 + -(-mg1) = -0_(n,L) by POLYRED:1;
then
mg1 + -mg2 = -(0.(Polynom-Ring(n,L))) by A33,A46,
RLVECT_1:6
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:12
.= 0_(n,L) by POLYNOM1:def 11;
hence contradiction by A34,POLYNOM1:def 7;
end;
(mg2 - mg1) - ((mg2-mg1).HT(mg2,T)/HC(g2,T)) *
(HT(m2,T) *' g2) = (mg2 - mg1) - ((HC(m2,T)*HC(g2,T))/HC(g2,T)) * (HT(m2,T) *'
g2) by A43,TERMORD:32
.= (mg2 - mg1) - ((HC(m2,T)*HC(g2,T))*(HC(g2,T)"
)) * (HT(m2,T) *' g2)
.= (mg2 - mg1) - (HC(m2,T)*(HC(g2,T)*(HC(g2,T)")
)) * (HT(m2,T) *' g2) by GROUP_1:def 3
.= (mg2 - mg1) - (HC(m2,T)*1.L) * (HT(m2,T) *'
g2) by A29,VECTSP_1:def 10
.= (mg2 - mg1) - HC(m2,T) * (HT(m2,T) *' g2)
.= (mg2 - mg1) - Monom(HC(m2,T),HT(m2,T)) *' g2
by POLYRED:22
.= (mg2 - mg1) - Monom(coefficient(m2),HT(m2,T))
*'g2 by TERMORD:23
.= (mg2 - mg1) - Monom(coefficient(m2),term(m2))
*'g2 by TERMORD:23
.= (mg2 - mg1) - mg2 by POLYNOM7:11
.= (mg2+-mg1)-mg2 by POLYNOM1:def 7
.= (mg2+-mg1)+-mg2 by POLYNOM1:def 7
.= (mg2+-mg2)+-mg1 by POLYNOM1:21
.= 0_(n,L)+-mg1 by POLYRED:3
.= -mg1 by POLYRED:2;
then mg2-mg1 reduces_to -mg1,g2,HT(mg2,T),T by A21
,A44,A45,A47,POLYRED:def 5;
then mg2-mg1 reduces_to -mg1,g2,T by POLYRED:def 6;
then mg2-mg1 reduces_to -mg1,P,T by A19,POLYRED:def 7
;
then [mg2-mg1,-mg1] in R by POLYRED:def 13;
then
A48: R reduces mg2-mg1,-mg1 by REWRITE1:15;
A49: -(1_(n,L)) = -((1.L) |(n,L)) by POLYNOM7:20
.= (-1.L) |(n,L) by Th16;
R reduces (-m1)*'g1,0_(n,L) by A9,POLYRED:45;
then R reduces -mg1,0_(n,L) by POLYRED:6;
then R reduces mg2-mg1,0_(n,L) by A48,REWRITE1:16;
then
A50: R reduces (-1_(n,L))*' (mg2-mg1),(-1_(n,L))*'
0_(n,L) by A49,POLYRED:47;
(-1_(n,L))*'(mg2-mg1) = (-1_(n,L))*'(mg2+-mg1)
by POLYNOM1:def 7
.= (-1_(n,L))*'mg2+(-1_(n,L))*'(-mg1) by
POLYNOM1:26
.= -(1_(n,L)*'mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
.= 1_(n,L)*'(-mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
.= 1_(n,L)*'(-mg2)+(-(1_(n,L)*'(-mg1))) by
POLYRED:6
.= 1_(n,L)*'(-mg2)+1_(n,L)*'(--mg1) by POLYRED:6
.= (-mg2)+1_(n,L)*'mg1 by A33,POLYNOM1:30
.= mg1 + -mg2 by POLYNOM1:30
.= mg1 - mg2 by POLYNOM1:def 7;
hence thesis by A31,A50,POLYNOM1:28;
end;
end;
hence thesis;
end;
case
A51: HT(mg1,T) = HT(mg2,T);
(f-mg2).HT(mg2,T) = 0.L by A22,A23,POLYNOM1:def 4;
then (f+-mg2).HT(mg2,T) = 0.L by POLYNOM1:def 7;
then f.HT(mg2,T) + (-mg2).HT(mg2,T) = 0.L by POLYNOM1:15;
then f.HT(mg2,T) + -(mg2.HT(mg2,T)) = 0.L by POLYNOM1:17;
then
A52: f.HT(mg2,T) = --(mg2.HT(mg2,T) ) by RLVECT_1:6;
(f-mg1).HT(mg1,T) = 0.L by A15,A16,POLYNOM1:def 4;
then (f+-mg1).HT(mg1,T) = 0.L by POLYNOM1:def 7;
then f.HT(mg1,T) + (-mg1).HT(mg1,T) = 0.L by POLYNOM1:15;
then f.HT(mg1,T) + -(mg1.HT(mg1,T)) = 0.L by POLYNOM1:17;
then
A53: f.HT(mg1,T) = --(mg1.HT(mg1,T) ) by RLVECT_1:6;
HC(mg1,T) = mg1.HT(mg1,T) by TERMORD:def 7
.= f.(HT(mg1,T)) by A53,RLVECT_1:17
.= mg2.HT(mg2,T) by A51,A52,RLVECT_1:17
.= HC(mg2,T) by TERMORD:def 7;
then HM(mg1,T) = Monom(HC(mg2,T),HT(mg2,T)) by A51,
TERMORD:def 8
.= HM(mg2,T) by TERMORD:def 8;
hence thesis by A1,A9,A19,A31,A35;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence b,c are_convergent_wrt R by A24,A14,POLYRED:50,REWRITE1:40;
end;
end;
hence b,c are_convergent_wrt R;
end;
then PolyRedRel(P,T) is locally-confluent by REWRITE1:def 24;
hence thesis by GROEB_1:def 3;
end;
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, p1,p2 be
Polynomial of n,L;
func S-Poly(p1,p2,T) -> Polynomial of n,L equals
HC(p2,T) * (lcm(HT(p1,T),HT
(p2,T))/HT(p1,T)) *' p1 - HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
coherence;
end;
:: definition 5.46, p. 211
Lm2: for L being add-associative left_zeroed right_zeroed add-cancelable
right_complementable associative distributive well-unital non empty
doubleLoopStr, P being Subset of L, p being Element of L st p in P holds p in
P-Ideal
proof
let L be add-associative left_zeroed right_zeroed add-cancelable associative
distributive well-unital right_complementable non empty doubleLoopStr, P be
Subset of L, p be Element of L;
set f = <*p*>;
assume
A1: p in P;
then reconsider P9 = P as non empty Subset of L;
now
let i be set;
assume
A2: i in dom f;
dom f = {1} by FINSEQ_1:2,38;
then i = 1 by A2,TARSKI:def 1;
then f/.i = f.1 by A2,PARTFUN1:def 6
.= p
.= 1.L * p
.= 1.L * p * 1.L;
hence ex u,v being Element of L, a being Element of P9 st f/.i = u*a*v by
A1;
end;
then reconsider f as LinearCombination of P9 by IDEAL_1:def 8;
Sum f = p by RLVECT_1:44;
hence thesis by IDEAL_1:60;
end;
Lm3: for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed well-unital distributive non
trivial doubleLoopStr, p,q being Polynomial of n,L, f,g being Element of
Polynom-Ring(n,L) holds (f = p & g = q) implies f - g = p - q
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed well-unital distributive non trivial
doubleLoopStr, p,q be Polynomial of n,L, f,g be Element of Polynom-Ring(n,L);
assume that
A1: f = p and
A2: g = q;
reconsider x = -q as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
reconsider x as Element of Polynom-Ring(n,L);
x + g = -q + q by A2,POLYNOM1:def 11
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
then
A3: -q = -g by RLVECT_1:6;
thus p - q = p + (-q) by POLYNOM1:def 7
.= f + (-g) by A1,A3,POLYNOM1:def 11
.= f - g;
end;
theorem Th18:
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 Abelian non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), p1,p2 being Polynomial of
n,L st p1 in P & p2 in P holds S-Poly(p1,p2,T) in P-Ideal
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 Abelian non trivial doubleLoopStr, P be
Subset of Polynom-Ring(n,L), p1,p2 be Polynomial of n,L;
assume that
A1: p1 in P and
A2: p2 in P;
set q1 = Monom(HC(p2,T),lcm(HT(p1,T),HT(p2,T))/HT(p1,T)), q2 = Monom(HC(p1,T
),lcm(HT(p1,T),HT(p2,T))/HT(p2,T));
reconsider p19 = p1, p29 = p2 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider p19, p29 as Element of Polynom-Ring(n,L);
reconsider q19 = q1, q29 = q2 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider q19, q29 as Element of Polynom-Ring(n,L);
p29 in P-Ideal by A2,Lm2;
then
A3: q29 * p29 in P-Ideal by IDEAL_1:def 2;
p19 in P-Ideal by A1,Lm2;
then q19 * p19 in P-Ideal by IDEAL_1:def 2;
then
A4: q19 * p19 - q29 * p29 in P-Ideal by A3,IDEAL_1:16;
set q = S-Poly(p1,p2,T);
A5: q1 *' p1 = q19 * p19 & q2 *' p2 = q29 * p29 by POLYNOM1:def 11;
q = q1 *' p1 - HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2 by
POLYRED:22
.= q1 *' p1 - q2 *' p2 by POLYRED:22;
hence thesis by A4,A5,Lm3;
end;
theorem Th19:
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, m1
,m2 being Monomial of n,L holds S-Poly(m1,m2,T) = 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, m1,m2 be
Monomial of n,L;
per cases;
suppose
A1: m1 = 0_(n,L);
A2: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))),T) =
coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T)))) by
TERMORD:23
.= HC(0_(n,L),T) by POLYNOM7:9
.= 0.L by TERMORD:17;
thus S-Poly(m1,m2,T) = Monom(HC(m2,T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T)))
*' 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by A1,
POLYRED:22
.= 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2
by POLYNOM1:28
.= 0_(n,L) - Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *'
m2 by POLYRED:22
.= 0_(n,L) - 0_(n,L) *' m2 by A2,TERMORD:17
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYNOM1:24;
end;
suppose
A3: m2 = 0_(n,L);
A4: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))),T) =
coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T)))) by
TERMORD:23
.= HC(0_(n,L),T) by POLYNOM7:9
.= 0.L by TERMORD:17;
thus S-Poly(m1,m2,T) = HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T))
*' m1 - Monom(HC(m1,T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' 0_(n,L) by A3,
POLYRED:22
.= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 - 0_(n,L)
by POLYNOM1:28
.= Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1 - 0_(n
,L) by POLYRED:22
.= 0_(n,L) *' m1 - 0_(n,L) by A4,TERMORD:17
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYNOM1:24;
end;
suppose
A5: m1 <> 0_(n,L) & m2 <> 0_(n,L);
then HC(m2,T) <> 0.L by TERMORD:17;
then
A6: HC(m2,T) is non zero;
HC(m1,T) <> 0.L by A5,TERMORD:17;
then
A7: HC(m1,T) is non zero;
A8: HT(m2,T) divides lcm(HT(m1,T),HT(m2,T)) by Th3;
A9: m2 = Monom(coefficient(m2),term(m2)) by POLYNOM7:11
.= Monom(HC(m2,T),term(m2)) by TERMORD:23
.= Monom(HC(m2,T),HT(m2,T)) by TERMORD:23;
A10: HT(m1,T) divides lcm(HT(m1,T),HT(m2,T)) by Th3;
A11: m1 = Monom(coefficient(m1),term(m1)) by POLYNOM7:11
.= Monom(HC(m1,T),term(m1)) by TERMORD:23
.= Monom(HC(m1,T),HT(m1,T)) by TERMORD:23;
A12: HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 = Monom(HC(m1,T),(
lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' m2 by POLYRED:22
.= Monom(HC(m2,T)*HC(m1,T), (lcm(HT(m1,T),HT(m2,T))/HT(m2,T))+HT(m2,T)
) by A7,A6,A9,TERMORD:3
.= Monom(HC(m2,T)*HC(m1,T), lcm(HT(m1,T),HT(m2,T))) by A8,Def1;
HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 = Monom(HC(m2,T),(
lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1 by POLYRED:22
.= Monom(HC(m2,T)*HC(m1,T), (lcm(HT(m1,T),HT(m2,T))/HT(m1,T))+HT(m1,T)
) by A7,A6,A11,TERMORD:3
.= Monom(HC(m2,T)*HC(m1,T), lcm(HT(m1,T),HT(m2,T))) by A10,Def1;
hence thesis by A12,POLYNOM1:24;
end;
end;
:: exercise 5.47 (i), p. 211
theorem Th20:
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 S-Poly(p,0_(n,L),T) = 0_(n,L) & S-Poly(0_(n,L),p,
T) = 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, p be
Polynomial of n,L;
set p2 = 0_(n,L);
thus S-Poly(p,0_(n,L),T) = HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T))
*' p - Monom(HC(p,T),lcm(HT(p,T),HT(p2,T))/HT(p2,T)) *' 0_(n,L) by POLYRED:22
.= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p - 0_(n,L) by
POLYNOM1:28
.= 0.L * ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p) - 0_(n,L) by TERMORD:17
.= ((0.L |(n,L)) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L) by
POLYNOM7:27
.= (0_(n,L) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L) by
POLYNOM7:19
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYRED:4;
thus S-Poly(0_(n,L),p,T) = Monom(HC(p,T),(lcm(HT(p2,T),HT(p,T))/HT(p2,T)))
*' 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by POLYRED:22
.= 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by
POLYNOM1:28
.= 0_(n,L) - 0.L * ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p) by TERMORD:17
.= 0_(n,L) - ((0.L |(n,L)) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p)) by
POLYNOM7:27
.= 0_(n,L) - (0_(n,L) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p)) by
POLYNOM7:19
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYRED:4;
end;
theorem
for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 being Polynomial of n,L holds S-Poly(p1,p2,T) = 0_(n,L) or HT(S-Poly(p1,p2,
T),T) < lcm(HT(p1,T),HT(p2,T)),T
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 almost_left_invertible non trivial doubleLoopStr, p1
,p2 be Polynomial of n,L;
assume
A1: S-Poly(p1,p2,T) <> 0_(n,L);
set sp = S-Poly(p1,p2,T), g1 = HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T))
*' p1, g2 = HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
per cases;
suppose
p1 = 0_(n,L) or p2 = 0_(n,L);
hence thesis by A1,Th20;
end;
suppose
A2: p1 <> 0_(n,L) & p2 <> 0_(n,L);
then
A3: HC(p2,T) <> 0.L by TERMORD:17;
then
A4: HC(p2,T) is non zero;
A5: HT(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T) = term(Monom(
HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) by TERMORD:23
.= lcm(HT(p1,T),HT(p2,T))/HT(p1,T) by A4,POLYNOM7:10;
A6: p1 is non-zero by A2,POLYNOM7:def 1;
HC(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T) = coefficient
(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) by TERMORD:23
.= HC(p2,T) by POLYNOM7:9;
then Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) <> 0_(n,L) by A3,
TERMORD:17;
then
A7: Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) is non-zero by
POLYNOM7:def 1;
A8: HC(g1,T) = HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *'
p1,T) by POLYRED:22
.= HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) * HC(p1,T
) by A6,A7,TERMORD:32
.= coefficient(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) * HC
(p1,T) by TERMORD:23
.= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
A9: HT(p1,T) divides lcm(HT(p1,T),HT(p2,T)) by Th3;
A10: HT(g1,T) = HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *'
p1,T) by POLYRED:22
.= HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) + HT(p1,T
) by A6,A7,TERMORD:31
.= lcm(HT(p1,T),HT(p2,T)) by A9,A5,Def1;
A11: HC(p1,T) <> 0.L by A2,TERMORD:17;
then
A12: HC(p1,T) is non zero;
A13: HT(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T) = term(Monom(
HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) by TERMORD:23
.= lcm(HT(p1,T),HT(p2,T))/HT(p2,T) by A12,POLYNOM7:10;
A14: p2 is non-zero by A2,POLYNOM7:def 1;
HC(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T) = coefficient
(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) by TERMORD:23
.= HC(p1,T) by POLYNOM7:9;
then Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) <> 0_(n,L) by A11,
TERMORD:17;
then
A15: Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) is non-zero by
POLYNOM7:def 1;
Support sp <> {} by A1,POLYNOM7:1;
then
A16: HT(sp,T) in Support sp by TERMORD:def 6;
A17: HT(p2,T) divides lcm(HT(p1,T),HT(p2,T)) by Th3;
A18: HC(g2,T) = HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *'
p2,T) by POLYRED:22
.= HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) * HC(p2,T
) by A14,A15,TERMORD:32
.= coefficient(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) * HC
(p2,T) by TERMORD:23
.= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
A19: HT(g2,T) = HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *'
p2,T) by POLYRED:22
.= HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) + HT(p2,T
) by A14,A15,TERMORD:31
.= lcm(HT(p1,T),HT(p2,T)) by A17,A13,Def1;
then sp.(lcm(HT(p1,T),HT(p2,T))) = (g1+-g2).HT(g2,T) by POLYNOM1:def 7
.= g1.HT(g2,T) + (-g2).HT(g2,T) by POLYNOM1:15
.= g1.HT(g2,T) + -(g2.HT(g2,T)) by POLYNOM1:17
.= HC(g1,T) + -(g2.HT(g2,T)) by A10,A19,TERMORD:def 7
.= HC(g1,T) + -HC(g2,T) by TERMORD:def 7
.= 0.L by A8,A18,RLVECT_1:5;
then
A20: not lcm(HT(p1,T),HT(p2,T)) in Support sp by POLYNOM1:def 4;
HT(sp,T) <= max(HT(g1,T),HT(g2,T),T), T by GROEB_1:7;
then HT(sp,T) <= lcm(HT(p1,T),HT(p2,T)),T by A10,A19,TERMORD:12;
hence thesis by A16,A20,TERMORD:def 3;
end;
end;
:: exercise 5.47 (ii), p. 211
theorem
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, p1
,p2 being non-zero Polynomial of n,L holds HT(p2,T) divides HT(p1,T) implies HC
(p2,T) * p1 top_reduces_to S-Poly(p1,p2,T),p2,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, p1,p2 be
non-zero Polynomial of n,L;
set hcp2 = HC(p2,T);
assume
A1: HT(p2,T) divides HT(p1,T);
then consider b being bag of n such that
A2: HT(p1,T) = HT(p2,T) + b by TERMORD:1;
set g = (hcp2*p1) - ((hcp2*p1).HT(p1,T)/HC(p2,T)) * (b *' p2);
A3: p2 <> 0_(n,L) by POLYNOM7:def 1;
A4: hcp2 <> 0.L;
p1 <> 0_(n,L) by POLYNOM7:def 1;
then Support p1 <> {} by POLYNOM7:1;
then
A5: HT(p1,T) in Support p1 by TERMORD:def 6;
A6: Support(p1) c= Support(hcp2*p1) by POLYRED:20;
then hcp2*p1 <> 0_(n,L) by A5,POLYNOM7:1;
then
A7: HT(hcp2*p1,T) = HT(p1,T) & hcp2*p1 reduces_to g,p2,HT(p1,T),T by A3,A5,A2
,A6,POLYRED:21,def 5;
A8: lcm(HT(p1,T),HT(p2,T)) = HT(p1,T) by A1,Th7;
g = (hcp2*p1) - (hcp2*(p1.HT(p1,T))/HC(p2,T)) * (b *' p2) by POLYNOM7:def 9
.= (hcp2*p1) - ((hcp2*HC(p1,T))/HC(p2,T)) * (b *' p2) by TERMORD:def 7
.= (hcp2*p1) - ((hcp2*HC(p1,T))*(HC(p2,T)")) * (b *' p2)
.= (hcp2*p1) - (HC(p1,T)*(hcp2*(HC(p2,T)"))) * (b *' p2) by GROUP_1:def 3
.= (hcp2*p1) - (HC(p1,T)*1.L) * (b *' p2) by A4,VECTSP_1:def 10
.= (hcp2*p1) - HC(p1,T) * (b *' p2)
.= HC(p2,T) * (EmptyBag n) *' p1 - HC(p1,T) * (b *' p2) by POLYRED:17
.= HC(p2,T) * (HT(p1,T)/HT(p1,T)) *' p1 - HC(p1,T) * (b *' p2) by Th6
.= S-Poly(p1,p2,T) by A1,A2,A8,Def1;
hence thesis by A7,POLYRED:def 10;
end;
:: exercise 5.47 (iii), p. 211
theorem
for n being Element of NAT, T being connected admissible 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, G being Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T implies (for g1,g2,h being Polynomial of n,L st
g1 in G & g2 in G & h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) holds
h = 0_(n,L))
proof
let n be Element of NAT, T be connected admissible 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, G be Subset of Polynom-Ring(n,L);
assume
A1: G is_Groebner_basis_wrt T;
set R = PolyRedRel(G,T);
A2: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
per cases;
suppose
G = {};
hence thesis;
end;
suppose
G <> {};
then reconsider G as non empty Subset of Polynom-Ring(n,L);
A3: R is locally-confluent by A1,GROEB_1:def 3;
now
A4: now
assume not 0_(n,L) is_a_normal_form_wrt R;
then consider b being object such that
A5: [0_(n,L),b] in R by REWRITE1:def 5;
consider f1,f2 being object such that
A6: f1 in NonZero Polynom-Ring(n,L) and
f2 in the carrier of Polynom-Ring(n,L) and
A7: [0_(n,L),b] = [f1,f2] by A5,ZFMISC_1:def 2;
A8: f1 = 0_(n,L) by A7,XTUPLE_0:1;
not f1 in {0_(n,L)} by A2,A6,XBOOLE_0:def 5;
hence contradiction by A8,TARSKI:def 1;
end;
let g1,g2,h being Polynomial of n,L;
assume that
A9: g1 in G & g2 in G and
A10: h is_a_normal_form_of S-Poly(g1,g2,T),R;
S-Poly(g1,g2,T) in G-Ideal by A9,Th18;
then R reduces S-Poly(g1,g2,T),0_(n,L) by A3,GROEB_1:15;
then
A11: S-Poly(g1,g2,T),0_(n,L) are_convertible_wrt R by REWRITE1:25;
R reduces S-Poly(g1,g2,T),h by A10,REWRITE1:def 6;
then h,S-Poly(g1,g2,T) are_convertible_wrt R by REWRITE1:25;
then
A12: h,0_(n,L) are_convertible_wrt R by A11,REWRITE1:30;
h is_a_normal_form_wrt R by A10,REWRITE1:def 6;
hence h = 0_(n,L) by A3,A4,A12,REWRITE1:def 19;
end;
hence thesis;
end;
end;
:: theorem 5.48 (i) ==> (ii), p. 211
theorem
for n being Element of NAT, 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, G being Subset of Polynom-Ring(n,L)
holds (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in G & h
is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) holds h = 0_(n,L)) implies
(for g1,g2 being Polynomial of n,L st g1 in G & g2 in G holds PolyRedRel(G,T)
reduces S-Poly(g1,g2,T),0_(n,L))
proof
let n be Element of 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, G be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(G,T);
assume
A1: for g1,g2,h being Polynomial of n,L st g1 in G & g2 in G & h
is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) holds h = 0_(n,L);
now
let g1,g2 be Polynomial of n,L;
now
per cases;
case
S-Poly(g1,g2,T) in field R;
hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:def 14;
end;
case
not S-Poly(g1,g2,T) in field R;
hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:46;
end;
end;
then consider q being object such that
A2: q is_a_normal_form_of S-Poly(g1,g2,T),R by REWRITE1:def 11;
R reduces S-Poly(g1,g2,T),q by A2,REWRITE1:def 6;
then reconsider q as Polynomial of n,L by Lm1;
assume g1 in G & g2 in G;
then q = 0_(n,L) by A1,A2;
hence R reduces S-Poly(g1,g2,T),0_(n,L) by A2,REWRITE1:def 6;
end;
hence thesis;
end;
:: theorem 5.48 (ii) ==> (iii), p. 211
theorem Th25:
for n being Element of NAT, 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, G being Subset of Polynom-Ring(n,L)
st not(0_(n,L) in G) holds (for g1,g2 being Polynomial of n,L st g1 in G & g2
in G holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L)) implies G
is_Groebner_basis_wrt T
proof
let n be Element of NAT, 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, G be Subset of Polynom-Ring(n,L);
assume
A1: not 0_(n,L) in G;
assume
A2: for g1,g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L);
now
let g1,g2 be Polynomial of n,L;
assume that
g1 <> g2 and
A3: g1 in G and
A4: g2 in G;
thus for m1,m2 being Monomial of n,L st HM(m1 *'g1,T) = HM(m2 *'g2,T)
holds PolyRedRel(G,T) reduces m1 *' g1 - m2 *' g2, 0_(n,L)
proof
set a1 = HC(g1,T), a2 = HC(g2,T);
set t1 = HT(g1,T), t2 = HT(g2,T);
let m1,m2 be Monomial of n,L;
assume
A5: HM(m1 *'g1,T) = HM(m2 *'g2,T);
A6: a2 <> 0.L by A1,A4,TERMORD:17;
reconsider g1,g2 as non-zero Polynomial of n,L by A1,A3,A4,POLYNOM7:def 1
;
set b1 = coefficient(m1), b2 = coefficient(m2);
set u1 = term(m1), u2 = term(m2);
A7: a1 <> 0.L by A1,A3,TERMORD:17;
then reconsider a1,a2 as non zero Element of L by A6,STRUCT_0:def 12;
A8: HC(m1*'g1,T) = coefficient(HM(m1*'g1,T)) by TERMORD:22
.= HC(m2*'g2,T) by A5,TERMORD:22;
now
per cases;
case
A9: b1 = 0.L or b2 = 0.L;
now
per cases by A9;
case
b1 = 0.L;
then HC(m1,T) = 0.L by TERMORD:23;
then m1 = 0_(n,L) by TERMORD:17;
then
A10: m1 *' g1 = 0_(n,L) by POLYRED:5;
then HC(m2*'g2,T) = 0.L by A8,TERMORD:17;
then m2 *' g2 = 0_(n,L) by TERMORD:17;
then m1 *' g1 - m2 *' g2 = 0_(n,L) by A10,POLYRED:4;
hence thesis by REWRITE1:12;
end;
case
b2 = 0.L;
then HC(m2,T) = 0.L by TERMORD:23;
then m2 = 0_(n,L) by TERMORD:17;
then
A11: m2 *' g2 = 0_(n,L) by POLYRED:5;
then HC(m1*'g1,T) = 0.L by A8,TERMORD:17;
then m1 *' g1 = 0_(n,L) by TERMORD:17;
then m1 *' g1 - m2 *' g2 = 0_(n,L) by A11,POLYRED:4;
hence thesis by REWRITE1:12;
end;
end;
hence thesis;
end;
case
A12: b1 <> 0.L & b2 <> 0.L;
then reconsider b1,b2 as non zero Element of L by STRUCT_0:def 12;
b2 * a2 <> 0.L by VECTSP_2:def 1;
then
A13: b2 * a2 is non zero;
t1 divides lcm(t1,t2) by Th3;
then consider s1 being bag of n such that
A14: t1 + s1 = lcm(t1,t2) by TERMORD:1;
HC(m2,T) <> 0.L by A12,TERMORD:23;
then
A15: m2 <> 0_(n,L) by TERMORD:17;
HC(m1,T) <> 0.L by A12,TERMORD:23;
then m1 <> 0_(n,L) by TERMORD:17;
then reconsider m1,m2 as non-zero Monomial of n,L by A15,
POLYNOM7:def 1;
A16: Monom(b1*a1,u1+t1) = Monom(b1,u1) *' Monom(a1,t1) by TERMORD:3
.= m1 *' Monom(a1,t1) by POLYNOM7:11
.= HM(m1,T) *' Monom(a1,t1) by TERMORD:23
.= HM(m1,T) *' HM(g1,T) by TERMORD:def 8
.= HM(m2*'g2,T) by A5,TERMORD:33
.= HM(m2,T) *' HM(g2,T) by TERMORD:33
.= HM(m2,T) *' Monom(a2,t2) by TERMORD:def 8
.= m2 *' Monom(a2,t2) by TERMORD:23
.= Monom(b2,u2) *' Monom(a2,t2) by POLYNOM7:11
.= Monom(b2*a2,u2+t2) by TERMORD:3;
then b1*a1 = coefficient(Monom(b2*a2,u2+t2)) by POLYNOM7:9
.= b2 * a2 by POLYNOM7:9;
then (b1 * a1) / a2 = (b2 * a2) * a2"
.= b2 * (a2 * a2") by GROUP_1:def 3
.= b2 * 1.L by A6,VECTSP_1:def 10;
then
A17: b2 / a1 = ((b1 * a1) / a2) / a1
.= ((b1 * a1) * a2") / a1
.= ((b1 * a1) * a2") * a1"
.= ((b1 * a2") * a1) * a1" by GROUP_1:def 3
.= (b1 * a2") * (a1 * a1") by GROUP_1:def 3
.= (b1 * a2") * 1.L by A7,VECTSP_1:def 10
.= b1 * a2"
.= b1 / a2;
b1 * a1 <> 0.L by VECTSP_2:def 1;
then b1 * a1 is non zero;
then
A18: u1 + t1 = term(Monom(b2*a2,u2+t2)) by A16,POLYNOM7:10
.= u2 + t2 by A13,POLYNOM7:10;
then t1 divides u1 + t1 & t2 divides u1 + t1 by TERMORD:1;
then lcm(t1,t2) divides u1 + t1 by Th4;
then consider v being bag of n such that
A19: u1 + t1 = lcm(t1,t2) + v by TERMORD:1;
u1 + t1 = (v + s1) + t1 by A14,A19,PRE_POLY:35;
then
A20: u1 = ((v + s1) + t1) -' t1 by PRE_POLY:48
.= v + s1 by PRE_POLY:48;
t2 divides lcm(t1,t2) by Th3;
then consider s2 being bag of n such that
A21: t2 + s2 = lcm(t1,t2) by TERMORD:1;
u2 + t2 = (v + s2) + t2 by A18,A21,A19,PRE_POLY:35;
then
A22: u2 = ((v + s2) + t2) -' t2 by PRE_POLY:48
.= v + s2 by PRE_POLY:48;
HT(g2,T) divides lcm(HT(g1,T),HT(g2,T)) by Th3;
then
A23: s2 = lcm(HT(g1,T),HT(g2,T))/HT(g2,T) by A21,Def1;
A24: (b2/a1)*a1 = (b2*a1")*a1
.= b2*(a1"*a1) by GROUP_1:def 3
.= b2*1.L by A7,VECTSP_1:def 10
.= b2;
HT(g1,T) divides lcm(HT(g1,T),HT(g2,T)) by Th3;
then
A25: s1 = lcm(HT(g1,T),HT(g2,T))/HT(g1,T) by A14,Def1;
A26: (b1/a2)*a2 = (b1*a2")*a2
.= b1*(a2"*a2) by GROUP_1:def 3
.= b1*1.L by A6,VECTSP_1:def 10;
m1 *' g1 - m2 *' g2 = Monom(b1,u1) *' g1 - m2 *' g2 by POLYNOM7:11
.= Monom(b1,u1) *' g1 - Monom(b2,u2) *' g2 by POLYNOM7:11
.= b1 * ((v+s1) *' g1) - Monom(b2,v+s2) *' g2 by A20,A22,POLYRED:22
.= b1 * (v *' (s1 *' g1)) - Monom(b2,v+s2) *' g2 by POLYRED:18
.= b1 * (v *' (s1 *' g1)) - b2 * ((v+s2) *' g2) by POLYRED:22
.= b1 * (v *' (s1 *' g1)) - b2 * (v *' (s2 *' g2)) by POLYRED:18
.= b1 * (v *' (s1 *' g1)) + -(b2 * (v *' (s2 *' g2))) by
POLYNOM1:def 7
.= b1 * (v *' (s1 *' g1)) + b2 * (-(v *' (s2 *' g2))) by POLYRED:9
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (-(v*'(s2*'
g2))) by A26,A24
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (v*'(-(s2*'
g2))) by Th13
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + (b1/a2) * (a1 * (v*'-(s2*'g2
))) by A17,POLYRED:11
.= (b1/a2) * (a2 * (v*'(s1*'g1))) + (b1/a2) * (a1 * (v*'-(s2*'g2
))) by POLYRED:11
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + a1 * (v*'-(s2*'g2))) by Th15
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (a1*(-(s2*'g2)))) by Th14
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by
POLYRED:9
.= (b1/a2) * (v *' (a2*(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by Th14
.= (b1/a2) * (v *' (a2*(s1*'g1) + (-(a1*(s2*'g2))))) by Th12
.= (b1/a2) * v *' S-Poly(g1,g2,T) by A25,A23,POLYNOM1:def 7
.= Monom(b1/a2,v) *' S-Poly(g1,g2,T) by POLYRED:22;
hence thesis by A2,A3,A4,POLYRED:48;
end;
end;
hence thesis;
end;
end;
hence thesis by Th17;
end;
:: theorem 5.48 (iii) ==> (i), p. 211
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 S-Poly(P,T) -> Subset of Polynom-Ring(n,L) equals
{ S-Poly(p1,p2,T)
where p1,p2 is Polynomial of n,L : p1 in P & p2 in P };
coherence
proof
set M = {S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L : p1 in P & p2
in P};
now
let u be object;
assume u in M;
then ex p1,p2 being Polynomial of n,L st u = S-Poly(p1,p2,T) & p1 in P &
p2 in P;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
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 finite
Subset of Polynom-Ring(n,L);
cluster S-Poly(P,T) -> finite;
coherence
proof
defpred P[object,object] means
ex p1,p2 being Polynomial of n,L st p1 = $1`1 &
$1`2 = p2 & p1 in P & p2 in P & $2 = S-Poly(p1,p2,T);
A1: for x being object st x in [:P,P:] ex y being object st P[x,y]
proof
let x be object;
assume x in [:P,P:];
then consider p1,p2 being object such that
A2: p1 in P & p2 in P and
A3: [p1,p2] = x by ZFMISC_1:def 2;
reconsider p1,p2 as Polynomial of n,L by A2,POLYNOM1:def 11;
take S-Poly(p1,p2,T);
take p1,p2;
thus x`1 = p1 by A3;
thus x`2 = p2 by A3;
thus thesis by A2;
end;
consider f being Function such that
A4: dom f = [:P,P:] & for x being object st x in [:P,P:] holds P[x,f.x]
from CLASSES1:sch 1(A1);
A5: now
let v be object;
assume v in S-Poly(P,T);
then consider p1,p2 being Polynomial of n,L such that
A6: v = S-Poly(p1,p2,T) and
A7: p1 in P & p2 in P;
A8: [p1,p2] in dom f by A4,A7,ZFMISC_1:def 2;
then consider p19,p29 being Polynomial of n,L such that
A9: [p1,p2]`1 = p19 & [p1,p2]`2 = p29 and
p19 in P and
p29 in P and
A10: f.[p1,p2] = S-Poly(p19,p29,T) by A4;
p1 = p19 & p2 = p29 by A9;
hence v in rng f by A6,A8,A10,FUNCT_1:def 3;
end;
now
let v be object;
assume v in rng f;
then consider u being object such that
A11: u in dom f and
A12: v = f.u by FUNCT_1:def 3;
ex p1,p2 being Polynomial of n,L st p1 = u`1 & u`2 = p2 & p1 in P &
p2 in P & f.u = S-Poly(p1,p2,T) by A4,A11;
hence v in S-Poly(P,T) by A12;
end;
then rng f = S-Poly(P,T) by A5,TARSKI:2;
hence thesis by A4,FINSET_1:8;
end;
end;
theorem
for n being Element of NAT, 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, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) & for g being Polynomial of n,L st g in G holds g is Monomial
of n,L holds G is_Groebner_basis_wrt T
proof
let n being Element of NAT, 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, G being Subset of Polynom-Ring(n,L);
assume that
A1: not 0_(n,L) in G and
A2: for g being Polynomial of n,L st g in G holds g is Monomial of n,L;
now
let g1,g2 be Polynomial of n,L;
assume g1 in G & g2 in G;
then g1 is Monomial of n,L & g2 is Monomial of n,L by A2;
then S-Poly(g1,g2,T) = 0_(n,L) by Th19;
hence PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L) by REWRITE1:12;
end;
hence thesis by A1,Th25;
end;
:: corollary 5.49, p. 212
begin :: Standard Representations
theorem
for L being non empty multLoopStr, P being non empty Subset of L, A
being LeftLinearCombination of P, i being Element of NAT holds A|i is
LeftLinearCombination of P
proof
let L be non empty multLoopStr, P be non empty Subset of L, A be
LeftLinearCombination of P, j be Element of NAT;
set C = A|(Seg j);
reconsider C as FinSequence of the carrier of L by FINSEQ_1:18;
now
let i be set;
A1: dom C c= dom A by RELAT_1:60;
assume
A2: i in dom C;
then C.i = A.i by FUNCT_1:47;
then C/.i = A.i by A2,PARTFUN1:def 6
.= A/.i by A2,A1,PARTFUN1:def 6;
hence ex u being Element of L, a being Element of P st C/.i = u * a by A2
,A1,IDEAL_1:def 9;
end;
then C is LeftLinearCombination of P by IDEAL_1:def 9;
hence thesis by FINSEQ_1:def 16;
end;
theorem
for L being non empty multLoopStr, P being non empty Subset of L, A
being LeftLinearCombination of P, i being Element of NAT holds A/^i is
LeftLinearCombination of P
proof
let L be non empty multLoopStr, P be non empty Subset of L, A be
LeftLinearCombination of P, j be Element of NAT;
set C = A/^j;
reconsider C as FinSequence of the carrier of L;
now
per cases;
case
A1: j <= len A;
then reconsider m = len A - j as Element of NAT by INT_1:5;
now
let i be set;
assume
A2: i in dom C;
then reconsider k = i as Element of NAT;
A3: dom C = Seg(len C) by FINSEQ_1:def 3
.= Seg(m) by A1,RFINSEQ:def 1;
then k <= len A - j by A2,FINSEQ_1:1;
then
A4: k + j <= (len A + -j) + j by XREAL_1:6;
A5: k <= k + j by NAT_1:11;
1 <= k by A2,A3,FINSEQ_1:1;
then 1 <= k + j by A5,XXREAL_0:2;
then j + k in Seg(len A) by A4,FINSEQ_1:1;
then j + k in dom A by FINSEQ_1:def 3;
then ex u being Element of L, a being Element of P st A/.(j+k) = u * a
by IDEAL_1:def 9;
hence ex u being Element of L, a being Element of P st C/.i = u * a by
A2,FINSEQ_5:27;
end;
hence thesis by IDEAL_1:def 9;
end;
case
not j <= len A;
then C = <*>(the carrier of L) by RFINSEQ:def 1;
then for i being set st i in dom C ex u being Element of L, a being
Element of P st C/.i = u * a;
hence thesis by IDEAL_1:def 9;
end;
end;
hence thesis;
end;
theorem
for L being non empty multLoopStr, P,Q being non empty Subset of L, A
being LeftLinearCombination of P holds P c= Q implies A is
LeftLinearCombination of Q
proof
let L be non empty multLoopStr, P,Q be non empty Subset of L, A be
LeftLinearCombination of P;
assume
A1: P c= Q;
now
let i be set;
assume i in dom A;
then consider u being Element of L, a being Element of P such that
A2: A/.i = u*a by IDEAL_1:def 9;
a in P;
hence ex u being Element of L, a being Element of Q st A/.i = u*a by A1,A2;
end;
hence thesis by IDEAL_1:def 9;
end;
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, P be non empty
Subset of Polynom-Ring(n,L), A,B be LeftLinearCombination of P;
redefine func A^B -> LeftLinearCombination of P; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
A^B is LeftLinearCombination of P \/ P;
hence thesis;
end;
end;
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, f be Polynomial
of n,L, P be non empty Subset of Polynom-Ring(n,L), A be LeftLinearCombination
of P;
pred A is_MonomialRepresentation_of f means
Sum A = f & for i being
Element of NAT st i in dom A ex m being Monomial of n,L, p being Polynomial of
n,L st p in P & A/.i = m *' p;
end;
theorem
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, f being Polynomial of n,L, P being non empty Subset of
Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_MonomialRepresentation_of f holds Support f c= union { Support(m*'p) where m
is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st i in
dom A & A/.i = m*'p }
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, f be Polynomial
of n,L, P be non empty Subset of Polynom-Ring(n,L), A be LeftLinearCombination
of P;
assume
A1: A is_MonomialRepresentation_of f;
defpred P[Nat] means for f being Polynomial of n,L, A being
LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = $1
holds Support f c= union {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p};
A2: ex n being Element of NAT st len A = n;
A3: now
let k be Nat;
assume
A4: P[k];
for f being Polynomial of n,L, A being LeftLinearCombination of P st
A is_MonomialRepresentation_of f & len A = k+1 holds Support f c= union {
Support(m*'p) where m is Monomial of n,L, p is Polynomial of n,L : ex i being
Element of NAT st i in dom A & A/.i = m*'p}
proof
A5: k <= k + 1 by NAT_1:11;
let f be Polynomial of n,L, A be LeftLinearCombination of P;
assume that
A6: A is_MonomialRepresentation_of f and
A7: len A = k+1;
A8: A <> <*>(the carrier of Polynom-Ring(n,L)) by A7;
A9: Sum A = f by A6;
reconsider A as non empty LeftLinearCombination of P by A8;
consider A9 being LeftLinearCombination of P, e being Element of
Polynom-Ring(n,L) such that
A10: A = A9^<* e *> and
<*e*> is LeftLinearCombination of P by IDEAL_1:33;
A11: dom A = Seg(k+1) by A7,FINSEQ_1:def 3;
reconsider ep = Sum(<*e*>) as Polynomial of n,L by POLYNOM1:def 11;
reconsider g = Sum A9 as Polynomial of n,L by POLYNOM1:def 11;
f = Sum A9 + Sum(<*e*>) by A9,A10,RLVECT_1:41
.= g + ep by POLYNOM1:def 11;
then
A12: Support f c= Support g \/ Support ep by POLYNOM1:20;
A13: len A = len A9 + len<*e*> by A10,FINSEQ_1:22
.= len A9 + 1 by FINSEQ_1:39;
then dom A9 = Seg k by A7,FINSEQ_1:def 3;
then
A14: dom A9 c= dom A by A11,A5,FINSEQ_1:5;
now
let i being Element of NAT;
assume
A15: i in dom A9;
then A/.i = A.i by A14,PARTFUN1:def 6
.= A9.i by A10,A15,FINSEQ_1:def 7
.= A9/.i by A15,PARTFUN1:def 6;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P &
A9/.i = m*'p by A6,A14,A15;
end;
then A9 is_MonomialRepresentation_of g;
then
A16: Support g c= union {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A9 & A9/.i = m*'p}
by A4,A7,A13;
now
let x be object;
assume
A17: x in Support f;
then reconsider u = x as Element of Bags n;
now
per cases by A12,A17,XBOOLE_0:def 3;
case
u in Support g;
then consider Y being set such that
A18: u in Y and
A19: Y in {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A9 & A9/.i = m*'p}
by A16,TARSKI:def 4;
consider m9 being Monomial of n,L, p9 being Polynomial of n,L such
that
A20: Y = Support(m9*'p9) and
A21: ex i being Element of NAT st i in dom A9 & A9/.i = m9*'p9 by A19;
consider i being Element of NAT such that
A22: i in dom A9 and
A23: A9/.i = m9*'p9 by A21;
A/.i = A.i by A14,A22,PARTFUN1:def 6
.= A9.i by A10,A22,FINSEQ_1:def 7
.= A9/.i by A22,PARTFUN1:def 6;
then Y in {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p} by
A14,A20,A22,A23;
hence u in union {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p} by
A18,TARSKI:def 4;
end;
case
A24: u in Support ep;
1 <= len A by A7,NAT_1:11;
then
A25: len A in Seg(len A) by FINSEQ_1:1;
dom A = Seg(len A) by FINSEQ_1:def 3;
then
A26: ex m9 being Monomial of n,L, p9 being Polynomial of n,L st p9
in P & A/.(len A) = m9 *' p9 by A6,A25;
A27: A.(len A) = e & e = Sum(<*e*>) by A10,A13,FINSEQ_1:42,RLVECT_1:44;
A28: len A in dom A by A25,FINSEQ_1:def 3;
then A/.(len A) = A.(len A) by PARTFUN1:def 6;
then
Support ep in {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p} by
A28,A26,A27;
hence u in union {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p} by
A24,TARSKI:def 4;
end;
end;
hence x in union {Support(m*'p) where m is Monomial of n,L, p is
Polynomial of n,L : ex i being Element of NAT st i in dom A & A/.i = m*'p};
end;
hence thesis by TARSKI:def 3;
end;
hence P[k+1];
end;
A29: P[ 0 ]
proof
let f be Polynomial of n,L, A be LeftLinearCombination of P;
assume that
A30: A is_MonomialRepresentation_of f and
A31: len A = 0;
A = <*>(the carrier of Polynom-Ring(n,L)) by A31;
then Sum A = 0.(Polynom-Ring(n,L)) by RLVECT_1:43;
then f = 0.(Polynom-Ring(n,L)) by A30;
then f = 0_(n,L) by POLYNOM1:def 11;
then Support f = {} by POLYNOM7:1;
hence thesis by XBOOLE_1:2;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A29,A3);
hence thesis by A1,A2;
end;
theorem
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, f,g being Polynomial of n,L, P being non empty Subset of
Polynom-Ring(n,L), A,B being LeftLinearCombination of P st A
is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds (A^B)
is_MonomialRepresentation_of f+g
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, f,g be
Polynomial of n,L, P be non empty Subset of Polynom-Ring(n,L), A,B be
LeftLinearCombination of P;
assume that
A1: A is_MonomialRepresentation_of f and
A2: B is_MonomialRepresentation_of g;
A3: now
let i be Element of NAT;
assume
A4: i in dom(A^B);
now
per cases by A4,FINSEQ_1:25;
case
A5: i in dom A;
dom A c= dom(A^B) by FINSEQ_1:26;
then (A^B)/.i = (A^B).i by A5,PARTFUN1:def 6
.= A.i by A5,FINSEQ_1:def 7
.= A/.i by A5,PARTFUN1:def 6;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P &
(A^B)/.i = m *' p by A1,A5;
end;
case
ex k being Nat st k in dom B & i = len A + k;
then consider k being Nat such that
A6: k in dom B and
A7: i = len A + k;
i in dom(A^B) by A6,A7,FINSEQ_1:28;
then (A^B)/.i = (A^B).i by PARTFUN1:def 6
.= B.k by A6,A7,FINSEQ_1:def 7
.= B/.k by A6,PARTFUN1:def 6;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P &
(A^B)/.i = m *' p by A2,A6;
end;
end;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P & (A^
B)/.i = m *' p;
end;
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);
Sum(A^B) = Sum A + Sum B by RLVECT_1:41
.= f9 + Sum B by A1
.= f9 + g9 by A2
.= f + g by POLYNOM1:def 11;
hence thesis by A3;
end;
Lm4: for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being Polynomial of n,L, P being non empty
Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_MonomialRepresentation_of f for b being bag of n holds (for i being Element
of NAT st i in dom A for m being Monomial of n,L, p being Polynomial of n,L st
A.i = m *' p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P;
assume
A1: A is_MonomialRepresentation_of f;
let b be bag of n;
assume
A2: for i being Element of NAT st i in dom A for m being Monomial of n,L
, p being Polynomial of n,L st A.i = m *' p & p in P holds (m*'p).b = 0.L;
defpred P[Nat] means for f being Polynomial of n,L, A being
LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum(A) &
len A = $1 holds (for i being Element of NAT st i in dom A for m being Monomial
of n,L, p being Polynomial of n,L st A.i = m*'p & p in P holds (m*'p).b = 0.L)
implies f.b = 0.L;
A3: now
let k be Nat;
assume
A4: P[k];
for f being Polynomial of n,L, A being LeftLinearCombination of P st A
is_MonomialRepresentation_of f & f = Sum(A) & len A = k+1 holds (for i being
Element of NAT st i in dom A for m being Monomial of n,L, p being Polynomial of
n,L st A.i = m*'p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L
proof
let f be Polynomial of n,L, A be LeftLinearCombination of P;
assume that
A5: A is_MonomialRepresentation_of f and
A6: f = Sum(A) and
A7: len A = k+1;
set B = A|(Seg k);
reconsider B as FinSequence of Polynom-Ring(n,L) by FINSEQ_1:18;
reconsider B as LeftLinearCombination of P by IDEAL_1:42;
set g = Sum B;
reconsider g as Polynomial of n,L by POLYNOM1:def 11;
A8: dom A = Seg(k+1) by A7,FINSEQ_1:def 3;
then k + 1 in dom A by FINSEQ_1:4;
then
A9: ex m being Monomial of n,L, p being Polynomial of n,L st p in P & A
/.(k+1) = m *' p by A5;
A10: k <= len A by A7,NAT_1:11;
then k <= k + 1 & dom B = Seg(k) by FINSEQ_1:17,NAT_1:11;
then
A11: dom B c= dom A by A8,FINSEQ_1:5;
now
let i be Element of NAT;
assume
A12: i in dom B;
then B/.i = B.i by PARTFUN1:def 6
.= A.i by A12,FUNCT_1:47
.= A/.i by A11,A12,PARTFUN1:def 6;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P &
B/.i = m *' p by A5,A11,A12;
end;
then
A13: B is_MonomialRepresentation_of g;
assume
A14: for i being Element of NAT st i in dom A for m being Monomial
of n,L, p being Polynomial of n,L st A.i = m*'p & p in P holds (m*'p).b = 0.L;
A15: now
let i be Element of NAT;
assume
A16: i in dom B;
now
let m be Monomial of n,L, p be Polynomial of n,L;
assume that
A17: B.i = m*'p and
A18: p in P;
A.i = m*'p by A16,A17,FUNCT_1:47;
hence (m*'p).b = 0.L by A14,A11,A16,A18;
end;
hence
for m being Monomial of n,L, p being Polynomial of n,L st B.i = m
*'p & p in P holds (m*'p).b = 0.L;
end;
reconsider h = A/.(k+1) as Polynomial of n,L by POLYNOM1:def 11;
B^<*A/.(k+1)*> = B^<*A.(k+1)*> by A8,FINSEQ_1:4,PARTFUN1:def 6
.= A by A7,FINSEQ_3:55;
then f = Sum(B) + Sum(<*A/.(k+1)*>) by A6,RLVECT_1:41
.= Sum B + A/.(k+1) by RLVECT_1:44
.= g + h by POLYNOM1:def 11;
then
A19: f.b = g.b + h.b by POLYNOM1:15;
A/.(k+1) = A.(k+1) by A8,FINSEQ_1:4,PARTFUN1:def 6;
then
A20: 0.L = h.b by A14,A8,A9,FINSEQ_1:4;
len B = k by A10,FINSEQ_1:17;
then g.b = 0.L by A4,A13,A15;
hence thesis by A19,A20,RLVECT_1:def 4;
end;
hence P[k+1];
end;
A21: P[ 0 ]
proof
let f be Polynomial of n,L, A be LeftLinearCombination of P;
assume that
A is_MonomialRepresentation_of f and
A22: f = Sum(A) & len A = 0;
assume
for i being Element of NAT st i in dom A for m being Monomial of n,L,
p being Polynomial of n,L st A.i = m*'p & p in P holds (m*'p).b = 0.L;
A = <*>the carrier of Polynom-Ring(n,L) by A22;
then f = Sum(<*>(the carrier of Polynom-Ring(n,L))) by A22
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:43
.= 0_(n,L) by POLYNOM1:def 11;
hence thesis by POLYNOM1:22;
end;
A23: for k being Nat holds P[k] from NAT_1:sch 2(A21,A3);
A24: ex n being Element of NAT st n = len A;
thus thesis by A1,A2,A23,A24;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P, b be bag of n;
pred A is_Standard_Representation_of f,P,b,T means
Sum A = f & for i
being Element of NAT st i in dom A ex m being non-zero Monomial of n,L, p being
non-zero Polynomial of n,L st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P;
pred A is_Standard_Representation_of f,P,T means
A is_Standard_Representation_of f,P,HT(f,T),T;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), b be bag of n;
pred f has_a_Standard_Representation_of P,b,T means
ex A being
LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L);
pred f has_a_Standard_Representation_of P,T means
ex A being
LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;
end;
theorem Th32:
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being Polynomial of n,L, P being non empty
Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P, b being bag of
n holds A is_Standard_Representation_of f,P,b,T implies A
is_MonomialRepresentation_of f
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P, b be bag of n;
assume
A1: A is_Standard_Representation_of f,P,b,T;
A2: now
let i be Element of NAT;
assume i in dom A;
then
ex m9 being non-zero Monomial of n,L, p9 being non-zero Polynomial of n
,L st p9 in P & A/.i = m9*'p9 & HT(m9*'p9,T) <= b,T by A1;
hence
ex m being Monomial of n,L, p being Polynomial of n,L st p in P & A/.
i = m*'p;
end;
Sum A = f by A1;
hence thesis by A2;
end;
Lm5: 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,g being Polynomial of n,L, f9,g9 being Element of
Polynom-Ring(n,L) st f = f9 & g = g9 for P being non empty Subset of
Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies ex A being
LeftLinearCombination of P st f9 = g9 + Sum A & for i being Element of NAT st i
in dom A ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n,
L st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T
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,g be Polynomial of n,L, f9,g9 be Element of
Polynom-Ring(n,L);
assume
A1: f = f9 & g = g9;
defpred P[Nat] means for f,g being Polynomial of n,L, f9,g9 being Element of
Polynom-Ring(n,L) st f = f9 & g = g9 for P being non empty Subset of
Polynom-Ring(n,L), R being RedSequence of PolyRedRel(P,T) st R.1 = f & R.len R
= g & len R = $1 ex A being LeftLinearCombination of P st f9 = g9 + Sum A & for
i being Element of NAT st i in dom A ex m being non-zero Monomial of n,L, p
being non-zero Polynomial of n,L st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T)
,T;
let P be non empty Subset of Polynom-Ring(n,L);
assume PolyRedRel(P,T) reduces f,g;
then consider R being RedSequence of PolyRedRel(P,T) such that
A2: R.1 = f & R.len R = 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];
for f,g being Polynomial of n,L, f9,g9 being Element of
Polynom-Ring(n,L) st f = f9 & g = g9 for P being non empty Subset of
Polynom-Ring(n,L), R being RedSequence of PolyRedRel(P,T) st R.1 = f & R.len R
= g & len R = k + 1 ex A being LeftLinearCombination of P st f9 = g9 + Sum A &
for i being Element of NAT st i in dom A ex m being non-zero Monomial of n,L, p
being non-zero Polynomial of n,L st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T)
,T
proof
let f,g be Polynomial of n,L, f9,g9 be Element of Polynom-Ring(n,L);
assume that
A7: f = f9 and
A8: g = g9;
let P be non empty Subset of Polynom-Ring(n,L), R be RedSequence of
PolyRedRel(P,T);
assume that
A9: R.1 = f and
A10: R.len R = g and
A11: len R = k + 1;
set Q = R|(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 A11,FINSEQ_1:17;
A14: dom R = Seg(k+1) by A11,FINSEQ_1:def 3;
A15: now
let i be Nat;
assume that
A16: i in dom Q and
A17: i+1 in dom Q;
i+1 <= k by A13,A17,FINSEQ_1:1;
then
A18: i+1 <= k+1 by A12,XXREAL_0:2;
i <= k by A13,A16,FINSEQ_1:1;
then
A19: i <= k+1 by A12,XXREAL_0:2;
1 <= i+1 by A13,A17,FINSEQ_1:1;
then
A20: i+1 in dom R by A14,A18,FINSEQ_1:1;
1 <= i by A13,A16,FINSEQ_1:1;
then i in dom R by A14,A19,FINSEQ_1:1;
then
A21: [R.i, R.(i+1)] in PolyRedRel(P,T) by A20,REWRITE1:def 2;
R.i = Q.i by A16,FUNCT_1:47;
hence [Q.i, Q.(i+1)] in PolyRedRel(P,T) by A17,A21,FUNCT_1:47;
end;
len Q = k by A11,A12,FINSEQ_1:17;
then reconsider Q as RedSequence of PolyRedRel(P,T) by A5,A15,
REWRITE1:def 2;
A22: 1 in dom Q by A5,A13,FINSEQ_1:1;
then
A23: Q.1 = f by A9,FUNCT_1:47;
1 <= k + 1 by NAT_1:11;
then
A24: k + 1 in dom R by A14,FINSEQ_1:1;
k in dom R by A5,A14,A12,FINSEQ_1:1;
then
A25: [R.k,R.(k+1)] in PolyRedRel(P,T) by A24,REWRITE1:def 2;
then consider h9,g2 being object such that
A26: [R.k,R.(k+1)] = [h9,g2] and
A27: h9 in NonZero Polynom-Ring(n,L) and
A28: g2 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
A29: R.k = h9 by A26,XTUPLE_0:1;
reconsider g2 as Polynomial of n,L by A28,POLYNOM1:def 11;
not h9 in {0_(n,L)} by A3,A27,XBOOLE_0:def 5;
then h9 <> 0_(n,L) by TARSKI:def 1;
then reconsider h9 as non-zero Polynomial of n,L by A27,POLYNOM1:def 11
,POLYNOM7:def 1;
A30: Q.k = h9 by A5,A13,A29,FINSEQ_1:3,FUNCT_1:47;
then reconsider u9 = Q.k as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider u = u9 as Polynomial of n,L by POLYNOM1:def 11;
Q.len Q = u by A11,A12,FINSEQ_1:17;
then consider A9 being LeftLinearCombination of P such that
A31: f9 = u9 + Sum A9 and
A32: for i being Element of NAT st i in dom A9 ex m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st p in P & A9.i = m*'p &
HT(m*'p,T)<=HT(f,T),T by A6,A7,A11,A12,A23,FINSEQ_1:17;
A33: k in dom Q by A5,A13,FINSEQ_1:3;
now
per cases;
case
u9 = g9;
hence thesis by A31,A32;
end;
case
A34: u9 <> g9;
reconsider hh = h9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
A35: PolyRedRel(P,T) reduces f,h9 by A5,A33,A30,A22,A23,REWRITE1:17;
A36: R.(k+1) = g2 by A26,XTUPLE_0:1;
then reconsider
gg = g2 as Element of Polynom-Ring(n,L) by A8,A10,A11;
h9 reduces_to g2,P,T by A25,A26,POLYRED:def 13;
then consider p9 being Polynomial of n,L such that
A37: p9 in P and
A38: h9 reduces_to g2,p9,T by POLYRED:def 7;
consider m9 being Monomial of n,L such that
A39: g2 = h9 - m9 *' p9 and
not HT(m9*'p9,T) in Support g2 and
A40: HT(m9*'p9,T) <= HT(h9,T),T by A38,GROEB_1:2;
A41: now
assume p9 = 0_(n,L);
then g2 = h9 - 0_(n,L) by A39,POLYRED:5
.= Q.k by A30,POLYRED:4;
hence contradiction by A8,A10,A11,A34,A36;
end;
A42: now
assume m9 = 0_(n,L);
then g2 = h9 - 0_(n,L) by A39,POLYRED:5
.= Q.k by A30,POLYRED:4;
hence contradiction by A8,A10,A11,A34,A36;
end;
reconsider mp = m9*'p9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider pp = p9 as Element of P by A37;
set B = (A9)^(<*mp*>);
reconsider mm = m9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
A43: gg = hh - mp by A39,Lm3;
reconsider m9 as non-zero Monomial of n,L by A42,POLYNOM7:def 1;
reconsider p9 as non-zero Polynomial of n,L by A41,POLYNOM7:def 1;
len B = len A9 + len<*m9*'p9*> by FINSEQ_1:22
.= len A9 + 1 by FINSEQ_1:40;
then
A44: dom B = Seg(len A9 + 1) by FINSEQ_1:def 3;
A45: mp = mm * pp by POLYNOM1:def 11;
now
let i be set;
assume
A46: i in dom B;
then reconsider j = i as Element of NAT;
A47: j <= len A9 + 1 by A44,A46,FINSEQ_1:1;
A48: 1 <= j by A44,A46,FINSEQ_1:1;
now
per cases;
case
j = len A9 + 1;
then mp = B.j by FINSEQ_1:42
.= B/.j by A46,PARTFUN1:def 6;
hence ex u being Element of Polynom-Ring(n,L), a being
Element of P st B/.i = u*a by A45;
end;
case
j <> len A9 + 1;
then j < len A9 + 1 by A47,XXREAL_0:1;
then j <= len A9 by NAT_1:13;
then j in Seg(len A9) by A48,FINSEQ_1:1;
then
A49: j in dom A9 by FINSEQ_1:def 3;
then consider
m being non-zero Monomial of n,L, p being non-zero
Polynomial of n,L such that
A50: p in P and
A51: A9.j = m*'p and
HT(m*'p,T) <= HT(f,T),T by A32;
reconsider a9 = p as Element of P by A50;
reconsider u9 = m as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
A52: B.j = B/.j by A46,PARTFUN1:def 6;
u9 * a9 = m *' p by POLYNOM1:def 11
.= B/.j by A49,A51,A52,FINSEQ_1:def 7;
hence ex u being Element of Polynom-Ring(n,L), a being
Element of P st B/.i = u*a;
end;
end;
hence
ex u being Element of Polynom-Ring(n,L), a being Element of
P st B/.i = u*a;
end;
then reconsider B as LeftLinearCombination of P by IDEAL_1:def 9;
h9 is_reducible_wrt p9,T by A38,POLYRED:def 8;
then h9 <> 0_(n,L) by POLYRED:37;
then HT(h9,T) <= HT(f,T),T by A35,POLYRED:44;
then
A53: HT(m9*'p9,T) <= HT(f,T),T by A40,TERMORD:8;
A54: now
let i be Element of NAT;
assume
A55: i in dom B;
then
A56: i <= len A9 + 1 by A44,FINSEQ_1:1;
A57: 1 <= i by A44,A55,FINSEQ_1:1;
now
per cases;
case
i = len A9 + 1;
hence ex m being non-zero Monomial of n,L, p being non-zero
Polynomial of n,L st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A37,A53,
FINSEQ_1:42;
end;
case
i <> len A9 + 1;
then i < len A9 + 1 by A56,XXREAL_0:1;
then i <= len A9 by NAT_1:13;
then i in Seg(len A9) by A57,FINSEQ_1:1;
then
A58: i in dom A9 by FINSEQ_1:def 3;
then consider
m being non-zero Monomial of n,L, p being non-zero
Polynomial of n,L such that
A59: p in P and
A60: A9.i = m*'p and
A61: HT(m*'p,T) <= HT(f,T),T by A32;
B.i = m *' p by A58,A60,FINSEQ_1:def 7;
hence ex m being non-zero Monomial of n,L, p being non-zero
Polynomial of n,L st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A59,A61;
end;
end;
hence ex m being non-zero Monomial of n,L, p being non-zero
Polynomial of n,L st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T;
end;
take B;
gg + Sum B = gg + (Sum(A9) + Sum(<*mp*>)) by RLVECT_1:41
.= gg + (Sum(A9) + mp) by RLVECT_1:44
.= (hh + -mp) + (Sum(A9) + mp) by A43
.= hh + (-mp + (Sum(A9) + mp)) by RLVECT_1:def 3
.= hh + (Sum(A9) + (-mp + mp)) by RLVECT_1:def 3
.= hh + (Sum(A9) + 0.(Polynom-Ring(n,L))) by RLVECT_1:5
.= hh + Sum(A9) by RLVECT_1:4
.= f9 by A5,A13,A29,A31,FINSEQ_1:3,FUNCT_1:47;
hence thesis by A8,A10,A11,A36,A54;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
A62: P[1]
proof
set A = <*>(the carrier of Polynom-Ring(n,L));
let f,g be Polynomial of n,L, f9,g9 be Element of Polynom-Ring(n,L);
assume
A63: f = f9 & g = g9;
let P be non empty Subset of Polynom-Ring(n,L), R be RedSequence of
PolyRedRel(P,T);
for i being set st i in dom A ex u being Element of Polynom-Ring(n,L),
a being Element of P st A/.i = u*a;
then reconsider A as LeftLinearCombination of P by IDEAL_1:def 9;
assume
A64: R.1 = f & R.len R = g & len R = 1;
take A;
f9 = g9 + 0.(Polynom-Ring(n,L)) by A63,A64,RLVECT_1:def 4
.= g9 + Sum A by RLVECT_1:43;
hence thesis;
end;
A65: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A62,A4);
1 <= len R by NAT_1:14;
hence thesis by A1,A65,A2;
end;
theorem
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
being bag of n st A is_Standard_Representation_of f,P,b,T & B
is_Standard_Representation_of g,P,b,T holds A^B is_Standard_Representation_of f
+g,P,b,T
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f,g be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A,B be LeftLinearCombination of P, b be bag of n;
assume that
A1: A is_Standard_Representation_of f,P,b,T and
A2: B is_Standard_Representation_of g,P,b,T;
A3: now
let i be Element of NAT;
assume
A4: i in dom(A^B);
now
per cases by A4,FINSEQ_1:25;
case
A5: i in dom A;
(A^B)/.i = (A^B).i by A4,PARTFUN1:def 6
.= A.i by A5,FINSEQ_1:def 7
.= A/.i by A5,PARTFUN1:def 6;
hence ex m being non-zero Monomial of n,L, p being non-zero Polynomial
of n,L st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A1,A5;
end;
case
ex k being Nat st k in dom B & i = len A + k;
then consider k being Nat such that
A6: k in dom B and
A7: i = len A + k;
(A^B)/.i = (A^B).i by A4,PARTFUN1:def 6
.= B.k by A6,A7,FINSEQ_1:def 7
.= B/.k by A6,PARTFUN1:def 6;
hence ex m being non-zero Monomial of n,L, p being non-zero Polynomial
of n,L st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A2,A6;
end;
end;
hence
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n
,L st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T;
end;
f = Sum A & g = Sum B by A1,A2;
then f + g = Sum A + Sum B by POLYNOM1:def 11
.= Sum(A^B) by RLVECT_1:41;
hence thesis by A3;
end;
theorem
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
being bag of n, i being Element of NAT st A is_Standard_Representation_of f,P,b
,T & B = A|i & g = Sum(A/^i) holds B is_Standard_Representation_of f-g,P,b,T
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f,g be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A,B be LeftLinearCombination of P, b be bag of n, i be
Element of NAT;
assume that
A1: A is_Standard_Representation_of f,P,b,T and
A2: B = A|i and
A3: g = Sum(A/^i);
A4: Sum A = f by A1;
dom(A|(Seg i)) c= dom A by RELAT_1:60;
then
A5: dom B c= dom A by A2,FINSEQ_1:def 16;
A6: now
let j being Element of NAT;
assume
A7: j in dom B;
then
A8: j in dom(A|(Seg i)) by A2,FINSEQ_1:def 16;
A/.j = A.j by A5,A7,PARTFUN1:def 6
.= (A|(Seg i)).j by A8,FUNCT_1:47
.= B.j by A2,FINSEQ_1:def 16
.= B/.j by A7,PARTFUN1:def 6;
hence
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n
,L st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A1,A5,A7;
end;
A = B ^ (A/^i) by A2,RFINSEQ:8;
then Sum A = Sum B + Sum(A/^i) by RLVECT_1:41;
then Sum A + -(Sum(A/^i)) = Sum B + (Sum(A/^i) + -Sum(A/^i)) by
RLVECT_1:def 3
.= Sum B + 0.(Polynom-Ring(n,L)) by RLVECT_1:5
.= Sum B by RLVECT_1:def 4;
then Sum B = Sum A - (Sum(A/^i))
.= f - g by A3,A4,Lm3;
hence thesis by A6;
end;
theorem
for n being Ordinal, T being connected TermOrder of n, L being Abelian
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
being bag of n, i being Element of NAT st A is_Standard_Representation_of f,P,b
,T & B = A/^i & g = Sum(A|i) & i <= len A holds B is_Standard_Representation_of
f-g,P,b,T
proof
let n be Ordinal, T be connected TermOrder of n, L be Abelian right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f,g be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A,B be LeftLinearCombination of P, b be bag of n, i be
Element of NAT;
assume that
A1: A is_Standard_Representation_of f,P,b,T and
A2: B = A/^i and
A3: g = Sum(A|i) and
A4: i <= len A;
A5: Sum A = f by A1;
A6: now
let j being Element of NAT;
assume
A7: j in dom B;
then
A8: j + i in dom A by A2,FINSEQ_5:26;
B/.j = B.j by A7,PARTFUN1:def 6
.= A.(j+i) by A2,A4,A7,RFINSEQ:def 1
.= A/.(j+i) by A8,PARTFUN1:def 6;
hence
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n
,L st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A1,A8;
end;
A = (A|i) ^ B by A2,RFINSEQ:8;
then Sum A = Sum(A|i) + Sum B by RLVECT_1:41;
then Sum A + -(Sum(A|i)) = (Sum(A|i) + -Sum(A|i)) + Sum B by RLVECT_1:def 3
.= 0.(Polynom-Ring(n,L)) + Sum B by RLVECT_1:5
.= Sum B by ALGSTR_1:def 2;
then Sum B = Sum A - (Sum(A|i))
.= f - g by A3,A5,Lm3;
hence thesis by A6;
end;
theorem Th36:
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being non-zero Polynomial of n,L, P being
non empty Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_MonomialRepresentation_of f ex i being Element of NAT, m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st i in dom A & p in P & A.
i = m *' p & HT(f,T) <= HT(m*'p,T),T
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be non-zero Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P;
HC(f,T) <> 0.L;
then
A1: f.(HT(f,T)) <> 0.L by TERMORD:def 7;
assume A is_MonomialRepresentation_of f;
then consider i being Element of NAT such that
A2: i in dom A and
A3: ex m being Monomial of n,L, p being Polynomial of n,L st A.i = m *'
p & p in P & (m*'p).HT(f,T) <> 0.L by A1,Lm4;
consider m being Monomial of n,L, p being Polynomial of n,L such that
A4: A.i = m *' p and
A5: (m*'p).HT(f,T) <> 0.L and
A6: p in P by A3;
A7: m*'p <> 0_(n,L) by A5,POLYNOM1:22;
then
A8: m <> 0_(n,L) by POLYRED:5;
p <> 0_(n,L) by A7,POLYNOM1:28;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 1;
reconsider m as non-zero Monomial of n,L by A8,POLYNOM7:def 1;
HT(f,T) in Support(m*'p) by A5,POLYNOM1:def 4;
then HT(f,T) <= HT(m*'p,T),T by TERMORD:def 6;
hence thesis by A2,A4,A6;
end;
theorem Th37:
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being non-zero Polynomial of n,L, P being
non empty Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_Standard_Representation_of f,P,T ex i being Element of NAT, m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st p in P & i in dom A & A
/.i = m *' p & HT(f,T) = HT(m*'p,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, f be non-zero Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L), A be LeftLinearCombination of P;
assume A is_Standard_Representation_of f,P,T;
then
A1: A is_Standard_Representation_of f,P,HT(f,T),T;
then consider
i being Element of NAT, m being non-zero Monomial of n,L, p being
non-zero Polynomial of n,L such that
A2: i in dom A and
p in P and
A3: A.i = m *' p and
A4: HT(f,T) <= HT(m*'p,T),T by Th32,Th36;
consider m9 being non-zero Monomial of n,L, p9 being non-zero Polynomial of
n,L such that
A5: p9 in P and
A6: A/.i = m9 *' p9 and
A7: HT(m9*'p9,T) <= HT(f,T),T by A1,A2;
take i,m9,p9;
m *' p = m9 *' p9 by A2,A3,A6,PARTFUN1:def 6;
hence thesis by A2,A4,A5,A6,A7,TERMORD:7;
end;
theorem Th38:
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 being Polynomial of n,L, P being non
empty Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,0_(n,L)
implies f has_a_Standard_Representation_of P,T
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 be Polynomial of n,L, P be non empty Subset of
Polynom-Ring(n,L);
reconsider f9 = f as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
A1: 0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
assume PolyRedRel(P,T) reduces f,0_(n,L);
then consider A being LeftLinearCombination of P such that
A2: f9 = 0.(Polynom-Ring(n,L)) + Sum A and
A3: for i being Element of NAT st i in dom A ex m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st p in P & A.i = m*'p & HT
(m*'p,T) <= HT(f,T),T by A1,Lm5;
A4: now
let i be Element of NAT;
assume
A5: i in dom A;
then
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A3;
hence
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n
,L st p in P & A/.i = m *' p & HT(m*'p,T) <= HT(f,T),T by A5,PARTFUN1:def 6;
end;
f = Sum A by A2,RLVECT_1:def 4;
then A is_Standard_Representation_of f,P,HT(f,T),T by A4;
then A is_Standard_Representation_of f,P,T;
hence thesis;
end;
:: lemma 5.60, p. 218
theorem Th39:
for n being Ordinal, T being admissible 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 non-zero Polynomial of n,L, P being non empty Subset of
Polynom-Ring(n,L) holds f has_a_Standard_Representation_of P,T implies f
is_top_reducible_wrt P,T
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 almost_left_invertible non trivial doubleLoopStr, f
be non-zero Polynomial of n,L, P be non empty Subset of Polynom-Ring(n,L);
assume f has_a_Standard_Representation_of P,T;
then consider A being LeftLinearCombination of P such that
A1: A is_Standard_Representation_of f,P,T;
consider i being Element of NAT, m being non-zero Monomial of n,L, p being
non-zero Polynomial of n,L such that
A2: p in P and
i in dom A and
A/.i = m*'p and
A3: HT(f,T) = HT(m*'p,T) by A1,Th37;
set s = HT(m,T);
A4: HT(f,T) = s + HT(p,T) by A3,TERMORD:31;
set g = f - (f.HT(f,T)/HC(p,T)) * (s *' p);
A5: f <> 0_(n,L) by POLYNOM7:def 1;
then Support f <> {} by POLYNOM7:1;
then p <> 0_(n,L) & HT(f,T) in Support f by POLYNOM7:def 1,TERMORD:def 6;
then f reduces_to g,p,HT(f,T),T by A5,A4,POLYRED:def 5;
then f top_reduces_to g,p,T by POLYRED:def 10;
then f is_top_reducible_wrt p,T by POLYRED:def 11;
hence thesis by A2,POLYRED:def 12;
end;
:: lemma 5.61, p. 218
theorem
for n being Element of NAT, T being connected admissible 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, G being non empty Subset of Polynom-Ring
(n,L) holds G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,
L st f in G-Ideal holds f has_a_Standard_Representation_of G,T
proof
let n be Element of NAT, T be connected admissible 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, P be non empty Subset of Polynom-Ring(n,L);
A1: now
assume for f being non-zero Polynomial of n,L st f in P-Ideal holds f
has_a_Standard_Representation_of P,T;
then for f being non-zero Polynomial of n,L st f in P-Ideal holds f
is_top_reducible_wrt P,T by Th39;
then
for b being bag of n st b in HT(P-Ideal,T) ex b9 being bag of n st b9
in HT(P,T) & b9 divides b by GROEB_1:18;
then HT(P-Ideal,T) c= multiples(HT(P,T)) by GROEB_1:19;
then PolyRedRel(P,T) is locally-confluent by GROEB_1:20;
hence P is_Groebner_basis_wrt T by GROEB_1:def 3;
end;
A2: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
now
assume P is_Groebner_basis_wrt T;
then PolyRedRel(P,T) is locally-confluent by GROEB_1:def 3;
hence for f being non-zero Polynomial of n,L st f in P-Ideal holds f
has_a_Standard_Representation_of P,T by A2,Th38,GROEB_1:15;
end;
hence thesis by A1;
end;
:: theorem 5.62, p. 219