:: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger's
:: First Criterium
:: by Christoph Schwarzweller
::
:: Received December 10, 2004
:: Copyright (c) 2004-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, PRE_POLY, ARYTM_3, ARYTM_1, ORDINAL1, BAGORDER,
XXREAL_0, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES, VECTSP_2, ZFMISC_1,
VALUED_0, POLYNOM7, CAT_3, RELAT_2, POLYNOM1, BROUWER, SUPINF_2,
XCMPLX_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, ALGSTR_1, CARD_1,
FUNCT_7, TERMORD, BINOP_1, POLYRED, REWRITE1, FINSEQ_1, STRUCT_0,
FINSET_1, FUNCT_4, FUNCOP_1, ALGSEQ_1, ORDERS_2, WAYBEL_4, RUSUB_4,
GROEB_2, MESFUNC1, GROEB_1, GROEB_3, NAT_1;
notations TARSKI, SUBSET_1, RELAT_1, XBOOLE_0, RELAT_2, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_4,
FUNCOP_1, PRE_POLY, STRUCT_0, ALGSTR_0, GROUP_1, ALGSTR_1, RLVECT_1,
VFUNCT_1, FINSET_1, XTUPLE_0, MCART_1, FINSEQ_1, VECTSP_2, VECTSP_1,
POLYNOM7, ORDERS_2, FUNCT_7, REWRITE1, BAGORDER, TERMORD, GROEB_1,
POLYRED, GROEB_2, WAYBEL_4, POLYNOM1;
constructors XXREAL_0, REWRITE1, VECTSP_2, WAYBEL_4, POLYNOM2, BAGORDER,
TERMORD, POLYRED, GROEB_1, GROEB_2, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, NAT_1,
INT_1, CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
POLYNOM1, POLYNOM2, POLYNOM4, POLYNOM7, TERMORD, POLYRED, ORDINAL1,
VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, RELSET_1, FUNCT_4;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities STRUCT_0, ALGSTR_0;
expansions TARSKI;
theorems TARSKI, VECTSP_1, POLYNOM1, RLVECT_1, NAT_1, INT_1, POLYNOM7,
REWRITE1, XBOOLE_0, TERMORD, CARD_1, FUNCT_1, XBOOLE_1, POLYRED, FUNCT_2,
BAGORDER, ALGSTR_1, CARD_2, GROEB_1, FUNCT_4, FUNCOP_1, FINSET_1,
VECTSP_2, RELSET_1, WAYBEL_4, GROEB_2, GROUP_1, FINSEQ_3, XREAL_1,
XXREAL_0, STRUCT_0, PRE_POLY, XTUPLE_0, SUBSET_1;
schemes FUNCT_2, NAT_1, INT_1;
begin :: Preliminaries
theorem Th1:
for X being set, b1,b2 being bag of X holds (b1 + b2) / b2 = b1
proof
let X be set, b1,b2 be bag of X;
b2 divides b1 + b2 by PRE_POLY:50;
then b2 + ((b1 + b2) / b2) = b1 + b2 by GROEB_2:def 1;
then (b2 + ((b1 + b2) / b2)) -' b2 = b1 by PRE_POLY:48;
hence thesis by PRE_POLY:48;
end;
theorem Th2:
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
being bag of n holds b1 <= b2,T implies b1 + b3 <= b2 + b3,T
proof
let n be Ordinal, T be admissible TermOrder of n, b1,b2,b3 be bag of n;
assume b1 <= b2,T;
then [b1,b2] in T by TERMORD:def 2;
then [b1+b3,b2+b3] in T by BAGORDER:def 5;
hence thesis by TERMORD:def 2;
end;
theorem Th3:
for n being Ordinal, T being TermOrder of n, b1,b2,b3 being bag
of n holds b1 <= b2,T & b2 < b3,T implies b1 < b3,T
proof
let n be Ordinal, T be TermOrder of n, b1,b2,b3 be bag of n;
assume that
A1: b1 <= b2,T and
A2: b2 < b3,T;
A3: b2 <= b3,T by A2,TERMORD:def 3;
then
A4: b1 <= b3,T by A1,TERMORD:8;
b2 <> b3 by A2,TERMORD:def 3;
then b1 <> b3 by A1,A3,TERMORD:7;
hence thesis by A4,TERMORD:def 3;
end;
theorem Th4:
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
being bag of n holds b1 < b2,T implies b1 + b3 < b2 + b3,T
proof
let n be Ordinal, T be admissible TermOrder of n, b1,b2,b3 be bag of n;
assume
A1: b1 < b2,T;
A2: now
assume
A3: b1+b3 = b2+b3;
b1 = (b1 + b3) -' b3 by PRE_POLY:48
.= b2 by A3,PRE_POLY:48;
hence contradiction by A1,TERMORD:def 3;
end;
b1 <= b2,T by A1,TERMORD:def 3;
then [b1,b2] in T by TERMORD:def 2;
then [b1+b3,b2+b3] in T by BAGORDER:def 5;
then b1+b3 <= b2+b3,T by TERMORD:def 2;
hence thesis by A2,TERMORD:def 3;
end;
theorem Th5:
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
b4 being bag of n holds b1 < b2,T & b3 <= b4,T implies b1 + b3 < b2 + b4,T
proof
let n be Ordinal, T be admissible TermOrder of n, b1,b2,b3,b4 be bag of n;
assume that
A1: b1 < b2,T and
A2: b3 <= b4,T;
b1 <= b2,T by A1,TERMORD:def 3;
then [b1,b2] in T by TERMORD:def 2;
then [b1+b3,b2+b3] in T by BAGORDER:def 5;
then
A3: b1+b3 <= b2+b3,T by TERMORD:def 2;
[b3,b4] in T by A2,TERMORD:def 2;
then [b2+b3,b2+b4] in T by BAGORDER:def 5;
then
A4: b2+b3 <= b2+b4,T by TERMORD:def 2;
A5: now
A6: b1 = b1 + b4 -' b4 & b2 = b2 + b4 -' b4 by PRE_POLY:48;
A7: b4 = b4 + b2 -' b2 & b3 = b3 + b2 -' b2 by PRE_POLY:48;
assume b1+b3 = b2+b4;
then b1+b4 = b2+b4 by A3,A4,A7,TERMORD:7;
hence contradiction by A1,A6,TERMORD:def 3;
end;
b1+b3 <= b2+b4,T by A3,A4,TERMORD:8;
hence thesis by A5,TERMORD:def 3;
end;
theorem Th6:
for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
b4 being bag of n holds b1 <= b2,T & b3 < b4,T implies b1 + b3 < b2 + b4,T
proof
let n be Ordinal, T be admissible TermOrder of n, b1,b2,b3,b4 be bag of n;
assume that
A1: b1 <= b2,T and
A2: b3 < b4,T;
b3 <= b4,T by A2,TERMORD:def 3;
then [b3,b4] in T by TERMORD:def 2;
then [b2+b3,b2+b4] in T by BAGORDER:def 5;
then
A3: b2+b3 <= b2+b4,T by TERMORD:def 2;
[b1,b2] in T by A1,TERMORD:def 2;
then [b1+b3,b2+b3] in T by BAGORDER:def 5;
then
A4: b1+b3 <= b2+b3,T by TERMORD:def 2;
A5: now
assume b1+b3 = b2+b4;
then
A6: b2+b4 = b2 +b3 by A4,A3,TERMORD:7;
b4 = b4 + b2 -' b2 & b3 = b3 + b2 -' b2 by PRE_POLY:48;
hence contradiction by A2,A6,TERMORD:def 3;
end;
b1+b3 <= b2+b4,T by A4,A3,TERMORD:8;
hence thesis by A5,TERMORD:def 3;
end;
begin :: More on Polynomials
theorem Th7:
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
m1,m2 being non-zero Monomial of n,L holds term(m1*'m2) = term(m1) + term(m2)
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, m1,m2 be
non-zero Monomial of n,L;
set T = the connected TermOrder of n;
A1: HC(m2,T) <> 0.L;
HC(m1,T) <> 0.L;
then reconsider
a = coefficient(m1), b = coefficient(m2) as non zero Element of L
by A1,TERMORD:23;
a * b <> 0.L by VECTSP_2:def 1;
then reconsider c = a * b as non zero Element of L by STRUCT_0:def 12;
m1 = Monom(a,term(m1)) & m2 = Monom(b,term(m2)) by POLYNOM7:11;
then term(m1 *' m2) = term(Monom(c,term(m1)+term(m2))) by TERMORD:3;
hence thesis by POLYNOM7:10;
end;
theorem Th8:
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, m being non-zero Monomial of n,L, b being bag of n
holds b in Support(p) iff term(m) + b in Support(m*'p)
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, p be
Polynomial of n,L, m be non-zero Monomial of n,L, b be bag of n;
A1: (m*'p).(term(m) + b) = m.term(m) * p.b by POLYRED:7;
m <> 0_(n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then Support m = {term(m)} by POLYNOM7:7;
then term(m) in Support m by TARSKI:def 1;
then
A2: m.term(m) <> 0.L by POLYNOM1:def 4;
A3: now
assume b in Support p;
then p.b <> 0.L by POLYNOM1:def 4;
then
term(m) + b is Element of Bags n & (m*'p).(term(m) + b) <> 0.L by A2,A1,
PRE_POLY:def 12,VECTSP_2:def 1;
hence term(m) + b in Support(m*'p) by POLYNOM1:def 4;
end;
now
assume term(m) + b in Support(m*'p);
then m.term(m) * p.b <> 0.L by A1,POLYNOM1:def 4;
then
A4: p.b <> 0.L;
b is Element of Bags n by PRE_POLY:def 12;
hence b in Support p by A4,POLYNOM1:def 4;
end;
hence thesis by A3;
end;
theorem Th9:
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, m being non-zero Monomial of n,L holds Support(m*'p)
= { term(m) + b where b is Element of Bags n : b in Support p }
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, p be
Polynomial of n,L, m be non-zero Monomial of n,L;
m <> 0_(n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then
A1: Support m = {term(m)} by POLYNOM7:7;
A2: Support(m*'p) c= {s + t where s,t is Element of Bags n : s in Support m
& t in Support p} by TERMORD:30;
A3: now
let u be object;
assume
A4: u in Support(m*'p);
then reconsider u9 = u as Element of Bags n;
u9 in {s + t where s,t is Element of Bags n : s in Support m & t in
Support p} by A2,A4;
then consider s,t being Element of Bags n such that
A5: u9 = s + t & s in Support m and
A6: t in Support p;
u9 = term(m) + t by A1,A5,TARSKI:def 1;
hence u in {term(m)+b where b is Element of Bags n : b in Support p} by A6;
end;
now
let u be object;
assume u in {term(m)+b where b is Element of Bags n : b in Support p};
then ex t being Element of Bags n st u = term(m) + t & t in Support p;
hence u in Support(m*'p) by Th8;
end;
hence thesis by A3,TARSKI:2;
end;
theorem Th10:
for n being Ordinal, L being add-associative
right_complementable left_zeroed right_zeroed well-unital distributive
domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, m being
non-zero Monomial of n,L holds card Support(p) = card Support(m*'p)
proof
let n be Ordinal, L be add-associative right_complementable left_zeroed
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p be Polynomial of n,L, m be non-zero Monomial of n,L;
defpred P[object,object] means $2 = term(m) + In($1,Bags n);
set T = the admissible connected TermOrder of n;
m <> 0_(n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then
A1: Support m = {term(m)} by POLYNOM7:7;
A2: for x being object st x in Support(p)
ex y being object st y in Support(m*'p) & P[x,y]
proof
let x be object;
assume
A3: x in Support p;
then reconsider x9 = x as Element of Bags n;
term(m) + x9 in Support(m*'p) by A3,Th8;
hence thesis;
end;
consider f being Function of Support(p),Support(m*'p) such that
A5: for x being object st x in Support(p) holds P[x,f.x] from FUNCT_2:sch 1
(A2 );
A6: now
assume
A7: Support(m*'p) = {};
now
assume Support p <> {};
then p <> 0_(n,L) by POLYNOM7:1;
then reconsider p9 = p as non-zero Polynomial of n,L by POLYNOM7:def 1;
HT(m,T) + HT(p9,T) in Support(m*'p9) by TERMORD:29;
hence contradiction by A7;
end;
hence Support(p) = {};
end;
then
A8: Support(p) c= dom f by FUNCT_2:def 1;
A9: Support(m*'p) c= {s + t where s,t is Element of Bags n : s in Support m
& t in Support p} by TERMORD:30;
A10: now
let u be object;
assume
A11: u in Support(m*'p);
then reconsider u9 = u as Element of Bags n;
u9 in {s + t where s,t is Element of Bags n : s in Support m & t in
Support p} by A9,A11;
then consider s,t being Element of Bags n such that
A12: u9 = s + t & s in Support m and
A13: t in Support p;
A14: t in dom f by A6,A13,FUNCT_2:def 1;
A15: t = In(t,Bags n);
u9 = term(m) + t by A1,A12,TARSKI:def 1;
then u9 = f.t by A5,A13,A15;
hence u in f.:Support(p) by A14,FUNCT_1:def 6;
end;
now
let x1,x2 be object;
assume that
A16: x1 in Support(p) and
A17: x2 in Support(p) and
A18: f.x1 = f.x2;
reconsider x19 = x1, x29 = x2 as Element of Bags n by A16,A17;
A19: x29 = In(x29,Bags n);
x19 = In(x19,Bags n);
then term(m) + x19 = f.x29 by A5,A16,A18
.= term(m) + x29 by A5,A17,A19;
hence x1 = x29 + term(m) -' term(m) by PRE_POLY:48
.= x2 by PRE_POLY:48;
end;
then f is one-to-one by A6,FUNCT_2:19;
then
A20: Support(p),f.:Support(p) are_equipotent by A8,CARD_1:33;
for u being object holds u in f.:Support(p) implies u in Support(m*'p);
then f.:Support(p) = Support(m*'p) by A10,TARSKI:2;
hence thesis by A20,CARD_1:5;
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
be Polynomial of n,L, g be object, P be 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;
reconsider l = len p - 1 as Element of NAT by INT_1:5,NAT_1:14;
A3: 1 <= len p by NAT_1:14;
set h = p.l;
1 <= l + 1 by NAT_1:12;
then
A4: l + 1 in dom p by FINSEQ_3:25;
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 dom p by A5,FINSEQ_3:25;
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;
theorem Th11:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr
holds Red(0_(n,L),T) = 0_(n,L)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed non trivial addLoopStr;
set e = 0_(n,L), h = HM(e,T);
HC(h,T) = HC(e,T) by TERMORD:27
.= e.(HT(e,T)) by TERMORD:def 7
.= 0.L by POLYNOM1:22;
then h = 0_(n,L) by TERMORD:17;
hence Red(e,T) = e - 0_(n,L) by TERMORD:def 9
.= 0_(n,L) by POLYRED:4;
end;
theorem Th12:
for n being Ordinal, L being Abelian add-associative
right_zeroed right_complementable commutative well-unital distributive non
trivial doubleLoopStr, p,q being Polynomial of n,L holds p - q = 0_(n,L)
implies p = q
proof
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable commutative well-unital distributive non trivial
doubleLoopStr, p,q be Polynomial of n,L;
assume p - q = 0_(n,L);
hence q = q + (p - q) by POLYNOM1:23
.= q + (p + -q) by POLYNOM1:def 7
.= (q + -q) + p by POLYNOM1:21
.= 0_(n,L) + p by POLYRED:3
.= p by POLYRED:2;
end;
theorem Th13:
for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr holds -(0_(X,L)) = 0_(X,L)
proof
let X be set, L be add-associative right_zeroed right_complementable non
empty addLoopStr;
set o = -(0_(X,L)), e = 0_(X,L);
A1: now
let x be object;
assume x in dom o;
then reconsider b = x as bag of X;
o.b = -(e.b) by POLYNOM1:17
.= -(0.L) by POLYNOM1:22
.= 0.L by RLVECT_1:12
.= e.b by POLYNOM1:22;
hence o.x = e.x;
end;
dom o = Bags X by FUNCT_2:def 1
.= dom e by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th14:
for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, f being Series of X,L holds 0_(X,L
) - f = -f
proof
let X be set, L be add-associative right_zeroed right_complementable non
empty addLoopStr, f be Series of X,L;
set p = 0_(X,L) - f;
A1: now
let x be object;
assume x in dom p;
then reconsider b = x as Element of Bags X;
p.b = (0_(X,L) + -f).b by POLYNOM1:def 7
.= 0_(X,L).b + (-f).b by POLYNOM1:15
.= 0.L + (-f).b by POLYNOM1:22
.= (-f).b by ALGSTR_1:def 2;
hence p.x = (-f).x;
end;
dom p = Bags X by FUNCT_2:def 1
.= dom(-f) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th15:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial doubleLoopStr,
p being Polynomial of n,L holds p - Red(p,T) = HM(p,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed non trivial doubleLoopStr, p be Polynomial
of n,L;
thus p - Red(p,T) = (HM(p,T) + Red(p,T)) - Red(p,T) by TERMORD:38
.= (HM(p,T) + Red(p,T)) + (-Red(p,T)) by POLYNOM1:def 7
.= HM(p,T) + (Red(p,T) + (-Red(p,T))) by POLYNOM1:21
.= HM(p,T) + 0_(n,L) by POLYRED:3
.= HM(p,T) by POLYNOM1:23;
end;
registration
let n be Ordinal, L be add-associative right_complementable right_zeroed
non empty addLoopStr, p be Polynomial of n,L;
cluster Support p -> finite;
coherence by POLYNOM1:def 5;
end;
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n,L;
redefine func {p,q} -> Subset of Polynom-Ring(n,L); :: redefines { (TARSKI, definition)
coherence
proof
now
let u be object;
assume
A1: u in {p,q};
now
per cases by A1,TARSKI:def 2;
case
u = p;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
case
u = q;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
end;
hence u in the carrier of Polynom-Ring(n,L);
end;
hence thesis by TARSKI:def 3;
end;
end;
begin :: Restriction and Splitting of Polynomials
definition
let X be set, L be non empty ZeroStr, s be Series of X,L, Y be Subset of
Bags X;
func s|Y -> Series of X,L equals
s +* ((Support s \ Y) --> 0.L);
coherence
proof
set m = (Support s \ Y) --> 0.L;
set r = s +* m;
A1: now
let x be object;
assume x in Bags X;
then reconsider x9 = x as Element of Bags X;
now
per cases;
case
A2: x9 in dom m;
then r.x9 = m.x9 by FUNCT_4:13
.= 0.L by A2,FUNCOP_1:7;
hence r.x in the carrier of L;
end;
case
not x in dom m;
then r.x9 = s.x9 by FUNCT_4:11;
hence r.x in the carrier of L;
end;
end;
hence r.x in the carrier of L;
end;
now
let u be object;
assume u in Support s \ Y;
then u in Support s by XBOOLE_0:def 5;
hence u in Bags X;
end;
then
A3: Support s \ Y c= Bags X;
dom s = Bags X & dom m = Support s \ Y by FUNCT_2:def 1;
then dom r = Bags X \/ (Support s \ Y) by FUNCT_4:def 1;
hence thesis by A3,A1,FUNCT_2:3,XBOOLE_1:12;
end;
end;
Lm2: for X being set, L being non empty ZeroStr, s being Series of X,L, Y
being Subset of Bags X holds Support(s|Y) c= Support s
proof
let X be set, L be non empty ZeroStr, s be Series of X,L, Y be Subset of
Bags X;
set m = (Support s \ Y) --> 0.L;
set r = s +* m;
let u be object;
assume
A1: u in Support(s|Y);
then reconsider u9 = u as Element of Bags X;
A2: r.u9 <> 0.L by A1,POLYNOM1:def 4;
now
per cases;
case
u9 in dom m;
hence u9 in Support s by XBOOLE_0:def 5;
end;
case
not u9 in dom m;
hence s.u9 <> 0.L by A2,FUNCT_4:11;
end;
end;
hence thesis by POLYNOM1:def 4;
end;
registration
let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n,L, Y be
Subset of Bags n;
cluster p|Y -> finite-Support;
coherence
proof
Support p is finite by POLYNOM1:def 5;
then Support(p|Y) is finite by Lm2,FINSET_1:1;
hence thesis by POLYNOM1:def 5;
end;
end;
theorem Th16:
for X being set, L being non empty ZeroStr, s being Series of X,
L, Y being Subset of Bags X holds Support s|Y = (Support s) /\ Y & for b being
bag of X st b in Support s|Y holds (s|Y).b = s.b
proof
let X be set, L be non empty ZeroStr, s be Series of X,L, Y be Subset of
Bags X;
set m = (Support s \ Y) --> 0.L;
set r = s +* m;
A1: now
let u be object;
assume
A2: u in Support(s|Y);
then reconsider u9 = u as Element of Bags X;
A3: now
assume
A4: u9 in dom m;
then r.u9 = m.u9 by FUNCT_4:13
.= 0.L by A4,FUNCOP_1:7;
hence contradiction by A2,POLYNOM1:def 4;
end;
r.u9 <> 0.L by A2,POLYNOM1:def 4;
then s.u9 <> 0.L by A3,FUNCT_4:11;
then
A5: u9 in Support s by POLYNOM1:def 4;
dom m = Support s \ Y by FUNCOP_1:13;
then u9 in Y by A3,A5,XBOOLE_0:def 5;
hence u in (Support s) /\ Y by A5,XBOOLE_0:def 4;
end;
A6: dom m = Support s \ Y by FUNCOP_1:13;
now
let u be object;
assume
A7: u in Support s /\ Y;
then
A8: u in Support s by XBOOLE_0:def 4;
then reconsider u9 = u as Element of Bags X;
u in Y by A7,XBOOLE_0:def 4;
then not u in Support s \ Y by XBOOLE_0:def 5;
then r.u9 = s.u9 by A6,FUNCT_4:11;
then r.u9 <> 0.L by A8,POLYNOM1:def 4;
hence u in Support s|Y by POLYNOM1:def 4;
end;
hence
A9: Support s|Y = Support s /\ Y by A1,TARSKI:2;
now
let b be bag of X;
assume b in Support s|Y;
then b in Y by A9,XBOOLE_0:def 4;
then not b in dom m by XBOOLE_0:def 5;
hence (s|Y).b = s.b by FUNCT_4:11;
end;
hence thesis;
end;
theorem
for X being set, L being non empty ZeroStr, s being Series of X,L, Y
being Subset of Bags X holds Support(s|Y) c= Support s by Lm2;
theorem
for X being set, L being non empty ZeroStr, s being Series of X,L
holds s|(Support s) = s & s|({} Bags X) = 0_(X,L)
proof
let X be set, L be non empty ZeroStr, s be Series of X,L;
set r = s|(Support s);
set e = s|({} Bags X);
r = s +* ({} --> 0.L) & dom({} --> 0.L) = {} by XBOOLE_1:37;
hence r = s +* {}
.= s;
A1: dom((Support s) --> 0.L) = Support s by FUNCOP_1:13;
A2: now
let u be object;
assume u in dom e;
then reconsider u9 = u as Element of Bags X;
now
per cases;
case
A3: u9 in Support s;
then e.u9 = ((Support s) --> 0.L).u9 by A1,FUNCT_4:13
.= 0.L by A3,FUNCOP_1:7;
hence e.u9 = 0_(X,L).u9 by POLYNOM1:22;
end;
case
A4: not u9 in Support s;
then e.u9 = s.u9 by A1,FUNCT_4:11;
then e.u9 = 0.L by A4,POLYNOM1:def 4;
hence e.u9 = 0_(X,L).u9 by POLYNOM1:22;
end;
end;
hence e.u = 0_(X,L).u;
end;
dom e = Bags X by FUNCT_2:def 1
.= dom(0_(X,L)) by FUNCT_2:def 1;
hence thesis by A2,FUNCT_1:2;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat such that
A1: i <= card(Support p);
func Upper_Support(p,T,i) -> finite Subset of Bags n means
:Def2:
it c=
Support p & card it = i & for b,b9 being bag of n st b in it & b9 in Support p
& b <= b9,T holds b9 in it;
existence
proof
defpred P[Nat] means $1 > card(Support p) or ex M being finite
Subset of Bags n st M c= Support p & card M = $1 & for b,b9 being bag of n st b
in M & b9 in Support p & b <= b9,T holds b9 in M;
A2: now
let k be Nat;
assume
A3: P[k];
k + 1 > card(Support p) or ex M being finite Subset of Bags n st M
c= Support p & card M = k + 1 & for b,b9 being bag of n st b in M & b9 in
Support p & b <= b9,T holds b9 in M
proof
set R = RelStr(#Bags n,T#);
assume
A4: not k + 1 > card(Support p);
k <= k + 1 by NAT_1:11;
then consider M1 being finite Subset of Bags n such that
A5: M1 c= Support p and
A6: card M1 = k and
A7: for b,b9 being bag of n st b in M1 & b9 in Support p & b <=
b9,T holds b9 in M1 by A3,A4,XXREAL_0:2;
set G = Support p \ M1;
now
let u be object;
assume u in G;
then u in Support p by XBOOLE_0:def 5;
hence u in Bags n;
end;
then reconsider G as Subset of Bags n by TARSKI:def 3;
A8: for u being object holds u in M1 implies u in Support p by A5;
now
assume G = {};
then Support p c= M1 by XBOOLE_1:37;
then for u being object holds u in Support p implies u in M1;
then card Support p = k by A6,A8,TARSKI:2;
hence contradiction by A4,NAT_1:16;
end;
then reconsider G as non empty finite Subset of Bags n;
consider x being Element of R such that
A9: x in G and
A10: x is_maximal_wrt G, the InternalRel of R by BAGORDER:6;
reconsider b = x as bag of n;
set M = M1 \/ {b};
now
let u be object;
assume u in {b};
then u = b by TARSKI:def 1;
hence u in Bags n;
end;
then {b} c= Bags n;
then M c= Bags n \/ Bags n by XBOOLE_1:13;
then reconsider M as finite Subset of Bags n;
now
let u be object;
assume
A11: u in M;
now
per cases by A11,XBOOLE_0:def 3;
case
u in M1;
hence u in Support p by A5;
end;
case
u in {b};
then u in G by A9,TARSKI:def 1;
hence u in Support p by XBOOLE_0:def 5;
end;
end;
hence u in Support p;
end;
then
A12: M c= Support p;
A13: now
let b9 be bag of n;
assume
A14: b9 in G;
now
per cases;
case
b9 = b;
hence b9 <= b,T by TERMORD:6;
end;
case
b9 <> b;
then not [b,b9] in T by A10,A14,WAYBEL_4:def 23;
then not b <= b9,T by TERMORD:def 2;
then b9 < b,T by TERMORD:5;
hence b9 <= b,T by TERMORD:def 3;
end;
end;
hence b9 <= b,T;
end;
A15: now
let b1,b2 being bag of n;
assume that
A16: b1 in M and
A17: b2 in Support p and
A18: b1 <= b2,T;
now
per cases by A16,XBOOLE_0:def 3;
case
b1 in M1;
then b2 in M1 by A7,A17,A18;
hence b2 in M by XBOOLE_0:def 3;
end;
case
b1 in {b};
then
A19: b1 = b by TARSKI:def 1;
per cases;
suppose
b2 = b1;
hence b2 in M by A16;
end;
suppose
b2 <> b1;
then
A20: b1 < b2,T by A18,TERMORD:def 3;
not b2 in G by A20,TERMORD:5,A13,A19;
then b2 in M1 by A17,XBOOLE_0:def 5;
hence b2 in M by XBOOLE_0:def 3;
end;
end;
end;
hence b2 in M;
end;
not b in M1 by A9,XBOOLE_0:def 5;
then card M = k + 1 by A6,CARD_2:41;
hence thesis by A12,A15;
end;
hence P[k+1];
end;
ex M being finite Subset of Bags n st M c= Support p & card M = 0 &
for b,b9 being bag of n st b in M & b9 in Support p & b <= b9,T holds b9 in M
proof
set M = {} Bags n;
take M;
thus thesis;
end;
then
A21: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A21,A2);
hence thesis by A1;
end;
uniqueness
proof
let F1,F2 be finite Subset of Bags n;
assume that
A22: F1 c= Support p and
A23: card F1 = i and
A24: for b,b9 being bag of n st b in F1 & b9 in Support p & b <= b9,T
holds b9 in F1;
assume that
A25: F2 c= Support p and
A26: card F2 = i and
A27: for b,b9 being bag of n st b in F2 & b9 in Support p & b <= b9,T
holds b9 in F2;
now
let u be object;
assume
A28: u in F1;
then reconsider u9 = u as Element of Bags n;
now
assume
A29: not u9 in F2;
now
let x be object;
assume
A30: x in F2;
then reconsider x9 = x as Element of Bags n;
now
per cases;
case
u9 <= x9,T;
hence x9 in F1 by A24,A25,A28,A30;
end;
case
not u9 <= x9,T;
then x9 < u9,T by TERMORD:5;
then x9 <= u9,T by TERMORD:def 3;
hence x9 in F1 by A22,A27,A28,A29,A30;
end;
end;
hence x in F1;
end;
then F2 c= F1;
then F2 c< F1 by A28,A29,XBOOLE_0:def 8;
hence contradiction by A23,A26,CARD_2:48;
end;
hence u in F2;
end;
then F1 c= F2;
hence thesis by A23,A26,CARD_2:102;
end;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat;
func Lower_Support(p,T,i) -> finite Subset of Bags n equals
Support(p) \ Upper_Support(p,T,i);
coherence
proof
Support(p) \ Upper_Support(p,T,i) c= Support p by XBOOLE_1:36;
hence thesis by XBOOLE_1:1;
end;
end;
theorem Th19:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Upper_Support(p,T,i) \/ Lower_Support(p,T,i) = Support p & Upper_Support(p,T,i)
/\ Lower_Support(p,T,i) = {}
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
set M = Upper_Support(p,T,i) /\ (Support(p)\Upper_Support(p,T,i));
assume i <= card(Support p);
then
A1: Upper_Support(p,T,i) c= Support p by Def2;
thus Upper_Support(p,T,i) \/ Lower_Support(p,T,i) = Upper_Support(p,T,i) \/
Support p by XBOOLE_1:39
.= Support p by A1,XBOOLE_1:12;
now
set x = the Element of M;
assume M <> {};
then x in Upper_Support(p,T,i) & x in Support(p)\Upper_Support(p,T,i) by
XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5;
end;
hence thesis;
end;
theorem Th20:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
b9 being bag of n st b in Upper_Support(p,T,i) & b9 in Lower_Support(p,T,i)
holds b9 < b,T
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume
A1: i <= card(Support p);
let b,b9 being bag of n;
assume that
A2: b in Upper_Support(p,T,i) and
A3: b9 in Lower_Support(p,T,i);
A4: Lower_Support(p,T,i) c= Support p by XBOOLE_1:36;
now
assume b <= b9,T;
then b9 in Upper_Support(p,T,i) by A1,A2,A3,A4,Def2;
then b9 in Upper_Support(p,T,i) /\ Lower_Support(p,T,i) by A3,
XBOOLE_0:def 4;
hence contradiction by A1,Th19;
end;
hence thesis by TERMORD:5;
end;
theorem
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,0) = {} & Lower_Support(p,T,0)
= Support p
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L;
set u = Upper_Support(p,T,0);
0 <= card(Support p);
then card u = 0 by Def2;
hence u = {};
hence thesis;
end;
theorem Th22:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,card(Support p)) = Support p &
Lower_Support(p,T,card(Support p)) = {}
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L;
set u = Upper_Support(p,T,card(Support p));
u c= Support p & card u = card(Support p) by Def2;
hence u = Support p by CARD_2:102;
hence thesis by XBOOLE_1:37;
end;
theorem Th23:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non trivial addLoopStr, p
being non-zero Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(
Support p) holds HT(p,T) in Upper_Support(p,T,i)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non trivial addLoopStr, p be non-zero
Polynomial of n,L, i be Element of NAT;
assume that
A1: 1 <= i and
A2: i <= card(Support p);
p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then
A3: HT(p,T) in Support p by TERMORD:def 6;
set u = Upper_Support(p,T,i);
set x = the Element of u;
A4: u <> {} by A1,A2,Def2,CARD_1:27;
then
A5: x in u;
then reconsider x9 = x as Element of Bags n;
u c= Support p by A2,Def2;
then x9 <= HT(p,T),T by A5,TERMORD:def 6;
hence thesis by A2,A4,A3,Def2;
end;
theorem Th24:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Lower_Support(p,T,i) c= Support p & card Lower_Support(p,T,i) = card(Support p)
- i & for b,b9 being bag of n st b in Lower_Support(p,T,i) & b9 in Support p &
b9 <= b,T holds b9 in Lower_Support(p,T,i)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i being Element of NAT;
assume
A1: i <= card Support p;
set l = Lower_Support(p,T,i);
thus l c= Support p by XBOOLE_1:36;
Upper_Support(p,T,i) c= Support p by A1,Def2;
hence card l = card(Support p)-card(Upper_Support(p,T,i)) by CARD_2:44
.= card(Support p) - i by A1,Def2;
now
let b,b9 be bag of n;
assume that
A2: b in Lower_Support(p,T,i) and
A3: b9 in Support p and
A4: b9 <= b,T;
A5: b9 in Upper_Support(p,T,i) \/ Lower_Support(p,T,i) by A1,A3,Th19;
now
assume not b9 in Lower_Support(p,T,i);
then b9 in Upper_Support(p,T,i) by A5,XBOOLE_0:def 3;
then b < b9,T by A1,A2,Th20;
hence contradiction by A4,TERMORD:5;
end;
hence b9 in Lower_Support(p,T,i);
end;
hence thesis;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Nat;
func Up(p,T,i) -> Polynomial of n,L equals
p|(Upper_Support(p,T,i));
coherence;
func Low(p,T,i) -> Polynomial of n,L equals
p|(Lower_Support(p,T,i));
coherence;
end;
Lm3: for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support(p|(Upper_Support(p,T,i))) = Upper_Support(p,T,i) & Support(p|(
Lower_Support(p,T,i))) = Lower_Support(p,T,i)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
set u = Upper_Support(p,T,i), pu = p|(Upper_Support(p,T,i));
set l = Lower_Support(p,T,i), pl = p|(Lower_Support(p,T,i));
assume i <= card(Support p);
then
A1: u c= Support p by Def2;
Support pu = (Support p) /\ u by Th16;
hence Support pu = u by A1,XBOOLE_1:28;
Support pl = (Support p) /\ l by Th16;
hence thesis by XBOOLE_1:28,36;
end;
theorem
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support Up(p,T,i) = Upper_Support(p,T,i) & Support Low(p,T,i) = Lower_Support(p
,T,i) by Lm3;
theorem Th26:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support(Up(p,T,i)) c= Support(p) & Support(Low(p,T,i)) c= Support(p)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume
A1: i <= card(Support p);
then Support(p|(Upper_Support(p,T,i))) = Upper_Support(p,T,i) & Support(p|(
Lower_Support(p,T,i))) = Lower_Support(p,T,i) by Lm3;
hence thesis by A1,Def2,Th24;
end;
theorem Th27:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(Support p
) holds Support(Low(p,T,i)) c= Support(Red(p,T))
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of
n,L, i be Element of NAT;
assume that
A1: 1 <= i and
A2: i <= card(Support p);
Support p <> {} by A1,A2;
then p <> 0_(n,L) by POLYNOM7:1;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 1;
set sl = Lower_Support(p,T,i);
A3: now
assume
A4: HT(p,T) in sl;
HT(p,T) in Upper_Support(p,T,i) by A1,A2,Th23;
then HT(p,T) in Upper_Support(p,T,i) /\ sl by A4,XBOOLE_0:def 4;
hence contradiction by A2,Th19;
end;
now
set u = the Element of {HT(p,T)} /\ sl;
assume {HT(p,T)} /\ sl <> {};
then u in {HT(p,T)} & u in sl by XBOOLE_0:def 4;
hence contradiction by A3,TARSKI:def 1;
end;
then {HT(p,T)} misses sl by XBOOLE_0:def 7;
then
A5: sl \ {HT(p,T)} = sl by XBOOLE_1:83
.= Support(Low(p,T,i)) by A2,Lm3;
Support(Low(p,T,i)) \ {HT(p,T)} c= Support(p) \ {HT(p,T)} by A2,Th26,
XBOOLE_1:33;
then Support(Low(p,T,i)) \ {HT(p,T)} c= Support(Red(p,T)) by TERMORD:36;
hence thesis by A2,A5,Lm3;
end;
theorem Th28:
for n be Ordinal, T be connected TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT st i <= card(Support p) for b being bag
of n st b in Support p holds (b in Support Up(p,T,i) or b in Support Low(p,T,i)
) & not(b in Support Up(p,T,i) /\ Support Low(p,T,i))
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume
A1: i <= card(Support p);
let b being bag of n;
assume
A2: b in Support p;
Support p = Upper_Support(p,T,i) \/ Lower_Support(p,T,i) by A1,Th19
.= Support Up(p,T,i) \/ Lower_Support(p,T,i) by A1,Lm3
.= Support Up(p,T,i) \/ Support Low(p,T,i) by A1,Lm3;
hence b in Support Up(p,T,i) or b in Support Low(p,T,i) by A2,XBOOLE_0:def 3;
Support Up(p,T,i) = Upper_Support(p,T,i) & Support Low(p,T,i) =
Lower_Support(p,T,i) by A1,Lm3;
hence thesis by A1,Th19;
end;
theorem Th29:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
b9 being bag of n st b in Support Low(p,T,i) & b9 in Support Up(p,T,i) holds b
< b9,T
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume
A1: i <= card(Support p);
let b,b9 be bag of n;
assume
A2: b in Support Low(p,T,i) & b9 in Support Up(p,T,i);
Support Up(p,T,i) = Upper_Support(p,T,i) & Support Low(p,T,i) =
Lower_Support(p,T,i) by A1,Lm3;
hence thesis by A1,A2,Th20;
end;
theorem Th30:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(Support p
) holds HT(p,T) in Support Up(p,T,i)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume that
A1: 1 <= i and
A2: i <= card(Support p);
Support p <> {} by A1,A2;
then
A3: HT(p,T) in Support p by TERMORD:def 6;
set u = Up(p,T,i);
set x = the Element of Support u;
A4: Support u = Upper_Support(p,T,i) by A2,Lm3;
then card (Support u) <> 0 by A1,A2,Def2;
then
A5: Support u <> {};
then
A6: x in Support u;
then reconsider x as Element of Bags n;
Support u c= Support p by A2,A4,Def2;
then x <= HT(p,T),T by A6,TERMORD:def 6;
hence thesis by A2,A4,A5,A3,Def2;
end;
theorem Th31:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Low(p,T,i) holds Low(p,T,i).b = p.b & Up(p,T,i).
b = 0.L
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
set l = Lower_Support(p,T,i);
assume
A1: i <= card(Support p);
then
A2: l /\ Upper_Support(p,T,i) = {} by Th19;
let b be bag of n;
assume
A3: b in Support Low(p,T,i);
hence Low(p,T,i).b = p.b by Th16;
b in l by A1,A3,Lm3;
then not b in Upper_Support(p,T,i) by A2,XBOOLE_0:def 4;
then
A4: not b in Support(Up(p,T,i)) by A1,Lm3;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A4,POLYNOM1:def 4;
end;
theorem Th32:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Up(p,T,i) holds Up(p,T,i).b = p.b & Low(p,T,i).b
= 0.L
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
set u = Upper_Support(p,T,i);
assume
A1: i <= card(Support p);
then
A2: u /\ Lower_Support(p,T,i) = {} by Th19;
let b be bag of n;
assume
A3: b in Support Up(p,T,i);
hence Up(p,T,i).b = p.b by Th16;
b in u by A1,A3,Lm3;
then not b in Lower_Support(p,T,i) by A2,XBOOLE_0:def 4;
then
A4: not b in Support(Low(p,T,i)) by A1,Lm3;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A4,POLYNOM1:def 4;
end;
theorem Th33:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Up(p,T,i) + Low(p,T,i) = p
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
set u = Up(p,T,i) + Low(p,T,i);
assume
A1: i <= card(Support p);
A2: now
let x be object;
assume
A3: x in Support p;
then reconsider x9 = x as Element of Bags n;
A4: u.x9 = Up(p,T,i).x9 + Low(p,T,i).x9 by POLYNOM1:15;
A5: now
per cases by A1,A3,Th28;
case
A6: x9 in Support Up(p,T,i);
hence u.x9 = Up(p,T,i).x9 + 0.L by A1,A4,Th32
.= Up(p,T,i).x9 by RLVECT_1:def 4
.= p.x9 by A1,A6,Th32;
end;
case
A7: x9 in Support Low(p,T,i);
hence u.x9 = 0.L + Low(p,T,i).x9 by A1,A4,Th31
.= Low(p,T,i).x9 by ALGSTR_1:def 2
.= p.x9 by A1,A7,Th31;
end;
end;
p.x9 <> 0.L by A3,POLYNOM1:def 4;
hence x in Support u by A5,POLYNOM1:def 4;
end;
now
let x be object;
Support Up(p,T,i) c= Support p & Support Low(p,T,i) c= Support p by A1,Th26
;
then
Support u c= Support Up(p,T,i) \/ Support Low(p,T,i) & Support Up(p,T,
i) \/ Support Low(p,T,i) c= Support p by POLYNOM1:20,XBOOLE_1:8;
then
A8: Support u c= Support p;
assume x in Support u;
hence x in Support p by A8;
end;
then
A9: Support u = Support p by A2,TARSKI:2;
A10: now
let x be object;
assume x in dom p;
then reconsider x9 = x as Element of Bags n;
A11: u.x9 = Up(p,T,i).x9 + Low(p,T,i).x9 by POLYNOM1:15;
now
per cases;
case
A12: x9 in Support p;
now
per cases by A1,A12,Th28;
case
A13: x9 in Support Up(p,T,i);
hence u.x9 = Up(p,T,i).x9 + 0.L by A1,A11,Th32
.= Up(p,T,i).x9 by RLVECT_1:def 4
.= p.x9 by A1,A13,Th32;
end;
case
A14: x9 in Support Low(p,T,i);
hence u.x9 = 0.L + Low(p,T,i).x9 by A1,A11,Th31
.= Low(p,T,i).x9 by ALGSTR_1:def 2
.= p.x9 by A1,A14,Th31;
end;
end;
hence p.x9 = u.x9;
end;
case
A15: not x9 in Support p;
hence p.x9 = 0.L by POLYNOM1:def 4
.= u.x9 by A9,A15,POLYNOM1:def 4;
end;
end;
hence p.x = u.x;
end;
dom p = Bags n by FUNCT_2:def 1
.= dom u by FUNCT_2:def 1;
hence thesis by A10,FUNCT_1:2;
end;
theorem Th34:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Up(p,T,0) = 0_(n,L) & Low(p,T,0) = p
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L;
set u = Up(p,T,0), l = Low(p,T,0);
A1: 0 <= card(Support p);
then Support u = Upper_Support(p,T,0) by Lm3;
then card(Support u) = 0 by A1,Def2;
then Support u = {};
hence u = 0_(n,L) by POLYNOM7:1;
then 0_(n,L) + l = p by A1,Th33;
hence thesis by POLYRED:2;
end;
theorem Th35:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable Abelian non empty
doubleLoopStr, p being Polynomial of n,L holds Up(p,T,card(Support p)) = p &
Low(p,T,card(Support p)) = 0_(n,L)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable Abelian non empty doubleLoopStr, p be
Polynomial of n,L;
set u = Up(p,T,card(Support p)), l = Low(p,T,card(Support p));
Support u = (Support p) /\ Upper_Support(p,T,card(Support p)) by Th16;
then
A1: Support u c= Support p by XBOOLE_1:17;
A2: card(Support u) = card(Upper_Support(p,T,card(Support p))) by Lm3
.= card(Support p) by Th22;
A3: now
let x be object;
assume
A4: x in Support p;
now
assume not x in Support u;
then Support u c< Support p by A1,A4,XBOOLE_0:def 8;
hence contradiction by A2,CARD_2:48;
end;
hence x in Support u;
end;
for x being object holds x in Support u implies x in Support p by A1;
then
A5: Support u = Support p by A3,TARSKI:2;
A6: now
let x be object;
assume x in dom p;
then reconsider x9 = x as Element of Bags n;
now
per cases;
case
x in Support p;
hence p.x9 = u.x9 by A5,Th16;
end;
case
A7: not x in Support p;
hence p.x9 = 0.L by POLYNOM1:def 4
.= u.x9 by A5,A7,POLYNOM1:def 4;
end;
end;
hence p.x = u.x;
end;
dom p = Bags n by FUNCT_2:def 1
.= dom u by FUNCT_2:def 1;
hence
A8: p = u by A6,FUNCT_1:2;
thus 0_(n,L) = p + -p by POLYRED:3
.= (l + p) + -p by A8,Th33
.= l + (p + -p) by POLYNOM1:21
.= l + 0_(n,L) by POLYRED:3
.= l by POLYRED:2;
end;
theorem Th36:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable Abelian non trivial
doubleLoopStr, p being non-zero Polynomial of n,L holds Up(p,T,1) = HM(p,T) &
Low(p,T,1) = Red(p,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable Abelian non trivial doubleLoopStr, p be
non-zero Polynomial of n,L;
set u = Up(p,T,1), l = Low(p,T,1);
A1: now
assume card(Support p) < 1;
then Support p = {} by NAT_1:14;
then p = 0_(n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def 1;
end;
then Support u = Upper_Support(p,T,1) by Lm3;
then card(Support u) = 1 by A1,Def2;
then consider x being object such that
A2: Support u = {x} by CARD_2:42;
HT(p,T) in {x} by A1,A2,Th30;
then
A3: Support u = {HT(p,T)} by A2,TARSKI:def 1;
HM(p,T) <> 0_(n,L) by POLYNOM7:def 1;
then Support HM(p,T) <> {} by POLYNOM7:1;
then
A4: Support u = Support(HM(p,T)) by A3,TERMORD:21;
A5: now
let x be object;
assume x in dom HM(p,T);
then reconsider x9 = x as Element of Bags n;
now
per cases;
case
A6: x in Support HM(p,T);
then x9 = HT(p,T) by A3,A4,TARSKI:def 1;
hence (HM(p,T)).x9= p.x9 by TERMORD:18
.= u.x9 by A4,A6,Th16;
end;
case
A7: not x in Support HM(p,T);
hence (HM(p,T)).x9 = 0.L by POLYNOM1:def 4
.= u.x9 by A4,A7,POLYNOM1:def 4;
end;
end;
hence (HM(p,T)).x = u.x;
end;
dom HM(p,T) = Bags n by FUNCT_2:def 1
.= dom u by FUNCT_2:def 1;
hence HM(p,T) = u by A5,FUNCT_1:2;
then
A8: HM(p,T) + l = p by A1,Th33;
thus Red(p,T) = p - HM(p,T) by TERMORD:def 9
.= (l + HM(p,T)) + -HM(p,T) by A8,POLYNOM1:def 7
.= l + (HM(p,T) + -HM(p,T)) by POLYNOM1:21
.= l + 0_(n,L) by POLYRED:3
.= l by POLYRED:2;
end;
registration
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non trivial addLoopStr, p be non-zero
Polynomial of n,L;
cluster Up(p,T,0) -> monomial-like;
coherence
proof
Up(p,T,0) = 0_(n,L) by Th34;
hence thesis;
end;
end;
registration
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable Abelian non trivial doubleLoopStr, p be
non-zero Polynomial of n,L;
cluster Up(p,T,1) -> non-zero monomial-like;
coherence
proof
Up(p,T,1) = HM(p,T) by Th36;
hence thesis;
end;
cluster Low(p,T,card(Support p)) -> monomial-like;
coherence
proof
Low(p,T,card(Support p)) = 0_(n,L) by Th35;
hence thesis;
end;
end;
theorem Th37:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non trivial addLoopStr, p
being Polynomial of n,L, j being Element of NAT st j = card(Support p) - 1
holds Low(p,T,j) is non-zero Monomial of n,L
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non trivial addLoopStr, p be Polynomial of
n,L, j be Element of NAT;
set l = Low(p,T,j);
assume
A1: j = card(Support p) - 1;
A2: now
assume j > card(Support p);
then card(Support p) - 1 + 1 > card(Support p) + 1 by A1,XREAL_1:8;
then card(Support p) + -card(Support p) > (card(Support p) + 1) + -card(
Support p) by XREAL_1:8;
hence contradiction;
end;
then Support l = Lower_Support(p,T,j) by Lm3;
then card(Support l) = card(Support p) - (card(Support p) - 1) by A1,A2,Th24;
then consider x being object such that
A3: Support l = {x} by CARD_2:42;
x in Support l by A3,TARSKI:def 1;
then
A4: x is Element of Bags n;
l <> 0_(n,L) by A3,POLYNOM7:1;
hence thesis by A3,A4,POLYNOM7:6,def 1;
end;
theorem Th38:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds HT(Low(p,T,i+1),T) <= HT(Low(p,T,i),T), T
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT;
set li = Low(p,T,i), li1 = Low(p,T,i+1);
assume
A1: i < card(Support p);
then Support li = Lower_Support(p,T,i) by Lm3;
then
A2: card Support li = card(Support p) - i by A1,Th24;
A3: i + 1 <= card(Support p) by A1,NAT_1:13;
then
A4: Support li1 = Lower_Support(p,T,i+1) by Lm3;
then
A5: card Support li1 = card(Support p) - (i+1) by A3,Th24;
A6: Support li c= Support(p) by A1,Th26;
now
per cases;
case
i = card(Support p) - 1;
then card Support li1 = card(Support p) - card(Support p) by A4,Th24
.= 0;
then Support li1 = {};
then HT(li1,T) = EmptyBag n by TERMORD:def 6;
hence thesis by TERMORD:9;
end;
case
i <> card(Support p) - 1;
then card Lower_Support(p,T,i+1) <> 0 by A4,A5;
then Lower_Support(p,T,i+1) <> {};
then
A7: HT(Low(p,T,i+1),T) in Lower_Support(p,T,i+1) by A4,TERMORD:def 6;
now
assume HT(Low(p,T,i),T) < HT(Low(p,T,i+1),T), T;
then
A8: HT(Low(p,T,i),T) <= HT(Low(p,T,i+1),T), T by TERMORD:def 3;
now
let u9 be object;
assume
A9: u9 in Support li;
then reconsider u = u9 as Element of Bags n;
u <= HT(Low(p,T,i),T),T by A9,TERMORD:def 6;
hence u9 in Support li1 by A3,A6,A4,A7,A8,A9,Th24,TERMORD:8;
end;
then Support li c= Support li1;
then card(Support p) + -i <= card(Support p) + -(i+1) by A2,A5,NAT_1:43
;
then - i <= -(i + 1) by XREAL_1:6;
then i + 1 <= i by XREAL_1:24;
then (i + 1) - i <= i - i by XREAL_1:9;
then 1 <= 0;
hence contradiction;
end;
hence thesis by TERMORD:5;
end;
end;
hence thesis;
end;
theorem Th39:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 0 < i & i < card(Support p)
holds HT(Low(p,T,i),T) < HT(p,T),T
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
L, i be Element of NAT;
assume that
A1: 0 < i and
A2: i < card(Support p);
set l = Low(p,T,i);
now
per cases;
case
l = 0_(n,L);
then
A3: card Support l = 0 by CARD_1:27,POLYNOM7:1;
Support l = Lower_Support(p,T,i) by A2,Lm3;
then 0 + i = card(Support p) - i + i by A2,A3,Th24;
hence contradiction by A2;
end;
case
A4: l <> 0_(n,L);
A5: Support(Low(p,T,i)) c= Support(p) by A2,Th26;
A6: Support Low(p,T,i) = Lower_Support(p,T,i) by A2,Lm3;
A7: now
assume
A8: HT(p,T) in Support l;
A9: now
let u be object;
assume
A10: u in Support p;
then reconsider x = u as Element of Bags n;
x <= HT(p,T),T by A10,TERMORD:def 6;
hence u in Support l by A2,A6,A8,A10,Th24;
end;
for u being object holds u in Support l implies u in Support p by A5;
then card Support p = card Support l by A9,TARSKI:2
.= card(Support p) - i by A2,A6,Th24;
hence contradiction by A1;
end;
Support l <> {} by A4,POLYNOM7:1;
then
A11: HT(l,T) in Support l by TERMORD:def 6;
then HT(l,T) <= HT(p,T),T by A5,TERMORD:def 6;
hence thesis by A7,A11,TERMORD:def 3;
end;
end;
hence thesis;
end;
theorem Th40:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed well-unital
distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,
L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
Support p) for b being bag of n holds term(m) + b in Support Low(m*'p,T,i) iff
b in Support Low(p,T,i)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed well-unital distributive
domRing-like non trivial doubleLoopStr, p be Polynomial of n,L, m be non-zero
Monomial of n,L, i be Element of NAT;
set l = Low(p,T,i);
assume
A1: i <= card(Support p);
then
A2: Support l c= Support p by Th26;
A3: Support Up(p,T,i) = Upper_Support(p,T,i) by A1,Lm3;
then
A4: card(Support Up(p,T,i)) = i by A1,Def2;
A5: Support Up(p,T,i) c= Support(p) by A1,Th26;
A6: Support Low(p,T,i) = Lower_Support(p,T,i) by A1,Lm3;
let b be bag of n;
A7: i <= card Support(m*'p) by A1,Th10;
then
A8: Support Low(m*'p,T,i) = Lower_Support(m*'p,T,i) by Lm3;
A9: Support Low(m*'p,T,i) c= Support(m*'p) by A7,Th26;
A10: Support Up(m*'p,T,i) c= Support(m*'p) by A7,Th26;
A11: Support Up(m*'p,T,i) = Upper_Support(m*'p,T,i) by A7,Lm3;
then
A12: card(Support Up(m*'p,T,i)) = i by A7,Def2;
then
A13: Support Up(p,T,i) = {} implies Support Up(m*'p,T,i) = {} by A4;
A14: now
assume
A15: term(m) + b in Support Low(m*'p,T,i);
A16: now
assume term(m) + b in Support Up(m*'p,T,i);
then term(m) + b in Support(Up(m*'p,T,i)) /\ Support(Low(m*'p,T,i)) by
A15,XBOOLE_0:def 4;
hence contradiction by A7,A9,A15,Th28;
end;
A17: Support(m*'p) = { term(m) + u where u is Element of Bags n : u in
Support p } by Th9;
A18: now
defpred P[object,object] means $1 = term(m) + (In($2, Bags n));
assume
A19: b in Support Up(p,T,i);
A20: now
let b9 be bag of n;
assume
A21: term(m) + b9 in Support Up(m*'p,T,i);
then
A22: term(m) + b < term(m) + b9,T by A7,A11,A8,A15,Th20;
not b9 <= b,T by A22,TERMORD:5,Th2;
then b < b9,T by TERMORD:5;
then
A23: b <= b9,T by TERMORD:def 3;
b9 in Support(p) by A10,A21,Th8;
hence b9 in Support Up(p,T,i) by A1,A3,A19,A23,Def2;
end;
A24: for x being object st x in Support Up(m*'p,T,i)
ex y being object st y in Support Up(p,T,i) & P[x,y]
proof
let x be object;
assume
A25: x in Support Up(m*'p,T,i);
then x in Support(m*'p) by A10;
then consider x9 being Element of Bags n such that
A26: x = term(m) + x9 and
x9 in Support p by A17;
take x9;
thus thesis by A20,A25,A26;
end;
consider f being Function of Support Up(m*'p,T,i),Support Up(p,T,i) such
that
A27: for x being object st x in Support Up(m*'p,T,i) holds P[x,f.x]
from FUNCT_2:sch 1(A24);
now
let x1,x2 be object;
assume that
A28: x1 in dom f and
A29: x2 in dom f and
A30: f.x1 = f.x2;
f.x2 in rng f by A29,FUNCT_1:3;
then
A31: f.x2 in Support Up(p,T,i);
f.x1 in rng f by A28,FUNCT_1:3;
then f.x1 in Support Up(p,T,i);
then reconsider x19 = f.x1, x29 = f.x2 as Element of Bags n by A31;
A32: x19 = In(x19,Bags n);
x29 = In(x29,Bags n);
hence x1 = term(m) + x19 by A27,A28,A30
.= x2 by A27,A29,A30,A32;
end;
then
A33: f is one-to-one by FUNCT_1:def 4;
Support(Up(m*'p,T,i)) c= dom f by A13,FUNCT_2:def 1;
then Support(Up(m*'p,T,i)),f.:Support(Up(m*'p,T,i)) are_equipotent by A33
,CARD_1:33;
then card(f.:Support(Up(m*'p,T,i))) = card Support(Up(m*'p,T,i)) by
CARD_1:5
.= i by A7,A11,Def2;
then b in f.:Support(Up(m*'p,T,i)) by A4,A19,CARD_2:102;
then consider bb being object such that
A34: bb in dom f and
A35: bb in Support Up(m*'p,T,i) & f.bb = b by FUNCT_1:def 6;
f.bb in rng f by A34,FUNCT_1:3;
then f.bb in Support Up(p,T,i);
then reconsider bb9 = f.bb as Element of Bags n;
bb9 = In(bb9,Bags n);
hence contradiction by A16,A27,A35;
end;
term(m) + b in Support(m*'p) by A9,A15;
then term(m) + b in { term(m) + u where u is Element of Bags n : u in
Support p } by Th9;
then consider u being Element of Bags n such that
A36: term(m) + b = term(m) + u and
A37: u in Support p;
b = term(m) + b -' term(m) by PRE_POLY:48
.= u by A36,PRE_POLY:48;
hence b in Support Low(p,T,i) by A1,A37,A18,Th28;
end;
A38: Support Up(m*'p,T,i) = {} implies Support Up(p,T,i) = {} by A12,A4;
now
assume
A39: b in Support Low(p,T,i);
A40: now
assume b in Support Up(p,T,i);
then b in Support(Up(p,T,i)) /\ Support(Low(p,T,i)) by A39,XBOOLE_0:def 4
;
hence contradiction by A1,A2,A39,Th28;
end;
A41: now
defpred P[object,object] means $2 = term(m) + In($1,Bags n);
assume
A42: term(m) + b in Support Up(m*'p,T,i);
A43: now
let b9 be bag of n;
assume
A44: b9 in Support Up(p,T,i);
then term(m) + b < term(m) + b9,T by A1,A3,A6,A39,Th4,Th20;
then
A45: term(m) + b <= term(m) + b9,T by TERMORD:def 3;
term(m) + b9 in Support(m*'p) by A5,A44,Th8;
hence term(m) + b9 in Support Up(m*'p,T,i) by A7,A11,A42,A45,Def2;
end;
A46: for x being object st x in Support Up(p,T,i)
ex y being object st y in Support Up(m*'p,T,i) & P[x,y]
proof
let x be object;
assume
A47: x in Support Up(p,T,i);
then reconsider x9 = x as Element of Bags n;
take term(m) + x9;
thus thesis by A43,A47;
end;
consider f being Function of Support Up(p,T,i),Support Up(m*'p,T,i) such
that
A48: for x being object st x in Support Up(p,T,i) holds P[x,f.x] from
FUNCT_2:sch 1(A46);
now
let x1,x2 be object;
assume that
A49: x1 in dom f and
A50: x2 in dom f and
A51: f.x1 = f.x2;
x1 in Support Up(p,T,i) & x2 in Support Up(p,T,i) by A49,A50;
then reconsider x = x1, y = x2 as Element of Bags n;
y = In(y,Bags n);
then
A52: f.y = term(m) + y by A48,A50;
x = In(x,Bags n);
then
A53: f.x = term(m) + x by A48,A49;
thus x1 =term(m)+x-'term(m) by PRE_POLY:48
.= x2 by A51,A53,A52,PRE_POLY:48;
end;
then
A54: f is one-to-one by FUNCT_1:def 4;
Support(Up(p,T,i)) c= dom f by A38,FUNCT_2:def 1;
then Support(Up(p,T,i)),f.:Support(Up(p,T,i)) are_equipotent by A54,
CARD_1:33;
then card(f.:Support(Up(p,T,i))) = card Support(Up(p,T,i)) by CARD_1:5
.= i by A1,A3,Def2;
then term(m) + b in f.:Support(Up(p,T,i)) by A12,A42,CARD_2:102;
then consider bb being object such that
A55: bb in dom f and
A56: bb in Support Up(p,T,i) and
A57: f.bb = term(m) + b by FUNCT_1:def 6;
reconsider bb as Element of Bags n by A56;
bb = In(bb,Bags n);
then
A58: term(m) + bb = term(m) + b by A48,A55,A57;
bb = term(m) + bb -' term(m) by PRE_POLY:48
.= b by A58,PRE_POLY:48;
hence contradiction by A40,A55;
end;
term(m) + b in Support(m*'p) by A2,A39,Th8;
hence term(m) + b in Support Low(m*'p,T,i) by A7,A41,Th28;
end;
hence thesis by A14;
end;
theorem Th41:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Support Low(p,T,i+1) c= Support Low(p,T,i)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT;
set l = Low(p,T,i), l1 = Low(p,T,i+1);
assume
A1: i < card(Support p);
then
A2: i + 1 <= card(Support p) by NAT_1:13;
then
A3: card Support p - i >= 1 by XREAL_1:19;
A4: Support Low(p,T,i) = Lower_Support(p,T,i) by A1,Lm3;
then card Support l = card(Support p) - i by A1,Th24;
then
A5: HT(Low(p,T,i),T) in Lower_Support(p,T,i) by A3,A4,CARD_1:27,TERMORD:def 6;
A6: HT(Low(p,T,i+1),T) <= HT(Low(p,T,i),T), T by A1,Th38;
A7: Support(Low(p,T,i+1)) c= Support(p) by A2,Th26;
let u9 be object;
assume
A8: u9 in Support l1;
then reconsider u = u9 as Element of Bags n;
u <= HT(Low(p,T,i+1),T),T by A8,TERMORD:def 6;
hence u9 in Support l by A1,A7,A4,A6,A5,A8,Th24,TERMORD:8;
end;
theorem Th42:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non empty
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Support Low(p,T,i) \ Support Low(p,T,i+1) = {HT(Low(p,T,i),T)}
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT;
set l = Low(p,T,i), l1 = Low(p,T,i+1);
assume
A1: i < card(Support p);
then
A2: Support Low(p,T,i) = Lower_Support(p,T,i) by Lm3;
then
A3: card Support l = card(Support p) - i by A1,Th24;
now
assume Lower_Support(p,T,i) = {};
then card(Support p) - i = 0 by A1,Th24,CARD_1:27;
hence contradiction by A1;
end;
then
A4: HT(Low(p,T,i),T) in Support l by A2,TERMORD:def 6;
A5: Support(Low(p,T,i)) c= Support(p) by A1,Th26;
A6: i + 1 <= card(Support p) by A1,NAT_1:13;
then Support Low(p,T,i+1) = Lower_Support(p,T,i+1) by Lm3;
then
A7: card Support l1 = card(Support p) - (i+1) by A6,Th24;
then
card(Support Low(p,T,i) \ Support Low(p,T,i+1)) = (card(Support p) - i)
- (card(Support p) - (i+1)) by A1,A3,Th41,CARD_2:44
.= 1;
then consider x being object such that
A8: Support Low(p,T,i) \ Support Low(p,T,i+1) = {x} by CARD_2:42;
A9: Support Low(p,T,i+1) = Lower_Support(p,T,i+1) by A6,Lm3;
now
assume
A10: x <> HT(Low(p,T,i),T);
A11: now
assume not HT(Low(p,T,i),T) in Support l1;
then HT(Low(p,T,i),T) in Support l \ Support l1 by A4,XBOOLE_0:def 5;
hence contradiction by A8,A10,TARSKI:def 1;
end;
A12: now
let u be object;
assume
A13: u in Support l;
then reconsider u9 = u as Element of Bags n;
u9 <= HT(Low(p,T,i),T),T by A13,TERMORD:def 6;
hence u in Support l1 by A6,A5,A9,A11,A13,Th24;
end;
Support Low(p,T,i+1) c= Support Low(p,T,i) by A1,Th41;
then for u being object holds u in Support l1 implies u in Support l;
then card(Support p) + -i <= card(Support p) + -(i+1) by A3,A7,A12,TARSKI:2
;
then - i <= -(i + 1) by XREAL_1:6;
then i + 1 <= i by XREAL_1:24;
then (i + 1) - i <= i - i by XREAL_1:9;
then 1 <= 0;
hence contradiction;
end;
hence thesis by A8;
end;
theorem Th43:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_zeroed right_complementable non trivial
addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Low(p,T,i+1) = Red(Low(p,T,i),T)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_zeroed right_complementable non trivial addLoopStr, p
be Polynomial of n,L, i be Element of NAT;
set l = Low(p,T,i), l1 = Low(p,T,i+1), r = Red(l,T);
assume
A1: i < card(Support p);
then
A2: Support(Low(p,T,i)) c= Support(p) by Th26;
Support Low(p,T,i) = Lower_Support(p,T,i) by A1,Lm3;
then
A3: card Support l = card(Support p) - i by A1,Th24;
A4: Support(Low(p,T,i+1)) c= Support(Low(p,T,i)) by A1,Th41;
A5: i + 1 <= card(Support p) by A1,NAT_1:13;
then Support Low(p,T,i+1) = Lower_Support(p,T,i+1) by Lm3;
then
A6: card Support l1 = card(Support p) - (i+1) by A5,Th24;
A7: Support Low(p,T,i+1) = Lower_Support(p,T,i+1) by A5,Lm3;
now
set u = the Element of {HT(l,T)} /\ Support l1;
assume
A8: {HT(l,T)} /\ Support l1 <> {};
then u in {HT(l,T)} by XBOOLE_0:def 4;
then
A9: u = HT(l,T) by TARSKI:def 1;
A10: u in Support l1 by A8,XBOOLE_0:def 4;
now
let u9 be object;
assume
A11: u9 in Support l;
then reconsider u = u9 as Element of Bags n;
u <= HT(Low(p,T,i),T),T by A11,TERMORD:def 6;
hence u9 in Support l1 by A5,A2,A7,A10,A9,A11,Th24;
end;
then Support l c= Support l1;
then card(Support p) + -i <= card(Support p) + -(i+1) by A3,A6,NAT_1:43;
then - i <= -(i + 1) by XREAL_1:6;
then i + 1 <= i by XREAL_1:24;
then (i + 1) - i <= i - i by XREAL_1:9;
then 1 <= 0;
hence contradiction;
end;
then
A12: Support l1 misses {HT(l,T)} by XBOOLE_0:def 7;
A13: Support Low(p,T,i) \ Support Low(p,T,i+1) = {HT(Low(p,T,i),T)} by A1,Th42;
then Support Low(p,T,i) = Support l1 \/ {HT(l,T)} by A1,Th41,XBOOLE_1:45;
then
A14: Support r = (Support l1 \/ {HT(l,T)}) \ {HT(l,T)} by TERMORD:36
.= Support l1 \ {HT(l,T)} by XBOOLE_1:40
.= Support l1 by A12,XBOOLE_1:83;
A15: now
let x be object;
assume x in dom l1;
then reconsider b = x as Element of Bags n;
now
per cases;
case
A16: b in Support l1;
then not b in {HT(Low(p,T,i),T)} by A13,XBOOLE_0:def 5;
then
A17: b <> HT(l,T) by TARSKI:def 1;
thus l1.b = p.b by A5,A16,Th31
.= l.b by A1,A4,A16,Th31
.= r.b by A4,A16,A17,TERMORD:40;
end;
case
A18: not b in Support l1;
hence l1.b = 0.L by POLYNOM1:def 4
.= r.b by A14,A18,POLYNOM1:def 4;
end;
end;
hence l1.x = r.x;
end;
dom l1 = Bags n by FUNCT_2:def 1
.= dom r by FUNCT_2:def 1;
hence thesis by A15,FUNCT_1:2;
end;
theorem Th44:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed well-unital
distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,
L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
Support p) holds Low(m*'p,T,i) = m *' Low(p,T,i)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed well-unital distributive
domRing-like non trivial doubleLoopStr, p be Polynomial of n,L, m be non-zero
Monomial of n,L, i be Element of NAT;
set l = Low(p,T,i), lm = Low(m*'p,T,i);
assume
A1: i <= card(Support p);
then
A2: i <= card(Support(m*'p)) by Th10;
A3: Support(m*'l) c= {s + t where s,t is Element of Bags n : s in Support m
& t in Support l} by TERMORD:30;
A4: now
m <> 0_(n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then
A5: Support m = {term(m)} by POLYNOM7:7;
then term(m) in Support m by TARSKI:def 1;
then
A6: m.term(m) <> 0.L by POLYNOM1:def 4;
let u be object;
assume
A7: u in Support m*'l;
then reconsider u9 = u as Element of Bags n;
u in {s + t where s,t is Element of Bags n : s in Support m & t in
Support l} by A3,A7;
then consider s,t being Element of Bags n such that
A8: u9 = s + t and
A9: s in Support m and
A10: t in Support l;
A11: l.t <> 0.L by A10,POLYNOM1:def 4;
A12: term(m) = s by A9,A5,TARSKI:def 1;
then (m*'p).u9 = m.term(m) * p.t by A8,POLYRED:7
.= m.term(m) * l.t by A1,A10,Th31;
then (m*'p).u9 <> 0.L by A11,A6,VECTSP_2:def 1;
then
A13: u9 in Support(m*'p) by POLYNOM1:def 4;
now
assume not s+t in Support Low(m*'p,T,i);
then
A14: s+t in Support Up(m*'p,T,i) by A2,A8,A13,Th28;
now
let t9 be bag of n;
assume t9 in Support Low(p,T,i);
then s+t9 in Support Low(m*'p,T,i) by A1,A12,Th40;
then
A15: s+t9 < s+t,T by A2,A14,Th29;
not t <= t9,T by A15,TERMORD:5,Th2;
hence t9 < t,T by TERMORD:5;
end;
then t < t,T by A10;
hence contradiction by TERMORD:def 3;
end;
hence u in Support lm by A8;
end;
A16: Support(m*'p) c= {s + t where s,t is Element of Bags n : s in Support m
& t in Support p} by TERMORD:30;
now
let u be object;
assume
A17: u in Support Low(m*'p,T,i);
then reconsider u9 = u as Element of Bags n;
Support Low(m*'p,T,i) c= Support(m*'p) by A2,Th26;
then u9 in Support(m*'p) by A17;
then
A18: u9 in {s + t where s,t is Element of Bags n : s in Support m & t in
Support p} by A16;
m <> 0_(n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then
A19: Support m = {term(m)} by POLYNOM7:7;
then term(m) in Support m by TARSKI:def 1;
then
A20: m.term(m) <> 0.L by POLYNOM1:def 4;
consider s,t being Element of Bags n such that
A21: u = s + t and
A22: s in Support m and
A23: t in Support p by A18;
A24: p.t <> 0.L by A23,POLYNOM1:def 4;
A25: term(m) = s by A22,A19,TARSKI:def 1;
then
A26: t in Support l by A1,A17,A21,Th40;
(m*'l).(term(m)+t) = m.term(m) * l.t by POLYRED:7
.= m.term(m) * p.t by A1,A26,Th31;
then (m*'l).u9 <> 0.L by A21,A20,A25,A24,VECTSP_2:def 1;
hence u in Support(m*'Low(p,T,i)) by POLYNOM1:def 4;
end;
then
A27: Support(m*'l) = Support lm by A4,TARSKI:2;
A28: now
let x be object;
assume x in dom(m*'l);
then reconsider b = x as Element of Bags n;
now
per cases;
case
A29: b in Support(m*'l);
then
A30: b in {s + t where s,t is Element of Bags n : s in Support m & t
in Support l} by A3;
A31: b in Support lm by A4,A29;
consider s,t being Element of Bags n such that
A32: b = s + t and
A33: s in Support m and
A34: t in Support l by A30;
Support m = {term(m)} by A33,POLYNOM7:7;
then
A35: term(m) = s by A33,TARSKI:def 1;
hence (m*'l).b = m.term(m) * l.t by A32,POLYRED:7
.= m.term(m) * p.t by A1,A34,Th31
.= (m*'p).b by A32,A35,POLYRED:7
.= lm.b by A2,A31,Th31;
end;
case
A36: not b in Support(m*'l);
hence (m*'l).b = 0.L by POLYNOM1:def 4
.= lm.b by A27,A36,POLYNOM1:def 4;
end;
end;
hence (m*'l).x = lm.x;
end;
dom(m*'l) = Bags n by FUNCT_2:def 1
.= dom lm by FUNCT_2:def 1;
hence thesis by A28,FUNCT_1:2;
end;
begin :: More on Polynomial Reduction
Lm4: 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 Subset of Polynom-Ring(n,L), R being RedSequence of PolyRedRel(P,T), i
being Element of NAT st 1 <= i & i <= len R & len R > 1 holds R.i 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, P be Subset of
Polynom-Ring(n,L), R be RedSequence of PolyRedRel(P,T), i be Element of NAT;
assume that
A1: 1 <= i and
A2: i <= len R and
A3: 1 < len R;
A4: i in dom R by A1,A2,FINSEQ_3:25;
now
per cases;
case
i <> len R;
then i < len R by A2,XXREAL_0:1;
then 1 <= i + 1 & i + 1 <= len R by NAT_1:11,13;
then i + 1 in dom R by FINSEQ_3:25;
then [R.i,R.(i+1)] in PolyRedRel(P,T) by A4,REWRITE1:def 2;
then R.i in dom PolyRedRel(P,T) by XTUPLE_0:def 12;
then R.i in the carrier of Polynom-Ring(n,L) by XBOOLE_0:def 5;
hence thesis by POLYNOM1:def 11;
end;
case
A5: i = len R;
A6: i - 1 is Element of NAT by A1,INT_1:5;
1 + -1 < i + -1 by A3,A5,XREAL_1:8;
then
A7: 1 <= i - 1 by A6,NAT_1:14;
A8: i = (i - 1) + 1;
i - 1 <= len R by A5,XREAL_1:146;
then i - 1 in dom R by A6,A7,FINSEQ_3:25;
then [R.(i-1),R.i] in PolyRedRel(P,T) by A4,A8,REWRITE1:def 2;
then R.i in rng PolyRedRel(P,T) by XTUPLE_0:def 13;
hence thesis by POLYNOM1:def 11;
end;
end;
hence thesis;
end;
theorem Th45:
for n being Ordinal, 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
trivial doubleLoopStr, f,g,p being Polynomial of n,L st f reduces_to g,p,T
holds -f reduces_to -g,p,T
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g,p be Polynomial of n,L;
assume f reduces_to g,p,T;
then consider b being bag of n such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
b in Support f by A1,POLYRED:def 5;
then
A2: b in Support -f by GROEB_1:5;
consider s being bag of n such that
A3: s + HT(p,T) = b and
A4: g = f - (f.b/HC(p,T)) * (s *' p) by A1,POLYRED:def 5;
g = f + (-((f.b/HC(p,T)) * (s *' p))) by A4,POLYNOM1:def 7;
then
A5: -g = -f + -(-((f.b/HC(p,T)) * (s *' p))) by POLYRED:1
.= -f - -((f.b/HC(p,T)) * (s *' p)) by POLYNOM1:def 7
.= -f - (-(f.b/HC(p,T))) * (s *' p) by POLYRED:9
.= -f - (-(f.b*(HC(p,T))")) * (s *' p)
.= -f - ((-f.b)*(HC(p,T))") * (s *' p) by VECTSP_1:9
.= -f - ((-f.b)/(HC(p,T))) * (s *' p)
.= -f - ((-f).b/HC(p,T)) * (s *' p) by POLYNOM1:17;
A6: now
A7: --f = f by POLYNOM1:19;
assume -f = 0_(n,L);
then f = -(0_(n,L)) by A7 .= 0_(n,L) by Th13;
hence contradiction by A1,POLYRED:def 5;
end;
p <> 0_(n,L) by A1,POLYRED:def 5;
then -f reduces_to -g,p,b,T by A3,A6,A5,A2,POLYRED:def 5;
hence thesis by POLYRED:def 6;
end;
Lm5: for n being Ordinal, T being connected admissible TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint for b1,b2 being
bag of n st b1 in Support p1 & b2 in Support p2 holds not(b1 = HT(p1,T) & b2 =
HT(p2,T)) implies not(HT(p1,T) + b2 = HT(p2,T) + b1)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 be Polynomial of n,L;
assume
A1: HT(p1,T),HT(p2,T) are_disjoint;
let b1,b2 be bag of n;
assume that
A2: b1 in Support p1 and
A3: b2 in Support p2;
assume
A4: not(b1 = HT(p1,T) & b2 = HT(p2,T));
b2 <= HT(p2,T),T by A3,TERMORD:def 6;
then
A5: HT(p1,T) + b2 <= HT(p1,T) + HT(p2,T),T by Th2;
b1 <= HT(p1,T),T by A2,TERMORD:def 6;
then
A6: HT(p2,T) + b1 <= HT(p1,T) + HT(p2,T),T by Th2;
assume
A7: HT(p1,T) + b2 = HT(p2,T) + b1;
then
A8: HT(p1,T) divides HT(p2,T) + b1 by PRE_POLY:50;
A9: HT(p2,T) divides HT(p1,T) + b2 by A7,PRE_POLY:50;
now
per cases by A4;
case
A10: not b1 = HT(p1,T);
HT(p2,T) divides HT(p2,T) + b1 by PRE_POLY:50;
then lcm(HT(p1,T),HT(p2,T)) divides HT(p2,T) + b1 by A8,GROEB_2:4;
then HT(p1,T) + HT(p2,T) divides HT(p2,T) + b1 by A1,GROEB_2:5;
then HT(p1,T) + HT(p2,T) <= HT(p2,T) + b1,T by TERMORD:10;
then
A11: HT(p1,T) + HT(p2,T) = HT(p2,T) + b1 by A6,TERMORD:7;
HT(p1,T) = HT(p1,T) + HT(p2,T) -' HT(p2,T) by PRE_POLY:48;
hence contradiction by A10,A11,PRE_POLY:48;
end;
case
A12: not b2 = HT(p2,T);
HT(p1,T) divides HT(p1,T) + b2 by PRE_POLY:50;
then lcm(HT(p1,T),HT(p2,T)) divides HT(p1,T) + b2 by A9,GROEB_2:4;
then HT(p1,T) + HT(p2,T) divides HT(p1,T) + b2 by A1,GROEB_2:5;
then HT(p1,T) + HT(p2,T) <= HT(p1,T) + b2,T by TERMORD:10;
then
A13: HT(p1,T) + HT(p2,T) = HT(p1,T) + b2 by A5,TERMORD:7;
HT(p2,T) = HT(p1,T) + HT(p2,T) -' HT(p1,T) by PRE_POLY:48;
hence contradiction by A12,A13,PRE_POLY:48;
end;
end;
hence thesis;
end;
theorem Th46:
for n being Ordinal, 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
trivial doubleLoopStr, f,f1,g,p being Polynomial of n,L st f reduces_to f1,{p}
,T & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
holds f + g reduces_to f1 + g,{p},T
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,f1,g,p be Polynomial of n,L;
assume that
A1: f reduces_to f1,{p},T and
A2: for b1 being bag of n st b1 in Support g holds not HT(p,T) divides b1;
consider q being Polynomial of n,L such that
A3: q in {p} and
A4: f reduces_to f1,q,T by A1,POLYRED:def 7;
p = q by A3,TARSKI:def 1;
then consider br being bag of n such that
A5: f reduces_to f1,p,br,T by A4,POLYRED:def 6;
consider s being bag of n such that
A6: s + HT(p,T) = br and
A7: f1 = f -(f.br/HC(p,T))*(s*'p) by A5,POLYRED:def 5;
A8: not br in Support g by A6,TERMORD:1,A2;
A9: br is Element of Bags n by PRE_POLY:def 12;
A10: p in {p} by TARSKI:def 1;
A11: br in Support f by A5,POLYRED:def 5;
A12: (f+g).br = f.br + g.br by POLYNOM1:15
.= f.br + 0.L by A8,A9,POLYNOM1:def 4
.= f.br by RLVECT_1:def 4;
A13: p <> 0_(n,L) by A5,POLYRED:def 5;
now
per cases;
case
f + g = 0_(n,L);
then (f + g) - f = -f by Th14;
then (f + g) + -f = -f by POLYNOM1:def 7;
then (f + -f) + g = -f by POLYNOM1:21;
then 0_(n,L) + g = -f by POLYRED:3;
then g = -f by POLYRED:2;
hence contradiction by A11,A8,GROEB_1:5;
end;
case
A14: f + g <> 0_(n,L);
set g1 = (f+g) - ((f+g).br/HC(p,T))*(s*'p);
(f+g).br <> 0.L by A11,A12,POLYNOM1:def 4;
then br in Support(f+g) by A11,POLYNOM1:def 4;
then f+g reduces_to g1,p,br,T by A13,A6,A14,POLYRED:def 5;
then
A15: f+g reduces_to g1,p,T by POLYRED:def 6;
g1 = (f+g) + (-((f.br/HC(p,T))*(s*'p))) by A12,POLYNOM1:def 7
.= (f + -((f.br/HC(p,T))*(s*'p))) + g by POLYNOM1:21
.= f1 + g by A7,POLYNOM1:def 7;
hence thesis by A10,A15,POLYRED:def 7;
end;
end;
hence thesis;
end;
theorem Th47:
for n being Ordinal, 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
trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds f*'g
reduces_to Red(f,T)*'g,{g},T
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g be non-zero Polynomial of n,L;
set fg = f*'g;
set q = fg - (fg.HT(fg,T)/HC(g,T)) * (HT(f,T) *' g);
reconsider r = -HM(f,T) as Polynomial of n,L;
A1: g <> 0_(n,L) by POLYNOM7:def 1;
A2: HC(g,T) <> 0.L;
A3: fg <> 0_(n,L) by POLYNOM7:def 1;
then Support fg <> {} by POLYNOM7:1;
then
A4: HT(fg,T) in Support fg by TERMORD:def 6;
HT(fg,T) = HT(f,T) + HT(g,T) by TERMORD:31;
then fg reduces_to q,g,HT(fg,T),T by A3,A1,A4,POLYRED:def 5;
then
A5: g in {g} & fg reduces_to q,g,T by POLYRED:def 6,TARSKI:def 1;
q = fg - (HC(fg,T)/HC(g,T)) * (HT(f,T) *' g) by TERMORD:def 7
.= fg - ((HC(f,T)*HC(g,T))/HC(g,T)) * (HT(f,T) *' g) by TERMORD:32
.= fg - ((HC(f,T)*HC(g,T))*HC(g,T)") * (HT(f,T) *' g)
.= fg - (HC(f,T)*(HC(g,T)*HC(g,T)")) * (HT(f,T) *' g) by GROUP_1:def 3
.= fg - (HC(f,T)*1.L) * (HT(f,T) *' g) by A2,VECTSP_1:def 10
.= fg - HC(f,T) * (HT(f,T) *' g)
.= fg - Monom(HC(f,T),HT(f,T)) *' g by POLYRED:22
.= fg - HM(f,T) *' g by TERMORD:def 8
.= fg + -(HM(f,T) *' g) by POLYNOM1:def 7
.= fg + (r *' g) by POLYRED:6
.= g *' (f + -HM(f,T)) by POLYNOM1:26
.= (f - HM(f,T)) *' g by POLYNOM1:def 7
.= Red(f,T) *' g by TERMORD:def 9;
hence thesis by A5,POLYRED:def 7;
end;
theorem
for n being Ordinal, 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 trivial
doubleLoopStr, f,g being non-zero Polynomial of n,L, p being Polynomial of n,L
st p.(HT(f*'g,T)) = 0.L holds f*'g+p reduces_to Red(f,T)*'g+p,{g},T
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g be non-zero Polynomial of n,L, p be Polynomial of n,L;
assume
A1: p.(HT(f*'g,T)) = 0.L;
f*'g <> 0_(n,L) by POLYNOM7:def 1;
then Support(f*'g) <> {} by POLYNOM7:1;
then HT(f*'g,T) in Support(f*'g) by TERMORD:def 6;
then
A2: (f*'g).HT(f*'g,T) <> 0.L by POLYNOM1:def 4;
reconsider r = -HM(f,T) as Polynomial of n,L;
set fg = f*'g+p;
set q = fg - ((fg).HT(f*'g,T)/HC(g,T)) * (HT(f,T) *' g);
A3: HT(f*'g,T) = HT(f,T) + HT(g,T) by TERMORD:31;
A4: g <> 0_(n,L) by POLYNOM7:def 1;
A5: HC(g,T) <> 0.L;
fg.(HT(f*'g,T)) = (f*'g).HT(f*'g,T) + p.HT(f*'g,T) by POLYNOM1:15
.= (f*'g).HT(f*'g,T) by A1,RLVECT_1:def 4;
then
A6: HT(f*'g,T) in Support fg by A2,POLYNOM1:def 4;
then fg <> 0_(n,L) by POLYNOM7:1;
then fg reduces_to q,g,HT(f*'g,T),T by A6,A4,A3,POLYRED:def 5;
then
A7: g in {g} & fg reduces_to q,g,T by POLYRED:def 6,TARSKI:def 1;
q = fg - (((f*'g).HT(f*'g,T)+0.L)/HC(g,T)) * (HT(f,T) *' g) by A1,POLYNOM1:15
.= fg - ((f*'g).HT(f*'g,T)/HC(g,T)) * (HT(f,T) *' g) by RLVECT_1:def 4
.= fg - (HC(f*'g,T)/HC(g,T)) * (HT(f,T) *' g) by TERMORD:def 7
.= fg - ((HC(f,T)*HC(g,T))/HC(g,T)) * (HT(f,T) *' g) by TERMORD:32
.= fg - ((HC(f,T)*HC(g,T))*HC(g,T)") * (HT(f,T) *' g)
.= fg - (HC(f,T)*(HC(g,T)*HC(g,T)")) * (HT(f,T) *' g) by GROUP_1:def 3
.= fg - (HC(f,T)*1.L) * (HT(f,T) *' g) by A5,VECTSP_1:def 10
.= fg - HC(f,T) * (HT(f,T) *' g)
.= fg - Monom(HC(f,T),HT(f,T)) *' g by POLYRED:22
.= fg - HM(f,T) *' g by TERMORD:def 8
.= fg + -(HM(f,T) *' g) by POLYNOM1:def 7
.= (f*'g+p) + (r *' g) by POLYRED:6
.= (f*'g + r *' g) + p by POLYNOM1:21
.= g *' (f + -HM(f,T)) + p by POLYNOM1:26
.= (f - HM(f,T)) *' g + p by POLYNOM1:def 7
.= Red(f,T) *' g + p by TERMORD:def 9;
hence thesis by A7,POLYRED:def 7;
end;
theorem Th49:
for n being Ordinal, 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
trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g being Polynomial
of n,L st PolyRedRel(P,T) reduces f,g holds PolyRedRel(P,T) reduces -f,-g
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P be Subset of Polynom-Ring(n,L), f,g be Polynomial of n,L;
assume PolyRedRel(P,T) reduces f,g;
then consider R being RedSequence of PolyRedRel(P,T) such that
A1: R.1 = f and
A2: R.len R = g by REWRITE1:def 3;
defpred P[Nat] means for q being Polynomial of n,L st q = R.$1
holds PolyRedRel(P,T) reduces -f,-q;
A3: 1 <= len R by NAT_1:14;
A4: now
let k be Element of NAT;
assume
A5: 1 <= k & k < len R;
then 1 < len R by XXREAL_0:2;
then reconsider p = R.k as Polynomial of n,L by A5,Lm4;
assume P[k];
then
A6: PolyRedRel(P,T) reduces -f,-p;
now
let q be Polynomial of n,L;
assume
A7: q = R.(k+1);
1 <= k+1 & k+1 <= len R by A5,NAT_1:13;
then
A8: k+1 in dom R by FINSEQ_3:25;
k in dom R by A5,FINSEQ_3:25;
then [R.k, R.(k+1)] in PolyRedRel(P,T) by A8,REWRITE1:def 2;
then p reduces_to q,P,T by A7,POLYRED:def 13;
then consider l being Polynomial of n,L such that
A9: l in P and
A10: p reduces_to q,l,T by POLYRED:def 7;
-p reduces_to -q,l,T by A10,Th45;
then -p reduces_to -q,P,T by A9,POLYRED:def 7;
then [-p,-q] in PolyRedRel(P,T) by POLYRED:def 13;
then PolyRedRel(P,T) reduces -p,-q by REWRITE1:15;
hence PolyRedRel(P,T) reduces -f,-q by A6,REWRITE1:16;
end;
hence P[k+1];
end;
A11: P[1] by A1,REWRITE1:12;
for i being Element of NAT st 1<=i & i<=len R holds P[i] from
INT_1:sch 7(A11,A4);
hence thesis by A2,A3;
end;
theorem
for n being Ordinal, 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 trivial
doubleLoopStr, f,f1,g,p being Polynomial of n,L st PolyRedRel({p},T) reduces f
,f1 & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
holds PolyRedRel({p},T) reduces f+g,f1+g
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,f1,g,p be Polynomial of n,L;
assume that
A1: PolyRedRel({p},T) reduces f,f1 and
A2: for b1 being bag of n st b1 in Support g holds not HT(p,T) divides b1;
consider R being RedSequence of PolyRedRel({p},T) such that
A3: R.1 = f and
A4: R.len R = f1 by A1,REWRITE1:def 3;
defpred P[Nat] means for q being Polynomial of n,L st q = R.$1
holds PolyRedRel({p},T) reduces f+g,q+g;
A5: now
let k be Element of NAT;
assume
A6: 1 <= k & k < len R;
then 1 < len R by XXREAL_0:2;
then reconsider h = R.k as Polynomial of n,L by A6,Lm4;
assume P[k];
then
A7: PolyRedRel({p},T) reduces f+g,h+g;
now
let q be Polynomial of n,L;
assume
A8: q = R.(k+1);
1 <= k+1 & k+1 <= len R by A6,NAT_1:13;
then
A9: k+1 in dom R by FINSEQ_3:25;
k in dom R by A6,FINSEQ_3:25;
then [R.k, R.(k+1)] in PolyRedRel({p},T) by A9,REWRITE1:def 2;
then h reduces_to q,{p},T by A8,POLYRED:def 13;
then h+g reduces_to q+g,{p},T by A2,Th46;
then [h+g,q+g] in PolyRedRel({p},T) by POLYRED:def 13;
then PolyRedRel({p},T) reduces h+g,q+g by REWRITE1:15;
hence PolyRedRel({p},T) reduces f+g,q+g by A7,REWRITE1:16;
end;
hence P[k+1];
end;
A10: 1 <= len R by NAT_1:14;
A11: P[1] by A3,REWRITE1:12;
for i being Element of NAT st 1<=i & i<=len R holds P[i] from
INT_1:sch 7(A11,A5);
hence thesis by A4,A10;
end;
theorem Th51:
for n being Ordinal, 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
trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds PolyRedRel({
g},T) reduces f*'g,0_(n,L)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g be non-zero Polynomial of n,L;
defpred P[Nat] means for f being Polynomial of n,L st card(
Support f) = $1 holds PolyRedRel({g},T) reduces f*'g,0_(n,L);
A1: ex n being Element of NAT st card(Support f) = n;
A2: now
let k be Nat;
assume
A3: P[k];
now
let f be Polynomial of n,L;
set rf = Red(f,T);
assume
A4: card(Support f) = k+1;
now
assume f = 0_(n,L);
then Support f = {} by POLYNOM7:1;
hence contradiction by A4;
end;
then reconsider f1 = f as non-zero Polynomial of n,L by POLYNOM7:def 1;
f1*'g reduces_to rf*'g,{g},T by Th47;
then [f1*'g,rf*'g] in PolyRedRel({g},T) by POLYRED:def 13;
then
A5: PolyRedRel({g},T) reduces f*'g,rf*'g by REWRITE1:15;
f1 <> 0_(n,L) by POLYNOM7:def 1;
then Support f <> {} by POLYNOM7:1;
then HT(f,T) in Support f by TERMORD:def 6;
then for u being object st u in {HT(f,T)} holds u in Support f by
TARSKI:def 1;
then
A6: {HT(f,T)} c= Support f;
Support rf = Support(f) \ {HT(f,T)} by TERMORD:36;
then card(Support rf) = card(Support f) - card({HT(f,T)}) by A6,CARD_2:44
.= (k + 1) - 1 by A4,CARD_1:30
.= k + 0;
then PolyRedRel({g},T) reduces rf*'g,0_(n,L) by A3;
hence PolyRedRel({g},T) reduces f*'g,0_(n,L) by A5,REWRITE1:16;
end;
hence P[k+1];
end;
now
let f be Polynomial of n,L;
assume card(Support f) = 0;
then Support f = {};
then f = 0_(n,L) by POLYNOM7:1;
then f*'g = 0_(n,L) by POLYRED:5;
hence PolyRedRel({g},T) reduces f*'g,0_(n,L) by REWRITE1:12;
end;
then
A7: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A7,A2);
hence thesis by A1;
end;
begin :: The Criterium
theorem Th52:
for n being Ordinal, T being connected admissible TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
for b1,b2 being bag of n st b1 in Support Red(p1,T) & b2 in Support Red(p2,T)
holds not(HT(p1,T) + b2 = HT(p2,T) + b1)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 be Polynomial of n,L;
assume
A1: HT(p1,T),HT(p2,T) are_disjoint;
A2: Support(Red(p1,T)) c= Support(p1) & Support(Red(p2,T)) c= Support(p2) by
TERMORD:35;
let b1,b2 be bag of n;
assume that
A3: b1 in Support Red(p1,T) and
A4: b2 in Support Red(p2,T);
now
assume b1 = HT(p1,T);
then Red(p1,T).b1 = 0.L by TERMORD:39;
hence contradiction by A3,POLYNOM1:def 4;
end;
hence thesis by A1,A3,A4,A2,Lm5;
end;
theorem Th53:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
holds S-Poly(p1,p2,T) = HM(p2,T) *' Red(p1,T) - HM(p1,T) *' Red(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 Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2
be Polynomial of n,L;
assume HT(p1,T),HT(p2,T) are_disjoint;
then lcm(HT(p1,T),HT(p2,T)) = HT(p1,T) + HT(p2,T) by GROEB_2:5;
hence S-Poly(p1,p2,T) = HC(p2,T) * ((HT(p1,T) + HT(p2,T))/HT(p1,T)) *' p1 -
HC(p1,T) * ((HT(p1,T) + HT(p2,T))/HT(p2,T)) *' p2 by GROEB_2:def 4
.= HC(p2,T) * HT(p2,T) *' p1 - HC(p1,T) * ((HT(p1,T) + HT(p2,T))/HT(p2,T
)) *' p2 by Th1
.= HC(p2,T) * HT(p2,T) *' p1 - HC(p1,T) * HT(p1,T) *' p2 by Th1
.= HC(p2,T) * HT(p2,T) *' (HM(p1,T) + Red(p1,T)) - HC(p1,T) * HT(p1,T)
*' p2 by TERMORD:38
.= HC(p2,T) * HT(p2,T) *' (HM(p1,T) + Red(p1,T)) - HC(p1,T) * HT(p1,T)
*' (HM(p2,T) + Red(p2,T)) by TERMORD:38
.= Monom(HC(p2,T),HT(p2,T)) *' (HM(p1,T) + Red(p1,T)) - HC(p1,T) * HT(p1
,T) *' (HM(p2,T) + Red(p2,T)) by POLYRED:22
.= Monom(HC(p2,T),HT(p2,T)) *' (HM(p1,T) + Red(p1,T)) - Monom(HC(p1,T),
HT(p1,T)) *' (HM(p2,T) + Red(p2,T)) by POLYRED:22
.= HM(p2,T) *' (HM(p1,T) + Red(p1,T)) - Monom(HC(p1,T),HT(p1,T)) *' (HM(
p2,T) + Red(p2,T)) by TERMORD:def 8
.= HM(p2,T) *' (HM(p1,T) + Red(p1,T)) - HM(p1,T) *' (HM(p2,T) + Red(p2,T
)) by TERMORD:def 8
.= (HM(p2,T) *' HM(p1,T) + HM(p2,T) *' Red(p1,T)) - HM(p1,T) *' (HM(p2,T
) + Red(p2,T)) by POLYNOM1:26
.= (HM(p2,T) *' HM(p1,T) + HM(p2,T) *' Red(p1,T)) - (HM(p1,T) *' HM(p2,T
) + HM(p1,T) *' Red(p2,T)) by POLYNOM1:26
.= (HM(p2,T) *' HM(p1,T) + HM(p2,T) *' Red(p1,T)) + -((HM(p1,T) *' HM(p2
,T)) + (HM(p1,T) *' Red(p2,T))) by POLYNOM1:def 7
.= (HM(p2,T) *' HM(p1,T) + HM(p2,T) *' Red(p1,T)) + (-(HM(p1,T) *' HM(p2
,T)) + -(HM(p1,T) *' Red(p2,T))) by POLYRED:1
.= HM(p2,T) *' Red(p1,T) + (HM(p2,T) *' HM(p1,T) + (-(HM(p1,T) *' HM(p2,
T)) + -(HM(p1,T) *' Red(p2,T)))) by POLYNOM1:21
.= HM(p2,T) *' Red(p1,T) + ((HM(p2,T) *' HM(p1,T) + -(HM(p1,T) *' HM(p2,
T))) + -(HM(p1,T) *' Red(p2,T))) by POLYNOM1:21
.= HM(p2,T) *' Red(p1,T) + (0_(n,L) + -(HM(p1,T) *' Red(p2,T))) by
POLYRED:3
.= HM(p2,T) *' Red(p1,T) + -(HM(p1,T) *' Red(p2,T)) by POLYRED:2
.= HM(p2,T) *' Red(p1,T) - (HM(p1,T) *' Red(p2,T)) by POLYNOM1:def 7;
end;
theorem Th54:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
holds S-Poly(p1,p2,T) = Red(p1,T) *' p2 - Red(p2,T) *' p1
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2
be Polynomial of n,L;
reconsider r1 = -Red(p1,T), r2 = -Red(p2,T) as Polynomial of n,L;
r2 *' Red(p1,T) = -(Red(p2,T) *' Red(p1,T)) by POLYRED:6
.= r1 *' Red(p2,T) by POLYRED:6;
then
A1: (r2 *' Red(p1,T) + -(r1 *' Red(p2,T))) = 0_(n,L) by POLYRED:3;
assume HT(p1,T),HT(p2,T) are_disjoint;
hence S-Poly(p1,p2,T) = HM(p2,T) *' Red(p1,T) - (HM(p1,T) *' Red(p2,T)) by
Th53
.= (p2 - Red(p2,T)) *' Red(p1,T) - (HM(p1,T) *' Red(p2,T)) by Th15
.= (p2 - Red(p2,T)) *' Red(p1,T) - ((p1 - Red(p1,T)) *' Red(p2,T)) by Th15
.= (p2 + -Red(p2,T)) *' Red(p1,T) - ((p1 - Red(p1,T)) *' Red(p2,T)) by
POLYNOM1:def 7
.= (p2 + -Red(p2,T)) *' Red(p1,T) - ((p1 + -Red(p1,T)) *' Red(p2,T)) by
POLYNOM1:def 7
.= (p2 *' Red(p1,T) + r2 *' Red(p1,T)) - ((p1 + -Red(p1,T)) *' Red(p2,T)
) by POLYNOM1:26
.= (p2 *' Red(p1,T) + r2 *' Red(p1,T)) - (p1 *' Red(p2,T) + r1 *' Red(p2
,T)) by POLYNOM1:26
.= (p2 *' Red(p1,T) + r2 *' Red(p1,T)) + -(p1 *' Red(p2,T) + r1 *' Red(
p2,T)) by POLYNOM1:def 7
.= (p2 *' Red(p1,T) + r2 *' Red(p1,T)) + (-(p1 *' Red(p2,T)) + -(r1 *'
Red(p2,T))) by POLYRED:1
.= p2 *' Red(p1,T) + (r2 *' Red(p1,T) + (-(r1 *' Red(p2,T)) + -(p1 *'
Red(p2,T)))) by POLYNOM1:21
.= p2 *' Red(p1,T) + (0_(n,L) + -(p1 *' Red(p2,T))) by A1,POLYNOM1:21
.= p2 *' Red(p1,T) + -(p1 *' Red(p2,T)) by POLYRED:2
.= Red(p1,T) *' p2 - Red(p2,T) *' p1 by POLYNOM1:def 7;
end;
theorem Th55:
for n being Ordinal, 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
trivial doubleLoopStr, p1,p2 being non-zero Polynomial of n,L st HT(p1,T),HT(
p2,T) are_disjoint & Red(p1,T) is non-zero & Red(p2,T) is non-zero holds
PolyRedRel({p1},T) reduces HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T), p2 *' Red
(p1,T)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 be non-zero Polynomial of n,L;
assume that
A1: HT(p1,T),HT(p2,T) are_disjoint and
A2: Red(p1,T) is non-zero & Red(p2,T) is non-zero;
reconsider red1 = Red(p1,T), red2 = Red(p2,T) as non-zero Polynomial of n,L
by A2;
set j = card(Support p2);
defpred P[Nat] means for m being Element of NAT st m <= card(
Support p2) & card(Support Low(p2,T,m)) = $1 holds PolyRedRel({p1},T) reduces
HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T), HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red
(p2,T)-Low(p2,T,m)) + Red(p1,T)*'Low(p2,T,m);
now
assume j = 0;
then Support p2 = {};
then p2 = 0_(n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def 1;
end;
then
A3: 1 <= j by NAT_1:14;
then 1 - 1 <= j - 1 by XREAL_1:9;
then reconsider j9 = j - 1 as Element of NAT by INT_1:3;
A4: HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Low(p2,T,1)) + Red(p1,T)*'
Low(p2,T,1) = HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Red(p2,T)) + Red(p1,T)
*'Low(p2,T,1) by Th36
.= HM(p2,T)*'Red(p1,T) - HM(p1,T)*'0_(n,L) + Red(p1,T)*'Low(p2,T,1) by
POLYNOM1:24
.= HM(p2,T)*'Red(p1,T) - 0_(n,L) + Red(p1,T)*'Low(p2,T,1) by POLYRED:5
.= HM(p2,T)*'Red(p1,T) + Red(p1,T)*'Low(p2,T,1) by POLYRED:4
.= HM(p2,T)*'Red(p1,T) + Red(p1,T)*'Red(p2,T) by Th36
.= (HM(p2,T) + Red(p2,T)) *' Red(p1,T) by POLYNOM1:26
.= p2 *' Red(p1,T) by TERMORD:38;
p2 <> 0_(n,L) by POLYNOM7:def 1;
then Support p2 <> {} by POLYNOM7:1;
then HT(p2,T) in Support p2 by TERMORD:def 6;
then for t being object holds t in {HT(p2,T)} implies t in Support p2 by
TARSKI:def 1;
then
A5: {HT(p2,T)} c= Support p2;
A6: card(Support red2) = card(Support(p2) \ {HT(p2,T)}) by TERMORD:36
.= card(Support(p2)) - card({HT(p2,T)}) by A5,CARD_2:44
.= j - 1 by CARD_2:42;
then
A7: card(Support Low(p2,T,1)) = j9 by Th36;
A8: for k being Element of NAT st 0 <= k & k < j9 holds P[k] implies P[k+1]
proof
let k be Element of NAT;
assume that
0 <= k and
A9: k < j9;
now
assume
A10: P[k];
now
HT(HM(p2,T)*'red1,T) = HT(HM(p2,T),T) + HT(red1,T) & HC(HM(p2,T)
*'red1,T) <> 0.L by TERMORD:31;
then
A11: (HM(p2,T)*'red1).(HT(HM(p2,T),T) + HT(red1,T)) <> 0.L by TERMORD:def 7;
A12: Support Red(p2,T) c= Support p2 by TERMORD:35;
red2 <> 0_(n,L) by POLYNOM7:def 1;
then
A13: Support red2 <> {} by POLYNOM7:1;
let m be Element of NAT;
assume that
A14: m <= card(Support p2) and
A15: card(Support Low(p2,T,m)) = k+1;
set m9 = m + 1;
now
assume m = card(Support p2);
then Low(p2,T,m) = 0_(n,L) by Th35;
hence contradiction by A15,CARD_1:27,POLYNOM7:1;
end;
then
A16: m < card(Support p2) by A14,XXREAL_0:1;
then card(Support Low(p2,T,m) \ Support Low(p2,T,m9)) = card(Support
Low(p2,T,m)) - card(Support Low(p2,T,m9)) by Th41,CARD_2:44;
then
A17: k + 1 - card(Support Low(p2,T,m9)) = card {HT(Low(p2,T,m),T)} by A15
,A16,Th42
.= 1 by CARD_1:30;
set f = HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Low(p2,T,m9)) + Red
(p1,T)*'Low(p2,T,m9);
A18: HT(HM(p2,T),T) + HT(red1,T) is Element of Bags n by PRE_POLY:def 12;
A19: m9 <= card(Support p2) by A16,NAT_1:13;
now
A20: Support(red1*'Low(p2,T,m9)) c= {s + t where s,t is Element of
Bags n : s in Support red1 & t in Support Low(p2,T,m9)} by TERMORD:30;
assume HT(HM(p2,T),T) + HT(red1,T) in Support(red1*'Low(p2,T, m9 ) );
then HT(HM(p2,T),T) + HT(red1,T) in {s + t where s,t is Element of
Bags n : s in Support red1 & t in Support Low(p2,T,m9)} by A20;
then consider s,t being Element of Bags n such that
A21: HT(HM(p2,T),T) + HT(red1,T) = s + t and
A22: s in Support red1 and
A23: t in Support Low(p2,T,m9);
A24: t < HT(p2,T),T
proof
now
per cases;
case
m9 = card(Support p2);
then Low(p2,T,m9) = 0_(n,L) by Th35;
hence contradiction by A23,POLYNOM7:1;
end;
case
A25: m9 <> card(Support p2);
A26: t <= HT(Low(p2,T,m9),T),T by A23,TERMORD:def 6;
m9 < card(Support p2) by A19,A25,XXREAL_0:1;
hence thesis by A26,Th3,Th39;
end;
end;
hence thesis;
end;
s <= HT(red1,T),T by A22,TERMORD:def 6;
then s + t < HT(p2,T) + HT(red1,T),T by A24,Th5;
then s + t < HT(HM(p2,T),T) + HT(red1,T),T by TERMORD:26;
hence contradiction by A21,TERMORD:def 3;
end;
then
A27: (red1*'Low(p2,T,m9)).(HT(HM(p2,T),T) + HT(red1,T)) = 0.L by A18,
POLYNOM1:def 4;
A28: 1 <= m9 by NAT_1:14;
now
red1 <> 0_(n,L) by POLYNOM7:def 1;
then Support red1 <> {} by POLYNOM7:1;
then
A29: HT(HM(p2,T),T) = HT(p2,T) & HT(red1,T) in Support red1 by TERMORD:26
,def 6;
A30: Support(HM(p1,T)*'(red2-Low(p2,T,m9))) c= {s + t where s,t is
Element of Bags n : s in Support HM(p1,T) & t in Support(red2-Low(p2,T,m9))}
by TERMORD:30;
assume HT(HM(p2,T),T) + HT(red1,T) in Support(HM(p1,T)*'(red2-Low(
p2,T,m9)));
then
A31: HT(HM(p2,T),T) + HT(red1,T) in {s + t where s,t is Element of
Bags n : s in Support HM(p1,T) & t in Support(red2-Low(p2,T,m9))} by A30;
red2 - Low(p2,T,m9) = red2 + -Low(p2,T,m9) & Support(-Low(p2,T,
m9)) = Support Low(p2,T,m9) by GROEB_1:5,POLYNOM1:def 7;
then
A32: Support(red2 - Low(p2,T,m9)) c= Support red2 \/ Support Low(p2,
T,m9) by POLYNOM1:20;
consider s,t being Element of Bags n such that
A33: HT(HM(p2,T),T) + HT(red1,T) = s + t and
A34: s in Support HM(p1,T) and
A35: t in Support(red2-Low(p2,T,m9)) by A31;
A36: Support Low(p2,T,m9) c= Support red2 by A19,A28,Th27;
A37: t in Support red2
proof
now
per cases by A35,A32,XBOOLE_0:def 3;
case
t in Support red2;
hence thesis;
end;
case
t in Support Low(p2,T,m9);
hence thesis by A36;
end;
end;
hence thesis;
end;
HM(p1,T) <> 0_(n,L) by POLYNOM7:def 1;
then Support HM(p1,T) <> {} by POLYNOM7:1;
then Support HM(p1,T) = {HT(p1,T)} by TERMORD:21;
then s = HT(p1,T) by A34,TARSKI:def 1;
hence contradiction by A1,A33,A29,A37,Th52;
end;
then (HM(p1,T)*'(red2-Low(p2,T,m9))).(HT(HM(p2,T),T) + HT(red1,T)) =
0.L by A18,POLYNOM1:def 4;
then
A38: - (HM(p1,T)*'(red2-Low(p2,T,m9))).(HT(HM(p2,T),T) + HT( red1,T))
= 0.L by RLVECT_1:12;
A39: Support Low(p2,T,m9) = Lower_Support(p2,T,m9) by A19,Lm3;
now
assume
A40: HT(red2,T) in Support Low(p2,T,m9);
A41: now
let t be object;
assume
A42: t in Support red2;
then reconsider t9 = t as bag of n;
Support red2 c= Support p2 & t9 <= HT(red2,T),T by A42,TERMORD:35
,def 6;
hence t in Support Low(p2,T,m9) by A19,A39,A40,A42,Th24;
end;
Support Low(p2,T,m9) c= Support red2 by A19,A28,Th27;
then for t being object holds t in Support Low(p2,T,m9)
implies t in Support red2;
hence contradiction by A6,A9,A17,A41,TARSKI:2;
end;
then Low(p2,T,m9) <> red2 by A13,TERMORD:def 6;
then Red(p2,T) - Low(p2,T,m9) <> 0_(n,L) by Th12;
then reconsider
z1 = Red(p2,T) - Low(p2,T,m9) as non-zero Polynomial of n,L
by POLYNOM7:def 1;
reconsider z = HM(p1,T) *' z1 as non-zero Polynomial of n,L;
z1 = Red(p2,T) + -Low(p2,T,m9) by POLYNOM1:def 7;
then
Support z1 c= Support Red(p2,T) \/ Support -Low(p2,T,m9) by POLYNOM1:20;
then
A43: Support z1 c= Support Red(p2,T) \/ Support Low(p2,T,m9) by GROEB_1:5;
z <> 0_(n,L) by POLYNOM7:def 1;
then Support z <> {} by POLYNOM7:1;
then reconsider w = card(Support z) - 1 as Element of NAT by INT_1:5
,NAT_1:14;
reconsider lowzw = Low(z,T,w) as non-zero Monomial of n,L by Th37;
set b = term(lowzw);
set s = b / HT(p1,T);
A44: Support(HM(p1,T) *' z1) c= {t9 + t where t9,t is Element of Bags
n: t9 in Support HM(p1,T) & t in Support z1} by TERMORD:30;
card(Support z) = w + 1;
then
A45: w < card(Support z) by NAT_1:16;
then
A46: Support(lowzw) c= Support(z) by Th26;
lowzw <> 0_(n,L) by POLYNOM7:def 1;
then Support lowzw <> {} by POLYNOM7:1;
then Support lowzw = {b} by POLYNOM7:7;
then
A47: b in Support lowzw by TARSKI:def 1;
then b in Support HM(p1,T) *' z1 by A46;
then b in {t9 + t where t9,t is Element of Bags n : t9 in Support HM(
p1,T) & t in Support z1} by A44;
then consider t9,t being Element of Bags n such that
A48: b = t9 + t and
A49: t9 in Support HM(p1,T) and
A50: t in Support z1;
HM(p1,T) <> 0_(n,L) by POLYNOM7:def 1;
then Support HM(p1,T) <> {} by POLYNOM7:1;
then Support HM(p1,T) = {term(HM(p1,T))} by POLYNOM7:7
.= {HT(p1,T)} by TERMORD:22;
then
A51: t9 = HT(p1,T) by A49,TARSKI:def 1;
then
A52: HT(p1,T) divides b by A48,PRE_POLY:50;
then
A53: s + HT(p1,T) = b by GROEB_2:def 1;
A54: s = s +HT(p1,T)-'HT(p1,T) by PRE_POLY:48
.= t by A48,A51,A53,PRE_POLY:48;
Support Red(p2,T) \/ Support Low(p2,T,m9) c= Support Red(p2,T)
\/ Support Red(p2,T) by A19,A28,Th27,XBOOLE_1:9;
then
A55: Support z1 c= Support red2 by A43;
then
A56: s in Support Red(p2,T) by A50,A54;
then s in (Support(p2) \ {HT(p2,T)}) by TERMORD:36;
then not s in {HT(p2,T)} by XBOOLE_0:def 5;
then
A57: s <> HT(p2,T) by TARSKI:def 1;
then
A58: Red(p2,T).s = p2.s by A56,A12,TERMORD:40;
A59: now
assume s in Support Low(p2,T,m9);
then
A60: p2.s = Low(p2,T,m9).s by Th16;
(Red(p2,T) - Low(p2,T,m9)).s = (Red(p2,T) + -Low(p2,T,m9)).s
by POLYNOM1:def 7
.= Red(p2,T).s + (-Low(p2,T,m9)).s by POLYNOM1:15
.= Red(p2,T).s + -(Low(p2,T,m9).s) by POLYNOM1:17
.= 0.L by A58,A60,RLVECT_1:5;
hence contradiction by A50,A54,POLYNOM1:def 4;
end;
A61: b is Element of Bags n by PRE_POLY:def 12;
A62: now
assume (Red(p1,T)*'Low(p2,T,m9)).b <> 0.L;
then
A63: b in Support(Red(p1,T)*'Low(p2,T,m9)) by A61,POLYNOM1:def 4;
Support(Red(p1,T)*'Low(p2,T,m9)) c= {u + v where u,v is
Element of Bags n : u in Support Red(p1,T) & v in Support Low(p2,T,m9)} by
TERMORD:30;
then b in {u + v where u,v is Element of Bags n : u in Support Red(
p1,T) & v in Support Low(p2,T,m9)} by A63;
then consider t9,t being Element of Bags n such that
A64: b = t9 + t and
A65: t9 in Support Red(p1,T) and
A66: t in Support Low(p2,T,m9);
A67: s + HT(p1,T) = t9 + t by A52,A64,GROEB_2:def 1;
now
assume s < t,T;
then
A68: s <= t,T by TERMORD:def 3;
t in Lower_Support(p2,T,m9) by A19,A66,Lm3;
then s in Lower_Support(p2,T,m9) by A19,A56,A12,A68,Th24;
hence contradiction by A19,A59,Lm3;
end;
then
A69: t <= s,T by TERMORD:5;
Support(Red(p1,T)) = Support(p1) \ {HT(p1,T)} by TERMORD:36;
then not t9 in {HT(p1,T)} by A65,XBOOLE_0:def 5;
then
A70: t9 <> HT(p1,T) by TARSKI:def 1;
Support Red(p1,T) c= Support p1 by TERMORD:35;
then t9 <= HT(p1,T),T by A65,TERMORD:def 6;
then t9 < HT(p1,T),T by A70,TERMORD:def 3;
then t + t9 < s + HT(p1,T) ,T by A69,Th6;
hence contradiction by A67,TERMORD:def 3;
end;
A71: now
HM(p2,T) <> 0_(n,L) by POLYNOM7:def 1;
then
A72: Support HM(p2,T) <> {} by POLYNOM7:1;
then HT(HM(p2,T),T) in Support HM(p2,T) by TERMORD:def 6;
then
A73: HT(p2,T) in Support HM(p2,T) by TERMORD:26;
A74: Support(HM(p2,T)*'Red(p1,T)) c= {u+v where u,v is Element of
Bags n : u in Support HM(p2,T) & v in Support Red(p1,T)} by TERMORD:30;
assume b in Support(HM(p2,T)*'Red(p1,T));
then b in {u + v where u,v is Element of Bags n : u in Support HM(
p2,T) & v in Support Red(p1,T)} by A74;
then consider t9,t being Element of Bags n such that
A75: b = t9 + t and
A76: t9 in Support HM(p2,T) and
A77: t in Support Red(p1,T);
ex x being bag of n st Support HM(p2,T) = {x} by A72,POLYNOM7:6;
then Support HM(p2,T) = {HT(p2,T)} by A73,TARSKI:def 1;
then t9 = HT(p2,T) by A76,TARSKI:def 1;
hence contradiction by A1,A55,A50,A53,A54,A75,A77,Th52;
end;
set g = f - (f.b/HC(p1,T)) * (s *' p1);
A78: HT(HM(p2,T),T) + HT(red1,T) is Element of Bags n by PRE_POLY:def 12;
A79: f.b = ((HM(p2,T)*'red1+-HM(p1,T)*'(red2-Low(p2,T,m9)))+red1*'Low
(p2,T,m9)). b by POLYNOM1:def 7
.= (HM(p2,T)*'red1 + -HM(p1,T)*'(red2-Low(p2,T,m9))).b + 0.L by A62,
POLYNOM1:15
.= (HM(p2,T)*'red1+-HM(p1,T)*'(red2-Low(p2,T,m9))).b by
RLVECT_1:def 4
.= (HM(p2,T)*'red1).b + (-HM(p1,T)*'(red2-Low(p2,T,m9))).b by
POLYNOM1:15
.= 0.L + (-HM(p1,T)*'(red2-Low(p2,T,m9))).b by A61,A71,POLYNOM1:def 4
.= (-HM(p1,T)*'(red2-Low(p2,T,m9))).b by RLVECT_1:def 4
.= -(HM(p1,T)*'(red2-Low(p2,T,m9)).b) by POLYNOM1:17;
w = card(Support z1) - 1 by Th10;
then reconsider lowz1w = Low(z1,T,w) as non-zero Monomial of n,L by
Th37;
w + 1 = card(Support z1) - 1 + 1 by Th10;
then
A80: w <= card(Support z1) by NAT_1:13;
lowz1w <> 0_(n,L) by POLYNOM7:def 1;
then Support lowz1w <> {} by POLYNOM7:1;
then
A81: Support lowz1w = {term(lowz1w)} by POLYNOM7:7;
card(Support z) = card(Support z1) by Th10;
then s + HT(p1,T) = term(HM(p1,T) *' lowz1w) by A45,A53,Th44
.= term(HM(p1,T)) + term(lowz1w) by Th7
.= HT(p1,T) + term(lowz1w) by TERMORD:22;
then
A82: s = HT(p1,T) + term(lowz1w) -' HT(p1,T) by PRE_POLY:48
.= term(lowz1w) by PRE_POLY:48;
then s in Support lowz1w by A81,TARSKI:def 1;
then
A83: s in Lower_Support(z1,T,w) by A80,Lm3;
Monom(p2.s,s) = HM(Low(p2,T,m),T)
proof
A84: now
let t be bag of n;
assume
A85: t in Support z1;
now
assume
A86: t < s,T;
then t <= s,T by TERMORD:def 3;
then t in Lower_Support(z1,T,w) by A80,A83,A85,Th24;
then t in Support lowz1w by A80,Lm3;
then t = term lowz1w by A81,TARSKI:def 1;
hence contradiction by A82,A86,TERMORD:def 3;
end;
hence s <= t,T by TERMORD:5;
end;
set r = HT(Low(p2,T,m),T);
Support Low(p2,T,m)\Support Low(p2,T,m9) = {HT(Low(p2,T,m),T)}
by A16,Th42;
then
A87: r in Support Low(p2,T,m)\Support Low(p2,T,m9) by TARSKI:def 1;
then
A88: not r in Support Low(p2,T,m9) by XBOOLE_0:def 5;
A89: (Red(p2,T) - Low(p2,T,m9)).r = (Red(p2,T) + -Low(p2,T,m9)).r
by POLYNOM1:def 7
.= Red(p2,T).r + (-Low(p2,T,m9)).r by POLYNOM1:15
.= Red(p2,T).r + -(Low(p2,T,m9).r) by POLYNOM1:17
.= Red(p2,T).r + -0.L by A88,POLYNOM1:def 4
.= Red(p2,T).r + 0.L by RLVECT_1:12
.= Red(p2,T).r by RLVECT_1:def 4;
A90: r in Support Low(p2,T,m) by A87,XBOOLE_0:def 5;
then
A91: r in Lower_Support(p2,T,m) by A14,Lm3;
A92: Support Low(p2,T,m) c= Support p2 by A14,Th26;
now
assume
A93: r = HT(p2,T);
A94: now
let u be object;
assume
A95: u in Support p2;
then reconsider u9 = u as Element of Bags n;
u9 <= r,T by A93,A95,TERMORD:def 6;
then u9 in Lower_Support(p2,T,m) by A14,A91,A95,Th24;
hence u in Support Low(p2,T,m) by A14,Lm3;
end;
for u being object holds u in Support Low(p2,T,m) implies u in
Support p2 by A92;
then k + 1 = j by A15,A94,TARSKI:2;
hence contradiction by A9;
end;
then
A96: not r in {HT(p2,T)} by TARSKI:def 1;
Support(Red(p2,T)) = Support(p2) \ {HT(p2,T)} by TERMORD:36;
then r in Support red2 by A90,A92,A96,XBOOLE_0:def 5;
then z1.r <> 0.L by A89,POLYNOM1:def 4;
then
A97: r in Support z1 by POLYNOM1:def 4;
Support red2 c= Support p2 by TERMORD:35;
then s in Lower_Support(p2,T,m) by A14,A56,A84,A91,A97,Th24;
then
A98: s in Support(Low(p2,T,m)) by A14,Lm3;
then
s in Support(Low(p2,T,m)) \ Support(Low(p2,T,m9)) by A59,XBOOLE_0:def 5;
then s in {HT(Low(p2,T,m),T)} by A16,Th42;
then
A99: s = HT(Low(p2,T,m),T) by TARSKI:def 1;
then
A100: (HM(Low(p2,T,m),T)).(HT(Low(p2,T,m),T)) = Low(p2,T,m).s by TERMORD:18
.= p2.s by A14,A98,Th31;
HC(Low(p2,T,m),T) = Low(p2,T,m).(HT(Low(p2,T,m),T)) by TERMORD:def 7
.= p2.s by A100,TERMORD:18;
hence thesis by A99,TERMORD:def 8;
end;
then
A101: Low(p2,T,m) = Monom(p2.s,s) + Red(Low(p2,T,m),T) by TERMORD:38
.= Monom(p2.s,s) + Low(p2,T,m9) by A16,Th43;
A102: (HM(p1,T) *' z1).b <> 0.L by A47,A46,POLYNOM1:def 4;
now
assume f.b = 0.L;
then (HM(p1,T) *' z1).b = -0.L by A79,RLVECT_1:17;
hence contradiction by A102,RLVECT_1:12;
end;
then
A103: p1 <> 0_(n,L) & b in Support f by A61,POLYNOM1:def 4,POLYNOM7:def 1;
f.(HT(HM(p2,T),T) + HT(red1,T)) = ((HM(p2,T)*'red1+-HM(p1,T)*'(
red2-Low(p2,T,m9)))+red1*'Low(p2,T,m9)). (HT(HM(p2,T),T) + HT(red1,T)) by
POLYNOM1:def 7
.= (HM(p2,T)*'red1 + -HM(p1,T)*'(red2-Low(p2,T,m9))). (HT(HM(p2,T)
,T) + HT(red1,T)) + 0.L by A27,POLYNOM1:15
.= (HM(p2,T)*'red1 + -HM(p1,T)*'(red2-Low(p2,T,m9))). (HT(HM(p2,T)
,T) + HT(red1,T)) by RLVECT_1:def 4
.= (HM(p2,T)*'red1).(HT(HM(p2,T),T) + HT(red1,T)) + (-HM(p1,T)*'(
red2-Low(p2,T,m9))). (HT(HM(p2,T),T) + HT(red1,T)) by POLYNOM1:15
.= (HM(p2,T)*'red1).(HT(HM(p2,T),T) + HT(red1,T)) + 0.L by A38,
POLYNOM1:17
.= (HM(p2,T)*'red1).(HT(HM(p2,T),T) + HT(red1,T)) by RLVECT_1:def 4;
then HT(HM(p2,T),T) + HT(red1,T) in Support f by A11,A78,POLYNOM1:def 4
;
then f <> 0_(n,L) by POLYNOM7:1;
then f reduces_to g,p1,b,T by A53,A103,POLYRED:def 5;
then
A104: f reduces_to g,p1,T by POLYRED:def 6;
p1 in {p1} by TARSKI:def 1;
then f reduces_to g,{p1},T by A104,POLYRED:def 7;
then [f,g] in PolyRedRel({p1},T) by POLYRED:def 13;
then
A105: PolyRedRel({p1},T) reduces f,g by REWRITE1:15;
m9 <= card(Support p2) by A16,NAT_1:13;
then
A106: PolyRedRel({p1},T) reduces HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(
p2,T),f by A10,A17;
A107: HT(p1,T) = HT(HM(p1,T),T) by TERMORD:26
.= term(HM(p1,T)) by TERMORD:23;
s is Element of Bags n by PRE_POLY:def 12;
then
A108: Low(p2,T,m9).s = 0.L by A59,POLYNOM1:def 4;
A109: Low(p2,T,m) = --Low(p2,T,m) by POLYNOM1:19;
A110: Low(p2,T,m9) = --Low(p2,T,m9) by POLYNOM1:19;
(HM(p1,T)*'(red2-Low(p2,T,m9))).b = (HM(p1,T)*'(red2-Low(p2,T,m9
))).(s+HT(p1,T)) by A52,GROEB_2:def 1
.= (HM(p1,T)).HT(p1,T) * (red2-Low(p2,T,m9)).s by A107,POLYRED:7
.= p1.HT(p1,T) * (red2-Low(p2,T,m9)).s by TERMORD:18
.= HC(p1,T) * (red2-Low(p2,T,m9)).s by TERMORD:def 7
.= HC(p1,T) * (red2 + -Low(p2,T,m9)).s by POLYNOM1:def 7
.= HC(p1,T) * (red2.s + (-Low(p2,T,m9)).s) by POLYNOM1:15
.= HC(p1,T) * (p2.s + (-Low(p2,T,m9)).s) by A56,A12,A57,TERMORD:40
.= HC(p1,T) * (p2.s + -(Low(p2,T,m9).s)) by POLYNOM1:17
.= HC(p1,T) * (p2.s + 0.L) by A108,RLVECT_1:12
.= HC(p1,T) * p2.s by RLVECT_1:def 4;
then (f.b/HC(p1,T)) * (s *' p1) = ((HC(p1,T) * (-p2.s))/HC(p1,T)) * (
s *' p1) by A79,VECTSP_1:9
.= ((HC(p1,T) * (-p2.s))*HC(p1,T)") * (s *' p1)
.= ((-p2.s)*(HC(p1,T)*HC(p1,T)")) * (s *' p1) by GROUP_1:def 3
.= ((-p2.s)*1.L) * (s *' p1) by VECTSP_1:def 10
.= (-p2.s) * (s *' p1);
then g = f + -(-p2.s) * (s *' p1) by POLYNOM1:def 7
.= f + (-(-p2.s)) * (s *' p1) by POLYRED:9
.= f + p2.s * (s *' p1) by RLVECT_1:17
.= f + Monom(p2.s,s) *' p1 by POLYRED:22
.= f + Monom(p2.s,s) *' (HM(p1,T) + Red(p1,T)) by TERMORD:38
.= f + (Monom(p2.s,s) *' HM(p1,T) + Monom(p2.s,s) *' Red(p1,T)) by
POLYNOM1:26
.= (HM(p2,T)*'Red(p1,T) + -HM(p1,T)*'(Red(p2,T)-Low(p2,T,m9)) +
Red(p1,T)*'Low(p2,T,m9)) + (Monom(p2.s,s) *' HM(p1,T) + Monom(p2.s,s) *' Red(p1
,T)) by POLYNOM1:def 7
.= (((HM(p2,T)*'Red(p1,T) + -HM(p1,T)*'(Red(p2,T)-Low(p2,T,m9))) +
Red(p1,T)*'Low(p2,T,m9)) + Monom(p2.s,s) *' HM(p1,T)) + Monom(p2.s,s) *' Red(p1
,T) by POLYNOM1:21
.= (((HM(p2,T)*'Red(p1,T) + -HM(p1,T)*'(Red(p2,T)-Low(p2,T,m9))) +
Monom(p2.s,s)*'HM(p1,T)) + Red(p1,T)*'Low(p2,T,m9)) + Monom(p2.s,s) *' Red(p1,T
) by POLYNOM1:21
.= (((HM(p2,T)*'Red(p1,T) + HM(p1,T)*'-(Red(p2,T)-Low(p2,T,m9)))+
Monom(p2.s,s) *' HM(p1,T)) + Red(p1,T)*'Low(p2,T,m9)) + Monom(p2.s,s) *' Red(p1
,T) by POLYRED:6
.= ((HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'-(Red(p2,T)-Low(p2,T,m9)) +
Monom(p2.s,s)*'HM(p1,T))) + Red(p1,T)*'Low(p2,T,m9)) + Monom(p2.s,s) *' Red(p1,
T) by POLYNOM1:21
.= ((HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'(-(Red(p2,T)-Low(p2,T,m9)) +
Monom(p2.s,s)))) + Red(p1,T)*'Low(p2,T,m9)) + Monom(p2.s,s) *' Red(p1,T) by
POLYNOM1:26
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'(-(Red(p2,T)-Low(p2,T,m9)) +
Monom(p2.s,s)))) + (Red(p1,T)*'Low(p2,T,m9) + Monom(p2.s,s) *' Red(p1,T)) by
POLYNOM1:21
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'(-(Red(p2,T)-Low(p2,T,m9)) +
Monom(p2.s,s)))) + Red(p1,T)*'Low(p2,T,m) by A101,POLYNOM1:26
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'(-(Red(p2,T)+ -Low(p2,T,m9))
+ Monom(p2.s,s)))) + Red(p1,T)*'Low(p2,T,m) by POLYNOM1:def 7
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'((-Red(p2,T)+ --Low(p2,T,m9))
+ Monom(p2.s,s)))) + Red(p1,T)*'Low(p2,T,m) by POLYRED:1
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'(-Red(p2,T) + --Low(p2,T,m))
)) + Red(p1,T)*'Low(p2,T,m) by A109,A110,A101,POLYNOM1:21
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'-(Red(p2,T) + -Low(p2,T,m)) )
) + Red(p1,T)*'Low(p2,T,m) by POLYRED:1
.= (HM(p2,T)*'Red(p1,T) + (HM(p1,T)*'-(Red(p2,T) -Low(p2,T,m)) ))
+ Red(p1,T)*'Low(p2,T,m) by POLYNOM1:def 7
.= (HM(p2,T)*'Red(p1,T) + -(HM(p1,T)*'(Red(p2,T) -Low(p2,T,m)) ))
+ Red(p1,T)*'Low(p2,T,m) by POLYRED:6
.= HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Low(p2,T,m)) + Red(
p1,T)*'Low(p2,T,m) by POLYNOM1:def 7;
hence
PolyRedRel({p1},T) reduces HM(p2,T)*'Red(p1,T)-HM(p1,T)*'Red(p2,T
),HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Low(p2,T,m)) + Red(p1,T)*'Low(p2,T
,m) by A105,A106,REWRITE1:16;
end;
hence P[k+1];
end;
hence thesis;
end;
A111: P[0]
proof
let m be Element of NAT;
assume that
m <= card(Support p2) and
A112: card(Support Low(p2,T,m)) = 0;
Support Low(p2,T,m) = {} by A112;
then Low(p2,T,m) = 0_(n,L) by POLYNOM7:1;
then
HM(p2,T)*'Red(p1,T) - HM(p1,T)*'(Red(p2,T)-Low(p2,T,m)) + Red(p1,T)*'
Low(p2,T,m) = HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T) + Red(p1,T)*'0_(n,L)
by POLYRED:4
.= HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T) + 0_(n,L) by POLYRED:5
.= HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T) by POLYRED:2;
hence thesis by REWRITE1:12;
end;
for i being Element of NAT st 0 <= i & i <= j9 holds P[i] from
INT_1:sch 7(A111,A8);
hence thesis by A3,A7,A4;
end;
theorem Th56:
for n being Ordinal, 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
trivial doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T)
are_disjoint holds PolyRedRel({p1,p2},T) reduces S-Poly(p1,p2,T),0_(n,L)
proof
let n be Ordinal, T be connected admissible TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, p1,p2 be Polynomial of n,L;
assume
A1: HT(p1,T),HT(p2,T) are_disjoint;
then
A2: S-Poly(p1,p2,T) = Red(p1,T) *' p2 - Red(p2,T) *' p1 by Th54;
now
per cases;
case
p1 = 0_(n,L);
then Red(p2,T) *' p1 = 0_(n,L) & Red(p1,T) = 0_(n,L) by Th11,POLYNOM1:28;
then S-Poly(p1,p2,T) = 0_(n,L) - 0_(n,L) by A2,POLYNOM1:28
.= 0_(n,L) by POLYRED:4;
hence thesis by REWRITE1:12;
end;
case
p1 <> 0_(n,L);
then reconsider p1a = p1 as non-zero Polynomial of n,L by POLYNOM7:def 1;
now
let u be object;
assume u in {p2};
then u = p2 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2;
end;
then
A3: {p2} c= {p1,p2};
then
A4: PolyRedRel({p2},T) c= PolyRedRel({p1,p2},T) by GROEB_1:4;
now
let u be object;
assume u in {p1};
then u = p1 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2;
end;
then
A5: {p1} c= {p1,p2};
then
A6: PolyRedRel({p1},T) c= PolyRedRel({p1,p2},T) by GROEB_1:4;
now
per cases;
case
p2 = 0_(n,L);
then Red(p1,T) *' p2 = 0_(n,L) & Red(p2,T) = 0_(n,L) by Th11,
POLYNOM1:28;
then S-Poly(p1,p2,T) = 0_(n,L) - 0_(n,L) by A2,POLYNOM1:28
.= 0_(n,L) by POLYRED:4;
hence thesis by REWRITE1:12;
end;
case
p2 <> 0_(n,L);
then reconsider p2a = p2 as non-zero Polynomial of n,L by
POLYNOM7:def 1;
now
per cases;
case
Red(p1,T) = 0_(n,L);
then
A7: S-Poly(p1,p2,T) = 0_(n,L) - Red(p2,T) *' p1 by A2,POLYNOM1:28;
now
per cases;
case
Red(p2,T) = 0_(n,L);
then S-Poly(p1,p2,T) = 0_(n,L) - 0_(n,L) by A7,POLYNOM1:28
.= 0_(n,L) by POLYRED:4;
hence thesis by REWRITE1:12;
end;
case
Red(p2,T) <> 0_(n,L);
then reconsider
rp2 = Red(p2,T) as non-zero Polynomial of n,L by
POLYNOM7:def 1;
PolyRedRel({p1a},T) reduces -(rp2*'p1a),-0_(n,L) by Th49,Th51
;
then PolyRedRel({p1a},T) reduces -(rp2*'p1a),0_(n,L) by Th13;
then PolyRedRel({p1},T) reduces S-Poly(p1,p2,T),0_(n,L) by A7
,Th14;
hence thesis by A5,GROEB_1:4,REWRITE1:22;
end;
end;
hence thesis;
end;
case
Red(p1,T) <> 0_(n,L);
then reconsider
rp1 = Red(p1,T) as non-zero Polynomial of n,L by POLYNOM7:def 1;
now
per cases;
case
Red(p2,T) = 0_(n,L);
then Red(p2,T) *' p1 = 0_(n,L) by POLYNOM1:28;
then
A8: S-Poly(p1,p2,T) = Red(p1,T) *' p2 - 0_ (n,L) by A1,Th54
.= Red(p1,T) *' p2 by POLYRED:4;
PolyRedRel({p2a},T) reduces rp1*'p2a,0_(n,L) by Th51;
hence thesis by A3,A8,GROEB_1:4,REWRITE1:22;
end;
case
Red(p2,T) <> 0_(n,L);
then reconsider
rp2 = Red(p2,T) as non-zero Polynomial of n,L by
POLYNOM7:def 1;
S-Poly(p1,p2,T) = HM(p2a,T)*'rp1 - HM(p1a,T)*'rp2 by A1,Th53;
then
A9: PolyRedRel({p1,p2},T) reduces S-Poly(p1,p2,T),p2 *' Red
(p1,T) by A1,A6,Th55,REWRITE1:22;
PolyRedRel({p1,p2},T) reduces rp1*'p2a,0_(n,L) by A4,Th51,
REWRITE1:22;
hence thesis by A9,REWRITE1:16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
:: theorem 5.66, p. 222 (Buchberger's first criterium)
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 being Polynomial of n,L st
g1 in G & g2 in G & not(HT(g1,T),HT(g2,T) are_disjoint) 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
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 G is_Groebner_basis_wrt T;
then 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) by
GROEB_2:23;
hence thesis by GROEB_2:24;
end;
:: theorem 5.68 (i) ==> (ii), p. 223
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 trivial 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
& not(HT(g1,T),HT(g2,T) are_disjoint) holds PolyRedRel(G,T) reduces S-Poly(g1,
g2,T),0_(n,L)) implies (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in
G & not(HT(g1,T),HT(g2,T) are_disjoint) & 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
trivial 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 & not HT(g1,T
),HT(g2,T) are_disjoint holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L);
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 g1,g2 being Polynomial of n,L;
assume that
A3: g1 in G and
A4: g2 in G;
now
per cases;
case
A5: HT(g1,T),HT(g2,T) are_disjoint;
now
let u be object;
assume
A6: u in {g1,g2};
now
per cases by A6,TARSKI:def 2;
case
u = g1;
hence u in G by A3;
end;
case
u = g2;
hence u in G by A4;
end;
end;
hence u in G;
end;
then
A7: {g1,g2} c= G;
PolyRedRel({g1,g2},T) reduces S-Poly(g1,g2,T),0_(n,L) by A5,Th56;
hence thesis by A7,GROEB_1:4,REWRITE1:22;
end;
case
not HT(g1,T),HT(g2,T) are_disjoint;
hence thesis by A2,A3,A4;
end;
end;
hence thesis;
end;
then G is_Groebner_basis_wrt T by A1,GROEB_2:25;
hence thesis by GROEB_2:23;
end;
:: theorem 5.68 (ii) ==> (iii), p. 223
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) st
not(0_(n,L) in G) holds (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in
G & not(HT(g1,T),HT(g2,T) are_disjoint) & h is_a_normal_form_of S-Poly(g1,g2,T)
,PolyRedRel(G,T) holds h = 0_(n,L)) implies G is_Groebner_basis_wrt 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, G be Subset of Polynom-Ring(n,L);
assume
A1: not 0_(n,L) in G;
assume
A2: for g1,g2,h being Polynomial of n,L st g1 in G & g2 in G & not HT(g1
,T),HT(g2,T) are_disjoint & h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,
T) holds h = 0_(n,L);
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 g1,g2 being Polynomial of n,L;
assume that
A3: g1 in G and
A4: g2 in G;
now
per cases;
case
A5: HT(g1,T),HT(g2,T) are_disjoint;
now
let u be object;
assume
A6: u in {g1,g2};
now
per cases by A6,TARSKI:def 2;
case
u = g1;
hence u in G by A3;
end;
case
u = g2;
hence u in G by A4;
end;
end;
hence u in G;
end;
then
A7: {g1,g2} c= G;
PolyRedRel({g1,g2},T) reduces S-Poly(g1,g2,T),0_(n,L) by A5,Th56;
hence thesis by A7,GROEB_1:4,REWRITE1:22;
end;
case
A8: not HT(g1,T),HT(g2,T) are_disjoint;
S-Poly(g1,g2,T) has_a_normal_form_wrt PolyRedRel(G,T)
proof
now
per cases;
case
not S-Poly(g1,g2,T) in field PolyRedRel(G,T);
hence thesis by REWRITE1:46;
end;
case
S-Poly(g1,g2,T) in field PolyRedRel(G,T);
hence thesis by REWRITE1:def 14;
end;
end;
hence thesis;
end;
then consider h being object such that
A9: h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) by
REWRITE1:def 11;
PolyRedRel(G,T) reduces S-Poly(g1,g2,T),h by A9,REWRITE1:def 6;
then reconsider h as Polynomial of n,L by Lm1;
h = 0_(n,L) by A2,A3,A4,A8,A9;
hence thesis by A9,REWRITE1:def 6;
end;
end;
hence thesis;
end;
hence thesis by A1,GROEB_2:25;
end;
:: theorem 5.68 (iii) ==> (i), p. 223