:: Characterization and Existence of {G}r\"obner Bases
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES,
ZFMISC_1, POLYNOM1, SUBSET_1, STRUCT_0, RELAT_2, BAGORDER, BINOP_1,
POLYRED, POLYNOM7, ARYTM_1, ARYTM_3, PRE_POLY, TERMORD, FUNCT_1, BROUWER,
RELAT_1, XBOOLE_0, XXREAL_0, SUPINF_2, VALUED_0, XCMPLX_0, CAT_3,
ALGSTR_1, IDEAL_1, FINSEQ_1, PARTFUN1, MESFUNC1, CARD_3, TARSKI, CARD_1,
ORDERS_2, REWRITE1, INT_1, FUNCT_4, GROUP_1, ORDERS_1, DICKSON, RLVECT_2,
FUNCOP_1, PBOOLE, FINSET_1, ORDINAL4, GROEB_1, NAT_1;
notations TARSKI, RELAT_1, XBOOLE_0, RELAT_2, XCMPLX_0, XXREAL_0, RELSET_1,
FUNCT_1, PARTFUN1, ORDINAL1, ALGSTR_0, ALGSTR_1, RLVECT_1, FINSET_1,
FUNCT_7, DICKSON, CARD_3, CARD_1, SUBSET_1, XTUPLE_0, MCART_1, FINSEQ_1,
YELLOW_1, ORDERS_1, PRALG_1, STRUCT_0, POLYNOM7, PBOOLE, FUNCOP_1,
ORDERS_2, VFUNCT_1, POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, VECTSP_1,
TERMORD, GROUP_1, NUMBERS, NAT_1, PRE_POLY, POLYRED, RECDEF_1;
constructors REWRITE1, VECTSP_2, PRALG_1, YELLOW_1, IDEAL_1, DICKSON,
BAGORDER, TERMORD, POLYRED, RECDEF_1, DOMAIN_1, RELSET_1, PBOOLE,
FUNCT_7, VFUNCT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1,
CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, YELLOW_1,
GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, DICKSON, TERMORD,
POLYRED, VALUED_0, ALGSTR_0, FINSEQ_1, PRE_POLY, FUNCOP_1, VFUNCT_1,
FUNCT_1, FUNCT_2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_2, RELAT_1;
equalities STRUCT_0, ALGSTR_0;
expansions TARSKI, RELAT_2, STRUCT_0;
theorems TARSKI, RELSET_1, FINSEQ_1, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1,
RLVECT_1, NAT_1, ALGSTR_1, POLYNOM7, REWRITE1, XBOOLE_0, IDEAL_1,
TERMORD, INT_1, FUNCT_1, ORDERS_2, FINSET_1, WELLORD2, XBOOLE_1, CARD_3,
DICKSON, FUNCOP_1, PRALG_1, YELLOW_1, FUNCT_7, FUNCT_2, CARD_2, BAGORDER,
ORDINAL1, VECTSP_2, POLYRED, RELAT_2, PARTFUN1, ORDERS_1, GROUP_1,
XREAL_1, XXREAL_0, VALUED_0, STRUCT_0, PRE_POLY, XTUPLE_0, PBOOLE;
schemes RELSET_1, NAT_1, CLASSES1;
begin :: Preliminaries
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial of n,L;
redefine func {p} -> Subset of Polynom-Ring(n,L); :: redefines { (TARSKI, definition)
coherence
proof
now
let u be object;
assume u in {p};
then u = p by TARSKI:def 1;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th1:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,
p,g being Polynomial of n,L holds f reduces_to g,p,T implies ex m being
Monomial of n,L st g = f - m *' p
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be
Polynomial of n,L;
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;
consider s being bag of n such that
s + HT(p,T) = b and
A2: g = f - (f.b/HC(p,T)) * (s *' p) by A1,POLYRED:def 5;
(f.b/HC(p,T)) * (s *' p) = Monom(f.b/HC(p,T),s) *' p by POLYRED:22;
hence thesis by A2;
end;
theorem
for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p,T
implies ex m being Monomial of n,L st g = f - m *' p & not(HT(m*'p,T) in
Support g) & HT(m*'p,T) <= HT(f,T),T
proof
let n be Ordinal, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, f,p,g 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: f.b <> 0.L by POLYNOM1:def 4;
p <> 0_(n,L) by A1,POLYRED:def 5;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 1;
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;
set m = Monom(f.b/HC(p,T),s);
A5: HC(p,T)" <> 0.L by VECTSP_1:25;
A6: f.b/HC(p,T) <> 0.L by A2,A5,VECTSP_2:def 1;
then
A7: f.b/HC(p,T) is non zero;
coefficient(m) <> 0.L by A6,POLYNOM7:9;
then HC(m,T) <> 0.L by TERMORD:23;
then m <> 0_(n,L) by TERMORD:17;
then reconsider m as non-zero Monomial of n,L by POLYNOM7:def 1;
A8: HT(m*'p,T) = HT(m,T) + HT(p,T) by TERMORD:31
.= term(m) + HT(p,T) by TERMORD:23
.= s + HT(p,T) by A7,POLYNOM7:10;
then HT(m*'p,T) in Support f by A1,A3,POLYRED:def 5;
then
(f.b/HC(p,T)) * (s *' p) = Monom(f.b/HC(p,T),s) *' p & HT(m*'p,T) <= HT
(f,T) ,T by POLYRED:22,TERMORD:def 6;
hence thesis by A1,A3,A4,A8,POLYRED:39;
end;
Lm1: for L being add-associative left_zeroed right_zeroed add-cancelable
right_complementable associative distributive well-unital non empty
doubleLoopStr, P being Subset of L, p being Element of L st p in P holds p in
P-Ideal
proof
let L be add-associative left_zeroed right_zeroed add-cancelable associative
distributive well-unital right_complementable non empty doubleLoopStr, P be
Subset of L, p be Element of L;
set f = <*p*>;
assume
A1: p in P;
then reconsider P9 = P as non empty Subset of L;
now
let i be set;
assume
A2: i in dom f;
dom f = {1} by FINSEQ_1:2,38;
then i = 1 by A2,TARSKI:def 1;
then f/.i = f.1 by A2,PARTFUN1:def 6
.= p
.= 1.L * p
.= 1.L * p * 1.L;
hence ex u,v being Element of L, a being Element of P9 st f/.i = u*a*v by
A1;
end;
then reconsider f as LinearCombination of P9 by IDEAL_1:def 8;
Sum f = p by RLVECT_1:44;
hence thesis by IDEAL_1:60;
end;
Lm2: for n being Ordinal, T being admissible connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr, p,q being Polynomial of n,L, f,g being Element of Polynom-Ring(
n,L) holds (f = p & g = q) implies f - g = p - q
proof
let n be Ordinal, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr, p,q be Polynomial of n,L, f,g be Element of Polynom-Ring(n,L);
assume that
A1: f = p and
A2: g = q;
reconsider x = -q as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
reconsider x as Element of Polynom-Ring(n,L);
x + g = -q + q by A2,POLYNOM1:def 11
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
then
A3: -q = -g by RLVECT_1:6;
thus p - q = p + (-q) by POLYNOM1:def 7
.= f + (-g) by A1,A3,POLYNOM1:def 11
.= f - g;
end;
Lm3: for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f
being Polynomial of n,L holds f is_irreducible_wrt 0_(n,L),T
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f be
Polynomial of n,L;
assume f is_reducible_wrt 0_(n,L),T;
then consider g being Polynomial of n,L such that
A1: f reduces_to g,0_(n,L),T by POLYRED:def 8;
ex b being bag of n st f reduces_to g,0_(n,L),b,T by A1,POLYRED:def 6;
hence thesis by POLYRED:def 5;
end;
theorem Th3:
for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,
g being Polynomial of n,L, P,Q being Subset of Polynom-Ring(n,L) st P c= Q
holds f reduces_to g,P,T implies f reduces_to g,Q,T
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,g be
Polynomial of n,L, P,Q be Subset of Polynom-Ring(n,L);
assume
A1: P c= Q;
assume f reduces_to g,P,T;
then ex p being Polynomial of n,L st p in P & f reduces_to g,p,T by
POLYRED:def 7;
hence thesis by A1,POLYRED:def 7;
end;
theorem Th4:
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,
Q being Subset of Polynom-Ring(n,L) holds P c= Q implies PolyRedRel(P,T) c=
PolyRedRel(Q,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P,Q being
Subset of Polynom-Ring(n,L);
assume
A1: P c= Q;
now
let u be object;
assume
A2: u in PolyRedRel(P,T);
then consider p,q being object such that
A3: p in NonZero Polynom-Ring(n,L) and
A4: q in the carrier of Polynom-Ring(n,L) and
A5: u = [p,q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A4,POLYNOM1:def 11;
0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
then not p in {0_(n,L)} by A3,XBOOLE_0:def 5;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L by A3,POLYNOM1:def 11
,POLYNOM7:def 1;
p reduces_to q,P,T by A2,A5,POLYRED:def 13;
then p reduces_to q,Q,T by A1,Th3;
hence u in PolyRedRel(Q,T) by A5,POLYRED:def 13;
end;
hence thesis;
end;
theorem Th5:
for n being Ordinal, L being right_zeroed add-associative
right_complementable non empty doubleLoopStr, p being Polynomial of n,L holds
Support(-p) = Support(p)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
non empty doubleLoopStr, p be Polynomial of n,L;
A1: now
let u be object;
assume
A2: u in Support(p);
then reconsider u9 = u as Element of Bags n;
A3: p.u9 <> 0.L by A2,POLYNOM1:def 4;
now
assume (-p).u9 = 0.L;
then (-p).u9 = -(-(0.L)) by RLVECT_1:17;
then -(p.u9) = -(-(0.L)) by POLYNOM1:17
.= 0.L by RLVECT_1:17;
then p.u9 = -(0.L) by RLVECT_1:17;
hence contradiction by A3,RLVECT_1:12;
end;
hence u in Support(-p) by POLYNOM1:def 4;
end;
now
let u be object;
assume
A4: u in Support(-p);
then reconsider u9 = u as Element of Bags n;
A5: (-p).u9 <> 0.L by A4,POLYNOM1:def 4;
now
A6: (-p).u9 = -(p.u9) by POLYNOM1:17;
assume p.u9 = 0.L;
hence contradiction by A5,A6,RLVECT_1:12;
end;
hence u in Support(p) by POLYNOM1:def 4;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th6:
for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, p being Polynomial of n,L holds HT(-p,T) =
HT(p,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, p be Polynomial of n,L;
per cases;
suppose
A1: p = 0_(n,L);
reconsider x = -p as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
reconsider x as Element of Polynom-Ring(n,L);
A2: -(0_(n,L)) = -(0_(n,L)) + 0_(n,L) by POLYNOM1:23
.= 0_(n,L) by POLYRED:3;
0.(Polynom-Ring(n,L)) = 0_(n,L) by POLYNOM1:def 11;
then x + 0.(Polynom-Ring(n,L)) = (-p) + 0_(n,L) by POLYNOM1:def 11
.= 0_(n,L) by A1,A2,POLYNOM1:23
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
then -p = -(0.Polynom-Ring(n,L)) by RLVECT_1:6
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:12
.= p by A1,POLYNOM1:def 11;
hence thesis;
end;
suppose
p <> 0_(n,L);
then
A3: Support(p) <> {} by POLYNOM7:1;
then Support(-p) <> {} by Th5;
then HT(-p,T) in Support(-p) by TERMORD:def 6;
then HT(-p,T) in Support(p) by Th5;
then
A4: HT(-p,T) <= HT(p,T),T by TERMORD:def 6;
HT(p,T) in Support(p) by A3,TERMORD:def 6;
then HT(p,T) in Support(-p) by Th5;
then HT(p,T) <= HT(-p,T),T by TERMORD:def 6;
hence thesis by A4,TERMORD:7;
end;
end;
theorem Th7:
for n being Ordinal, T being admissible connected TermOrder of n,
L being right_zeroed add-associative right_complementable well-unital
distributive non trivial doubleLoopStr, p,q being Polynomial of n,L
holds HT(p-q,T) <= max(HT(p,T),HT(q,T),T), T
proof
let n be Ordinal, T be admissible connected TermOrder of n, L be
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, p,q being Polynomial of n,L;
HT(p+(-q),T) <= max(HT(p,T),HT(-q,T),T),T by TERMORD:34;
then HT(p-q,T) <= max(HT(p,T),HT(-q,T),T),T by POLYNOM1:def 7;
hence thesis by Th6;
end;
theorem Th8:
for n being Ordinal, T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, p,q being Polynomial of n,L holds Support(q) c= Support(p)
implies q <= p,T
proof
let n be Ordinal, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p,
q be Polynomial of n,L;
assume
A1: Support q c= Support p;
defpred P[Nat] means for f,g being Polynomial of n,L st Support f
c= Support g & card(Support f) = $1 holds f <= g,T;
A2: now
let k be Nat;
assume
A3: P[k];
now
set R = RelStr(# Bags n, T#);
let f,g be Polynomial of n,L;
assume that
A4: Support f c= Support g and
A5: card(Support f) = k+1;
set rf = Red(f,T), rg = Red(g,T);
A6: Support f <> {} by A5;
then
A7: HT(f,T) in Support f by TERMORD:def 6;
f <> 0_(n,L) by A6,POLYNOM7:1;
then
A8: f is non-zero by POLYNOM7:def 1;
g <> 0_(n,L) by A4,A7,POLYNOM7:1;
then
A9: g is non-zero by POLYNOM7:def 1;
now
per cases;
case
A10: HT(f,T) = HT(g,T);
A11: Support(rf) = Support(f) \ {HT(f,T)} by TERMORD:36;
A12: Support(rg) = Support(g) \ {HT(g,T)} by TERMORD:36;
now
let u be object;
assume u in Support(rf);
then u in Support f & not u in {HT(f,T)} by A11,XBOOLE_0:def 5;
hence u in Support(rg) by A4,A10,A12,XBOOLE_0:def 5;
end;
then
A13: Support(rf) c= Support(rg);
for u being object holds u in {HT(f,T)} implies u in Support f
by A7,
TARSKI:def 1;
then
A14: {HT(f,T)} c= Support f;
A15: Support(f,T) <> {} & Support(g,T) <> {} by A4,A7,POLYRED:def 4;
A16: Support(rf,T) = Support rf by POLYRED:def 4;
HT(f,T) in {HT(f,T)} by TARSKI:def 1;
then
A17: not HT(f,T) in Support Red(f,T) by A11,XBOOLE_0:def 5;
A18: PosetMax(Support(f,T)) = HT(g,T) by A8,A10,POLYRED:24
.= PosetMax(Support(g,T)) by A9,POLYRED:24;
A19: Support(rg,T) = Support rg by POLYRED:def 4;
A20: Support(g,T) = Support g by POLYRED:def 4;
then
A21: Support(g,T)\{PosetMax(Support(g,T))} = Support(rg,T) by A9,A12,A19,
POLYRED:24;
Support(rf) \/ {HT(f,T)} = Support f \/ {HT(f,T)} by A11,XBOOLE_1:39
.= Support f by A14,XBOOLE_1:12;
then card(Support(Red(f,T))) + 1 = k + 1 by A5,A17,CARD_2:41;
then rf <= rg,T by A3,A13;
then [Support rf,Support rg] in FinOrd RelStr(# Bags n, T#) by
POLYRED:def 2;
then
A22: [Support(rf,T),Support(rg,T)] in union rng FinOrd-Approx R by A16,A19
,BAGORDER:def 15;
A23: Support(f,T) = Support f by POLYRED:def 4;
then Support(f,T)\{PosetMax(Support(f,T))} = Support(rf,T) by A8,A11
,A16,POLYRED:24;
then
[Support(f,T),Support(g,T)] in union rng FinOrd-Approx R by A22,A15
,A18,A21,BAGORDER:35;
then
[Support f,Support g] in FinOrd RelStr(# Bags n, T#) by A23,A20,
BAGORDER:def 15;
hence f <= g,T by POLYRED:def 2;
end;
case
A24: HT(f,T) <> HT(g,T);
now
assume HT(g,T) < HT(f,T),T;
then not HT(f,T) <= HT(g,T),T by TERMORD:5;
hence contradiction by A4,A7,TERMORD:def 6;
end;
then HT(f,T) <= HT(g,T),T by TERMORD:5;
then HT(f,T) < HT(g,T),T by A24,TERMORD:def 3;
then f < g,T by POLYRED:32;
hence f <= g,T by POLYRED:def 3;
end;
end;
hence f <= g,T;
end;
hence P[k+1];
end;
A25: ex k being Element of NAT st card(Support q) = k;
A26: P[ 0 ]
proof
let f,g be Polynomial of n,L;
assume that
Support f c= Support g and
A27: card(Support f) = 0;
Support f = {} by A27;
then f = 0_(n,L) by POLYNOM7:1;
hence thesis by POLYRED:30;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A26,A2);
hence thesis by A1,A25;
end;
theorem Th9:
for n being Ordinal, T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p being non-zero Polynomial of n,L holds f
is_reducible_wrt p,T implies HT(p,T) <= HT(f,T),T
proof
let n being Ordinal, T being connected admissible TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr, f,p being non-zero Polynomial of n,L;
assume f is_reducible_wrt p,T;
then consider b being bag of n such that
A1: b in Support f & HT(p,T) divides b by POLYRED:36;
b <= HT(f,T),T & HT(p,T) <= b,T by A1,TERMORD:10,def 6;
hence thesis by TERMORD:8;
end;
begin :: Characterization of Groebner Bases
theorem Th10:
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 trivial doubleLoopStr, p being Polynomial of n,L holds PolyRedRel({p},T)
is locally-confluent
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 trivial
doubleLoopStr, p be Polynomial of n,L;
set R = PolyRedRel({p},T);
A1: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
per cases;
suppose
A2: p = 0_(n,L);
now
let a,b,c be object;
assume that
A3: [a,b] in R and
[a,c] in R;
consider p9,q being object such that
A4: p9 in NonZero Polynom-Ring(n,L) and
A5: q in the carrier of Polynom-Ring(n,L) and
A6: [a,b] = [p9,q] by A3,ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A5,POLYNOM1:def 11;
not p9 in {0_(n,L)} by A1,A4,XBOOLE_0:def 5;
then p9 <> 0_(n,L) by TARSKI:def 1;
then reconsider p9 as non-zero Polynomial of n,L by A4,POLYNOM1:def 11
,POLYNOM7:def 1;
p9 reduces_to q,{p},T by A3,A6,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A7: g in {p} and
A8: p9 reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A2,A7,TARSKI:def 1;
then p9 is_reducible_wrt 0_(n,L),T by A8,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
hence thesis by REWRITE1:def 24;
end;
suppose
p <> 0_(n,L);
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 1;
now
let a,b,c being object;
assume that
A9: [a,b] in R and
A10: [a,c] in R;
consider pa,pb being object such that
A11: pa in NonZero Polynom-Ring(n,L) and
A12: pb in the carrier of Polynom-Ring(n,L) and
A13: [a,b] = [pa,pb] by A9,ZFMISC_1:def 2;
not pa in {0_(n,L)} by A1,A11,XBOOLE_0:def 5;
then pa <> 0_(n,L) by TARSKI:def 1;
then reconsider pa as non-zero Polynomial of n,L by A11,POLYNOM1:def 11
,POLYNOM7:def 1;
reconsider pb as Polynomial of n,L by A12,POLYNOM1:def 11;
A14: pb = b by A13,XTUPLE_0:1;
A15: pa = a by A13,XTUPLE_0:1;
then pa reduces_to pb,{p},T by A9,A14,POLYRED:def 13;
then ex p9 being Polynomial of n,L st p9 in {p} & pa reduces_to pb,p9,T
by POLYRED:def 7;
then
A16: pa reduces_to pb,p,T by TARSKI:def 1;
consider pa9,pc being object such that
pa9 in NonZero Polynom-Ring(n,L) and
A17: pc in the carrier of Polynom-Ring(n,L) and
A18: [a,c] = [pa9,pc] by A10,ZFMISC_1:def 2;
reconsider pc as Polynomial of n,L by A17,POLYNOM1:def 11;
A19: p in {p} by TARSKI:def 1;
A20: pc = c by A18,XTUPLE_0:1;
then pa reduces_to pc,{p},T by A10,A15,POLYRED:def 13;
then ex p9 being Polynomial of n,L st p9 in {p} & pa reduces_to pc,p9,T
by POLYRED:def 7;
then
A21: pa reduces_to pc,p,T by TARSKI:def 1;
now
per cases;
case
A22: pb = 0_(n,L);
then consider mb being Monomial of n,L such that
A23: 0_(n,L) = pa - mb *' p by A16,Th1;
0_(n,L) + mb*'p = (pa + -(mb*'p)) + mb*'p by A23,POLYNOM1:def 7;
then mb*'p = (pa + -(mb*'p)) + mb*'p by POLYRED:2;
then mb*'p = pa + (-(mb*'p) + mb*'p) by POLYNOM1:21;
then mb*'p = pa + 0_(n,L) by POLYRED:3;
then mb*'p = pa by POLYNOM1:23;
then consider mc being Monomial of n,L such that
A24: pc = mb *' p - mc *' p by A21,Th1;
pc = mb *' p + -(mc *' p) by A24,POLYNOM1:def 7;
then pc = mb *' p + (-mc) *' p by POLYRED:6;
then
A25: pc = (mb + -mc) *' p by POLYNOM1:26;
then
A26: pc = (mb - mc) *' p by POLYNOM1:def 7;
now
per cases;
case
mb = mc;
then pc = 0_(n,L) *'p by A26,POLYNOM1:24;
then pc = 0_(n,L) by POLYRED:5;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,A22,
REWRITE1:12;
end;
case
mb <> mc;
R reduces pb,0_(n,L) by A22,REWRITE1:12;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,A19
,A25,POLYRED:45;
end;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
end;
case
A27: pc = 0_(n,L);
then consider mc being Monomial of n,L such that
A28: 0_(n,L) = pa - mc *' p by A21,Th1;
0_(n,L) + mc*'p = (pa + -(mc*'p)) + mc*'p by A28,POLYNOM1:def 7;
then mc*'p = (pa + -(mc*'p)) + mc*'p by POLYRED:2;
then mc*'p = pa + (-(mc*'p) + mc*'p) by POLYNOM1:21;
then mc*'p = pa + 0_(n,L) by POLYRED:3;
then mc*'p = pa by POLYNOM1:23;
then consider mb being Monomial of n,L such that
A29: pb = mc *' p - mb *' p by A16,Th1;
pb = mc *' p + -(mb *' p) by A29,POLYNOM1:def 7;
then pb = mc *' p + (-mb) *' p by POLYRED:6;
then
A30: pb = (mc + -mb) *' p by POLYNOM1:26;
then
A31: pb = (mc - mb) *' p by POLYNOM1:def 7;
now
per cases;
case
mb = mc;
then pb = 0_(n,L) *'p by A31,POLYNOM1:24;
then pb = 0_(n,L) by POLYRED:5;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,A27,
REWRITE1:12;
end;
case
mb <> mc;
R reduces pc,0_(n,L) by A27,REWRITE1:12;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,A19
,A30,POLYRED:45;
end;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
end;
case
not(pb = 0_(n,L) or pc = 0_(n,L));
then reconsider pb,pc as non-zero Polynomial of n,L by POLYNOM7:def 1
;
now
per cases;
case
pb = pc;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,
REWRITE1:12;
end;
case
A32: pb <> pc;
now
assume pb - pc = 0_(n,L);
then (pb + -pc) + pc = 0_(n,L) + pc by POLYNOM1:def 7;
then pb + (-pc + pc) = 0_(n,L) + pc by POLYNOM1:21;
then pb + 0_(n,L) = 0_(n,L) + pc by POLYRED:3;
then pb + 0_(n,L) = pc by POLYRED:2;
hence contradiction by A32,POLYNOM1:23;
end;
then reconsider h = pb-pc as non-zero Polynomial of n,L by
POLYNOM7:def 1;
consider mb being Monomial of n,L such that
A33: pb = pa - mb *' p by A16,Th1;
consider mc being Monomial of n,L such that
A34: pc = pa - mc *' p by A21,Th1;
now
assume -mb + mc = 0_(n,L);
then mc + (-mb + mb) = 0_(n,L) + mb by POLYNOM1:21;
then mc + 0_(n,L) = 0_(n,L) + mb by POLYRED:3;
then mc + 0_(n,L) = mb by POLYRED:2;
hence contradiction by A32,A33,A34,POLYNOM1:23;
end;
then reconsider hh = -mb + mc as non-zero Polynomial of n,L by
POLYNOM7:def 1;
A35: --(mc *' p) = mc *' p by POLYNOM1:19;
h = (pa - mb *' p) + -(pa - mc *' p) by A33,A34,POLYNOM1:def 7
.= (pa - mb *' p) + -(pa + -(mc *' p)) by POLYNOM1:def 7
.= (pa - mb *' p) + (-pa + --(mc *' p)) by POLYRED:1
.= (pa + -(mb *' p)) + (-pa + --(mc *' p)) by POLYNOM1:def 7
.= ((pa + -(mb *' p)) + -pa) + (mc *' p) by A35,POLYNOM1:21
.= ((pa + -pa) + -(mb *' p)) + (mc *' p) by POLYNOM1:21
.= (0_(n,L) + -(mb *' p)) + (mc *' p) by POLYRED:3
.= -(mb *' p) + (mc *' p) by POLYRED:2
.= ((-mb) *' p) + (mc *' p) by POLYRED:6
.= hh *' p by POLYNOM1:26;
then consider f1,g1 being Polynomial of n,L such that
A36: f1 - g1 = 0_(n,L) and
A37: R reduces pb,f1 & R reduces pc,g1 by A19,POLYRED:45,49;
(f1 + -g1) + g1 = 0_(n,L) + g1 by A36,POLYNOM1:def 7;
then f1 + (-g1 + g1) = 0_(n,L) + g1 by POLYNOM1:21;
then f1 + 0_(n,L) = 0_(n,L) + g1 by POLYRED:3;
then f1 + 0_(n,L) = g1 by POLYRED:2;
then f1 = g1 by POLYNOM1:23;
hence
ex d being set st R reduces b,d & R reduces c,d by A14,A20,A37;
end;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
end;
end;
hence b,c are_convergent_wrt R by REWRITE1:def 7;
end;
hence thesis by REWRITE1:def 24;
end;
end;
theorem :: corollary 5.34, p. 205
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L) st
ex p being Polynomial of n,L st p in P & P-Ideal = {p}-Ideal holds PolyRedRel(P
,T) is locally-confluent
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume ex p being Polynomial of n,L st p in P & P-Ideal = {p}-Ideal;
then consider p being Polynomial of n,L such that
A1: p in P and
A2: P-Ideal = {p}-Ideal;
now
set Rp = PolyRedRel({p},T);
reconsider Rp as locally-confluent strongly-normalizing Relation by Th10;
let a,b,c being object;
assume that
A3: [a,b] in R and
A4: [a,c] in R;
a,b are_convertible_wrt R by A3,REWRITE1:29;
then
A5: b,a are_convertible_wrt R by REWRITE1:31;
consider pa,pb being object such that
pa in NonZero Polynom-Ring(n,L) and
A6: pb in the carrier of Polynom-Ring(n,L) and
A7: [a,b] = [pa,pb] by A3,ZFMISC_1:def 2;
reconsider pb as Polynomial of n,L by A6,POLYNOM1:def 11;
A8: pb = b by A7,XTUPLE_0:1;
consider pa9,pc being object such that
pa9 in NonZero Polynom-Ring(n,L) and
A9: pc in the carrier of Polynom-Ring(n,L) and
A10: [a,c] = [pa9,pc] by A4,ZFMISC_1:def 2;
reconsider pc as Polynomial of n,L by A9,POLYNOM1:def 11;
A11: pc = c by A10,XTUPLE_0:1;
reconsider pb9 = pb, pc9 = pc as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider pc9,pb9 as Element of Polynom-Ring(n,L);
a,c are_convertible_wrt R by A4,REWRITE1:29;
then pb9,pc9 are_congruent_mod {p}-Ideal by A2,A8,A11,A5,POLYRED:57
,REWRITE1:30;
then pb,pc are_convertible_wrt PolyRedRel({p},T) by POLYRED:58;
then b,c are_convergent_wrt Rp by A8,A11,REWRITE1:def 23;
then consider d being object such that
A12: Rp reduces b,d & Rp reduces c,d by REWRITE1:def 7;
for u being object holds u in {p} implies u in P by A1,TARSKI:def 1;
then {p} c= P;
then R reduces b,d & R reduces c,d by A12,Th4,REWRITE1:22;
hence b,c are_convergent_wrt R by REWRITE1:def 7;
end;
hence thesis by REWRITE1:def 24;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
empty doubleLoopStr, P be Subset of Polynom-Ring(n,L);
func HT(P,T) -> Subset of Bags n equals
{ HT(p,T) where p is Polynomial of n
,L : p in P & p <> 0_(n,L) };
coherence
proof
set M = {HT(p,T) where p is Polynomial of n,L : p in P & p <> 0_(n,L)};
now
let u be object;
assume u in M;
then ex p being Polynomial of n,L st u = HT(p,T) & p in P & p <> 0_(n,L);
hence u in Bags n;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let n be Ordinal, S be Subset of Bags n;
func multiples(S) -> Subset of Bags n equals
{ b where b is Element of Bags
n: ex b9 being bag of n st b9 in S & b9 divides b };
coherence
proof
set M = {b where b is Element of Bags n : ex b9 being bag of n st b9 in S
& b9 divides b};
now
let u be object;
assume u in M;
then
ex b being Element of Bags n st u = b & ex b9 being bag of n st b9 in
S & b9 divides b;
hence u in Bags n;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem :: theorem 5.35 (i) ==> (ii), p. 206
for n being Element of NAT, T being connected admissible TermOrder of
n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) is locally-confluent implies PolyRedRel(P,T) is confluent
;
theorem :: theorem 5.35 (ii) ==> (iii), p. 206
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) holds PolyRedRel(P,T) is confluent implies
PolyRedRel(P,T) is with_UN_property;
theorem :: theorem 5.35 (iii) ==> (iv), p. 206
for n being Element of NAT, T being connected admissible TermOrder of
n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) is with_UN_property implies PolyRedRel(P,T) is
with_Church-Rosser_property;
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, f
being Polynomial of n,L, g being object,
P being Subset of Polynom-Ring(n,L) holds
PolyRedRel(P,T) reduces f,g implies g is Polynomial of n,L
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f be
Polynomial of n,L, g be object, P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume R reduces f,g;
then consider p being RedSequence of R such that
A1: p.1 = f and
A2: p.len p = g by REWRITE1:def 3;
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 l + 1 in Seg(len p) by FINSEQ_1:1;
then
A4: l + 1 in dom p by FINSEQ_1:def 3;
per cases;
suppose
len p = 1;
hence thesis by A1,A2;
end;
suppose
len p <> 1;
then 0 + 1 < l + 1 by A3,XXREAL_0:1;
then
A5: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg(len p) by A5,FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A2,A4,REWRITE1:def 2;
then consider h9,g9 being object such that
A6: [h,g] = [h9,g9] and
h9 in NonZero Polynom-Ring(n,L) and
A7: g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
g = g9 by A6,XTUPLE_0:1;
hence thesis by A7,POLYNOM1:def 11;
end;
end;
Lm5: for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,
g being Polynomial of n,L, P being Subset of Polynom-Ring(n,L) holds PolyRedRel
(P,T) reduces f,g & g <> f implies ex h being Polynomial of n,L st f reduces_to
h,P,T & PolyRedRel(P,T) reduces h,g
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, f,g be
Polynomial of n,L, P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume that
A1: PolyRedRel(P,T) reduces f,g and
A2: g <> f;
consider p being RedSequence of R such that
A3: p.1 = f and
A4: p.len p = g by A1,REWRITE1:def 3;
set h = p.2;
len p > 0;
then len p + 1 > 0 + 1 by XREAL_1:8;
then
A5: 1 <= len p by NAT_1:13;
then 1 < len p by A2,A3,A4,XXREAL_0:1;
then
A6: 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg(len p) by FINSEQ_1:1;
then
A7: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg(len p) by A5,FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then
A8: [f,h] in R by A3,A7,REWRITE1:def 2;
then consider f9,h9 being object such that
A9: [f,h] = [f9,h9] and
f9 in NonZero Polynom-Ring(n,L) and
A10: h9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
A11: h = h9 by A9,XTUPLE_0:1;
len p in Seg(len p) by A5,FINSEQ_1:1;
then
A12: len p in dom p by FINSEQ_1:def 3;
reconsider h as Polynomial of n,L by A10,A11,POLYNOM1:def 11;
f reduces_to h,P,T by A8,POLYRED:def 13;
hence thesis by A4,A6,A7,A12,REWRITE1:17;
end;
theorem Th15: :: theorem 5.35 (iv) ==> (v), p. 206
for n being Element of NAT, T being connected admissible
TermOrder of n, L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian almost_left_invertible
non degenerated non empty doubleLoopStr, P being non empty Subset of
Polynom-Ring(n,L) holds PolyRedRel(P,T) is with_Church-Rosser_property implies
(for f being Polynomial of n,L st f in P-Ideal holds PolyRedRel(P,T) reduces f,
0_(n,L))
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P be non empty Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume
A1: PolyRedRel(P,T) is with_Church-Rosser_property;
now
reconsider e = 0_(n,L) as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
let f be Polynomial of n,L;
assume
A2: f in P-Ideal;
reconsider e as Element of Polynom-Ring(n,L);
reconsider f9 = f as Element of Polynom-Ring(n,L) by POLYNOM1:def 11;
reconsider f9 as Element of Polynom-Ring(n,L);
f - 0_(n,L) = f9 - e by Lm2;
then f9 - e in P-Ideal by A2,POLYRED:4;
then f9,e are_congruent_mod P-Ideal by POLYRED:def 14;
then f9,e are_convertible_wrt R by POLYRED:58;
then f9,e are_convergent_wrt R by A1,REWRITE1:def 23;
then consider c being object such that
A3: R reduces f,c and
A4: R reduces 0_(n,L),c by REWRITE1:def 7;
reconsider c9 = c as Polynomial of n,L by A3,Lm4;
now
assume c9 <> 0_(n,L);
then consider h being Polynomial of n,L such that
A5: 0_(n,L) reduces_to h,P,T and
PolyRedRel(P,T) reduces h,c9 by A4,Lm5;
consider pp being Polynomial of n,L such that
pp in P and
A6: 0_(n,L) reduces_to h,pp,T by A5,POLYRED:def 7;
0_(n,L) is_reducible_wrt pp,T by A6,POLYRED:def 8;
hence contradiction by POLYRED:37;
end;
hence R reduces f,0_(n,L) by A3;
end;
hence thesis;
end;
theorem Th16: :: theorem 5.35 (v) ==> (vi), p. 206
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) holds (for f being Polynomial of n,L st f in
P-Ideal holds PolyRedRel(P,T) reduces f,0_(n,L)) implies (for f being non-zero
Polynomial of n,L st f in P-Ideal holds f is_reducible_wrt P,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of
Polynom-Ring(n,L);
assume
A1: for f being Polynomial of n,L st f in P-Ideal holds PolyRedRel(P,T)
reduces f,0_(n,L);
now
let f be non-zero Polynomial of n,L;
assume f in P-Ideal;
then
A2: PolyRedRel(P,T) reduces f,0_(n,L) by A1;
f <> 0_(n,L) by POLYNOM7:def 1;
then ex g being Polynomial of n,L st f reduces_to g,P,T & PolyRedRel(P,T)
reduces g,0_(n,L) by A2,Lm5;
hence f is_reducible_wrt P,T by POLYRED:def 9;
end;
hence thesis;
end;
theorem Th17: :: theorem 5.35 (vi) ==> (vii), p. 206
for n being Element of NAT, T being admissible connected
TermOrder of n, L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian almost_left_invertible
non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L)
holds (for f being non-zero Polynomial of n,L st f in P-Ideal holds f
is_reducible_wrt P,T) implies (for f being non-zero Polynomial of n,L st f in P
-Ideal holds f is_top_reducible_wrt P,T)
proof
let n be Element of NAT, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, P be Subset of Polynom-Ring(n,L);
assume
A1: for f being non-zero Polynomial of n,L st f in P-Ideal holds f
is_reducible_wrt P,T;
thus for f being non-zero Polynomial of n,L st f in P-Ideal holds f
is_top_reducible_wrt P,T
proof
set H = {g where g is non-zero Polynomial of n,L : g in P-Ideal & not(g
is_top_reducible_wrt P,T)};
let f be non-zero Polynomial of n,L;
assume
A2: f in P-Ideal;
assume not f is_top_reducible_wrt P,T;
then
A3: f in H by A2;
now
let u be object;
assume u in H;
then ex g9 being non-zero Polynomial of n,L st u = g9 & g9 in P-Ideal &
not g9 is_top_reducible_wrt P,T;
hence u in the carrier of Polynom-Ring(n,L);
end;
then reconsider H as non empty Subset of Polynom-Ring(n,L) by A3,
TARSKI:def 3;
consider p being Polynomial of n,L such that
A4: p in H and
A5: for q being Polynomial of n,L st q in H holds p <= q,T by POLYRED:31;
A6: ex p9 being non-zero Polynomial of n,L st p9 = p & p9 in P-Ideal & not
p9 is_top_reducible_wrt P,T by A4;
then reconsider p as non-zero Polynomial of n,L;
p is_reducible_wrt P,T by A1,A6;
then consider q being Polynomial of n,L such that
A7: p reduces_to q,P,T by POLYRED:def 9;
consider u being Polynomial of n,L such that
A8: u in P and
A9: p reduces_to q,u,T by A7,POLYRED:def 7;
ex b being bag of n st p reduces_to q,u,b,T by A9,POLYRED:def 6;
then
A10: u <> 0_(n,L) by POLYRED:def 5;
then reconsider u as non-zero Polynomial of n,L by POLYNOM7:def 1;
consider b being bag of n such that
A11: p reduces_to q,u,b,T by A9,POLYRED:def 6;
A12: now
assume b = HT(p,T);
then p top_reduces_to q,u,T by A11,POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A6,A8,POLYRED:def 12;
end;
consider m being Monomial of n,L such that
A13: q = p - m *' u by A9,Th1;
reconsider uu = u, pp = p, mm = m as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider uu,pp,mm as Element of Polynom-Ring(n,L);
uu in P-Ideal by A8,Lm1;
then mm * uu in P-Ideal by IDEAL_1:def 2;
then -(mm * uu) in P-Ideal by IDEAL_1:13;
then
A14: pp + -(mm * uu) in P-Ideal by A6,IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 11;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then
A15: q in P-Ideal by A13,A14;
A16: q < p,T by A9,POLYRED:43;
A17: p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then
A18: HT(p,T) in Support p by TERMORD:def 6;
b in Support p by A11,POLYRED:def 5;
then b <= HT(p,T),T by TERMORD:def 6;
then b < HT(p,T),T by A12,TERMORD:def 3;
then
A19: HT(p,T) in Support q by A18,A11,POLYRED:40;
now
per cases;
case
A20: q <> 0_(n,L);
then reconsider q as non-zero Polynomial of n,L by POLYNOM7:def 1;
Support q <> {} by A20,POLYNOM7:1;
then HT(q,T) in Support q by TERMORD:def 6;
then
A21: HT(q,T) <= HT(p,T),T by A9,POLYRED:42;
HT(p,T) <= HT(q,T),T by A19,TERMORD:def 6;
then
A22: HT(q,T) = HT(p,T) by A21,TERMORD:7;
now
assume not q is_top_reducible_wrt P,T;
then q in H by A15;
then p <= q,T by A5;
hence contradiction by A16,POLYRED:29;
end;
then consider u9 being Polynomial of n,L such that
A23: u9 in P and
A24: q is_top_reducible_wrt u9,T by POLYRED:def 12;
consider q9 being Polynomial of n,L such that
A25: q top_reduces_to q9,u9,T by A24,POLYRED:def 11;
A26: p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then
A27: HT(p,T) in Support p by TERMORD:def 6;
A28: q reduces_to q9,u9,HT(q,T),T by A25,POLYRED:def 10;
then consider s being bag of n such that
A29: s + HT(u9,T) = HT(q,T) and
q9 = q - (q.(HT(q,T))/HC(u9,T)) * (s *' u9) by POLYRED:def 5;
set qq = p - (p.(HT(p,T))/HC(u9,T)) * (s *' u9);
u9 <> 0_(n,L) by A28,POLYRED:def 5;
then p reduces_to qq,u9,HT(p,T),T by A22,A29,A26,A27,POLYRED:def 5;
then p top_reduces_to qq,u9,T by POLYRED:def 10;
then p is_top_reducible_wrt u9,T by POLYRED:def 11;
hence contradiction by A6,A23,POLYRED:def 12;
end;
case
q = 0_(n,L);
then
A30: m *' u = (p - m *' u) + m *' u by A13,POLYRED:2
.= (p + -(m *' u)) + m *' u by POLYNOM1:def 7
.= p + (-(m *' u) + m *' u) by POLYNOM1:21
.= p + 0_(n,L) by POLYRED:3
.= p by POLYNOM1:23;
m <> 0_(n,L) by POLYNOM7:def 1,A30,POLYRED:5;
then reconsider m as non-zero Polynomial of n,L by POLYNOM7:def 1;
set pp = p - (p.(HT(p,T))/HC(u,T)) * (HT(m,T) *' u);
HT(p,T) = HT(m,T) + HT(u,T) by A30,TERMORD:31;
then p reduces_to pp,u,HT(p,T),T by A10,A17,A18,POLYRED:def 5;
then p top_reduces_to pp,u,T by POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A6,A8,POLYRED:def 12;
end;
end;
hence thesis;
end;
end;
theorem Th18: :: theorem 5.35 (vii) ==> (viii), p. 206
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) holds (for f being non-zero Polynomial of n,L
st f in P-Ideal holds f is_top_reducible_wrt P,T) implies (for b being bag of n
st b in HT(P-Ideal,T) ex b9 being bag of n st b9 in HT(P,T) & b9 divides b)
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);
assume
A1: for f being non-zero Polynomial of n,L st f in P-Ideal holds f
is_top_reducible_wrt P,T;
now
let b be bag of n;
assume b in HT(P-Ideal,T);
then consider p being Polynomial of n,L such that
A2: b = HT(p,T) and
A3: p in P-Ideal and
A4: p <> 0_(n,L);
reconsider p as non-zero Polynomial of n,L by A4,POLYNOM7:def 1;
p is_top_reducible_wrt P,T by A1,A3;
then consider u being Polynomial of n,L such that
A5: u in P and
A6: p is_top_reducible_wrt u,T by POLYRED:def 12;
consider q being Polynomial of n,L such that
A7: p top_reduces_to q,u,T by A6,POLYRED:def 11;
A8: p reduces_to q,u,HT(p,T),T by A7,POLYRED:def 10;
then u <> 0_(n,L) by POLYRED:def 5;
then
A9: HT(u,T) in {HT(r,T) where r is Polynomial of n,L : r in P & r <> 0_(n
,L)} by A5;
ex s being bag of n st s + HT(u,T) = HT(p,T) & q = p - ( p.(HT(p,T))/
HC(u,T)) * (s *' u) by A8,POLYRED:def 5;
hence ex b9 being bag of n st b9 in HT(P,T) & b9 divides b by A2,A9,
PRE_POLY:50;
end;
hence thesis;
end;
theorem :: theorem 5.35 (viii) ==> (ix), p. 206
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) holds (for b being bag of n st b in HT(P
-Ideal,T) ex b9 being bag of n st b9 in HT(P,T) & b9 divides b) implies HT(P
-Ideal,T) c= multiples(HT(P,T))
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of
Polynom-Ring(n,L);
assume
A1: for b being bag of n st b in HT(P-Ideal,T) ex b9 being bag of n st
b9 in HT(P,T) & b9 divides b;
let u be object;
assume
A2: u in HT(P-Ideal,T);
then reconsider u9 = u as Element of Bags n;
ex b9 being bag of n st b9 in HT(P,T) & b9 divides u9 by A1,A2;
hence u in multiples(HT(P,T));
end;
theorem :: theorem 5.35 (ix) ==> (i), p. 206
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L)
holds HT(P-Ideal,T) c= multiples(HT(P,T)) implies PolyRedRel(P,T) is
locally-confluent
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume
A1: HT(P-Ideal,T) c= multiples(HT(P,T));
A2: for f being Polynomial of n,L st f in P-Ideal & f <> 0_(n,L) holds f
is_reducible_wrt P,T
proof
let f be Polynomial of n,L;
assume that
A3: f in P-Ideal and
A4: f <> 0_(n,L);
HT(f,T) in {HT(p,T) where p is Polynomial of n,L : p in P-Ideal & p <>
0_(n,L)} by A3,A4;
then HT(f,T) in multiples(HT(P,T)) by A1;
then ex b being Element of Bags n st b = HT(f,T) & ex b9 being bag of n st
b9 in HT(P,T) & b9 divides b;
then consider b9 being bag of n such that
A5: b9 in HT(P,T) and
A6: b9 divides HT(f,T);
consider p being Polynomial of n,L such that
A7: b9 = HT(p,T) and
A8: p in P and
A9: p <> 0_(n,L) by A5;
consider s being bag of n such that
A10: b9 + s = HT(f,T) by A6,TERMORD:1;
set g = f - (f.(HT(f,T))/HC(p,T)) * (s *' p);
Support f <> {} by A4,POLYNOM7:1;
then HT(f,T) in Support f by TERMORD:def 6;
then f reduces_to g,p,HT(f,T),T by A4,A7,A9,A10,POLYRED:def 5;
then f reduces_to g,p,T by POLYRED:def 6;
then f reduces_to g,P,T by A8,POLYRED:def 7;
hence thesis by POLYRED:def 9;
end;
A11: for f being Polynomial of n,L st f in P-Ideal holds R reduces f,0_(n,L)
proof
let f be Polynomial of n,L;
assume
A12: f in P-Ideal;
per cases;
suppose
f = 0_(n,L);
hence thesis by REWRITE1:12;
end;
suppose
f <> 0_(n,L);
then f is_reducible_wrt P,T by A2,A12;
then consider v being Polynomial of n,L such that
A13: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in R by A13,POLYRED:def 13;
then f in field R by RELAT_1:15;
then f has_a_normal_form_wrt R by REWRITE1:def 14;
then consider g being object such that
A14: g is_a_normal_form_of f,R by REWRITE1:def 11;
A15: R reduces f,g by A14,REWRITE1:def 6;
then reconsider g9 = g as Polynomial of n,L by Lm4;
reconsider ff = f, gg = g9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider ff,gg as Element of Polynom-Ring(n,L);
f - g9 = ff - gg by Lm2;
then ff - gg in P-Ideal by A15,POLYRED:59;
then
A16: (ff - gg) - ff in P-Ideal by A12,IDEAL_1:16;
(ff - gg) - ff = (ff + -gg) - ff
.= (ff + -gg) + -ff
.= (ff + -ff) + -gg by RLVECT_1:def 3
.= 0.(Polynom-Ring(n,L)) + -gg by RLVECT_1:5
.= - gg by ALGSTR_1:def 2;
then --gg in P-Ideal by A16,IDEAL_1:14;
then
A17: g in P-Ideal by RLVECT_1:17;
assume not R reduces f,0_(n,L);
then g <> 0_(n,L) by A14,REWRITE1:def 6;
then g9 is_reducible_wrt P,T by A2,A17;
then consider u being Polynomial of n,L such that
A18: g9 reduces_to u,P,T by POLYRED:def 9;
A19: [g9,u] in R by A18,POLYRED:def 13;
g is_a_normal_form_wrt R by A14,REWRITE1:def 6;
hence contradiction by A19,REWRITE1:def 5;
end;
end;
now
let a,b,c being object;
assume that
A20: [a,b] in R and
A21: [a,c] in R;
consider a9,b9 being object such that
a9 in (NonZero Polynom-Ring(n,L)) and
A22: b9 in the carrier of Polynom-Ring(n,L) and
A23: [a,b] = [a9,b9] by A20,ZFMISC_1:def 2;
A24: b9 = b by A23,XTUPLE_0:1;
a,b are_convertible_wrt R by A20,REWRITE1:29;
then
A25: b,a are_convertible_wrt R by REWRITE1:31;
consider aa,c9 being object such that
aa in (NonZero Polynom-Ring(n,L)) and
A26: c9 in the carrier of Polynom-Ring(n,L) and
A27: [a,c] = [aa,c9] by A21,ZFMISC_1:def 2;
A28: c9 = c by A27,XTUPLE_0:1;
reconsider b9, c9 as Polynomial of n,L by A22,A26,POLYNOM1:def 11;
reconsider bb = b9, cc = c9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider bb,cc as Element of Polynom-Ring(n,L);
a,c are_convertible_wrt R by A21,REWRITE1:29;
then bb,cc are_congruent_mod P-Ideal by A24,A28,A25,POLYRED:57,REWRITE1:30;
then
A29: bb - cc in P-Ideal by POLYRED:def 14;
b9 - c9 = bb - cc by Lm2;
hence b,c are_convergent_wrt R by A11,A24,A28,A29,POLYRED:50;
end;
hence thesis by REWRITE1:def 24;
end;
definition :: definition 5.37, p. 207
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, G be Subset of
Polynom-Ring(n,L);
pred G is_Groebner_basis_wrt T means
PolyRedRel(G,T) is locally-confluent;
end;
definition :: definition 5.37, p. 207
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, G,I be Subset
of Polynom-Ring(n,L);
pred G is_Groebner_basis_of I,T means
G-Ideal = I & PolyRedRel(G,T) is locally-confluent;
end;
Lm6: 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),
a,b being object st a <> b holds PolyRedRel(P,T
) reduces a,b implies a is Polynomial of n,L & b 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), f,g be object;
set R = PolyRedRel(P,T);
assume
A1: f <> g;
assume R reduces f,g;
then consider p being RedSequence of R such that
A2: p.1 = f and
A3: p.len p = g by REWRITE1:def 3;
reconsider l = len p - 1 as Element of NAT by INT_1:5,NAT_1:14;
set q = p.(1+1), h = p.l;
A4: 1 <= len(p) by NAT_1:14;
now
per cases;
case
len p = 1;
hence f is Polynomial of n,L by A1,A2,A3;
end;
case
len p <> 1;
then 1 < len p by A4,XXREAL_0:1;
then 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg(len p) by FINSEQ_1:1;
then
A5: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg(len p) by A4,FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then [f,q] in R by A2,A5,REWRITE1:def 2;
then consider h9,g9 being object such that
A6: [f,q] = [h9,g9] and
A7: h9 in NonZero Polynom-Ring(n,L) and
g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
f = h9 by A6,XTUPLE_0:1;
hence f is Polynomial of n,L by A7,POLYNOM1:def 11;
end;
end;
hence f is Polynomial of n,L;
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg(len p) by FINSEQ_1:1;
then
A8: l + 1 in dom p by FINSEQ_1:def 3;
now
per cases;
case
len p = 1;
hence thesis by A1,A2,A3;
end;
case
len p <> 1;
then 0 + 1 < l + 1 by A4,XXREAL_0:1;
then
A9: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg(len p) by A9,FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A3,A8,REWRITE1:def 2;
then consider h9,g9 being object such that
A10: [h,g] = [h9,g9] and
h9 in NonZero Polynom-Ring(n,L) and
A11: g9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
g = g9 by A10,XTUPLE_0:1;
hence thesis by A11,POLYNOM1:def 11;
end;
end;
hence thesis;
end;
theorem
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, G,P being non empty Subset of
Polynom-Ring(n,L) st G is_Groebner_basis_of P,T holds PolyRedRel(G,T) is
Completion of PolyRedRel(P,T)
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, G,P be non empty Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume
A1: G is_Groebner_basis_of P,T;
then PolyRedRel(G,T) is locally-confluent;
then reconsider RG = PolyRedRel(G,T) as complete Relation;
for a,b being object holds a,b are_convertible_wrt R iff a,b
are_convergent_wrt RG
proof
let a,b be object;
A2: G-Ideal = P by A1;
A3: now
assume
A4: a,b are_convertible_wrt R;
now
per cases;
case
a = b;
hence a,b are_convergent_wrt RG by REWRITE1:38;
end;
case
A5: a <> b;
R \/ R~ reduces a,b by A4,REWRITE1:def 4;
then consider p being RedSequence of R \/ R~ such that
A6: p.1 = a and
A7: p.len p = b by REWRITE1:def 3;
reconsider l = len p - 1 as Element of NAT by INT_1:5,NAT_1:14;
A8: 1 <= len(p) by NAT_1:14;
set h = p.l, g = p.(1+1);
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg(len p) by FINSEQ_1:1;
then
A9: l + 1 in dom p by FINSEQ_1:def 3;
now
per cases;
case
len p = 1;
hence
a is Polynomial of n,L & b is Polynomial of n,L by A5,A6,A7;
end;
case
A10: len p <> 1;
then 0 + 1 < l + 1 by A8,XXREAL_0:1;
then
A11: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg(len p) by A11,FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then
A12: [h,b] in R \/ R~ by A7,A9,REWRITE1:def 2;
A13: now
per cases by A12,XBOOLE_0:def 3;
case
[h,b] in R;
then consider h9,b9 being object such that
A14: [h,b] = [h9,b9] and
h9 in NonZero Polynom-Ring(n,L) and
A15: b9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
b = b9 by A14,XTUPLE_0:1;
hence b is Polynomial of n,L by A15,POLYNOM1:def 11;
end;
case
[h,b] in R~;
then [b,h] in R by RELAT_1:def 7;
then consider h9,b9 being object such that
A16: [b,h] = [h9,b9] and
A17: h9 in NonZero Polynom-Ring(n,L) and
b9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
b = h9 by A16,XTUPLE_0:1;
hence b is Polynomial of n,L by A17,POLYNOM1:def 11;
end;
end;
1 < len p by A8,A10,XXREAL_0:1;
then 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg(len p) by FINSEQ_1:1;
then
A18: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg(len p) by A8,FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then
A19: [a,g] in R \/ R~ by A6,A18,REWRITE1:def 2;
now
per cases by A19,XBOOLE_0:def 3;
case
[a,g] in R;
then consider h9,b9 being object such that
A20: [a,g] = [h9,b9] and
A21: h9 in NonZero Polynom-Ring(n,L) and
b9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
a = h9 by A20,XTUPLE_0:1;
hence a is Polynomial of n,L by A21,POLYNOM1:def 11;
end;
case
[a,g] in R~;
then [g,a] in R by RELAT_1:def 7;
then consider h9,b9 being object such that
A22: [g,a] = [h9,b9] and
h9 in NonZero Polynom-Ring(n,L) and
A23: b9 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:2;
a = b9 by A22,XTUPLE_0:1;
hence a is Polynomial of n,L by A23,POLYNOM1:def 11;
end;
end;
hence a is Polynomial of n, L & b is Polynomial of n,L by A13;
end;
end;
then reconsider a9 = a, b9 = b as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider a9,b9 as Element of Polynom-Ring(n,L);
G-Ideal = P-Ideal by A2,IDEAL_1:44;
then a9,b9 are_congruent_mod G-Ideal by A4,POLYRED:57;
then a9,b9 are_convertible_wrt RG by POLYRED:58;
hence a,b are_convergent_wrt RG by REWRITE1:def 23;
end;
end;
hence a,b are_convergent_wrt RG;
end;
now
assume
A24: a,b are_convergent_wrt RG;
now
per cases;
case
a = b;
hence a,b are_convertible_wrt R by REWRITE1:26;
end;
case
A25: a <> b;
consider c being object such that
A26: RG reduces a,c and
A27: RG reduces b,c by A24,REWRITE1:def 7;
a is Polynomial of n,L & b is Polynomial of n,L
proof
now
per cases;
case
a = c;
hence thesis by A25,A27,Lm6;
end;
case
A28: a <> c;
now
per cases;
case
b = c;
hence thesis by A25,A26,Lm6;
end;
case
b <> c;
hence b is Polynomial of n,L by A27,Lm6;
end;
end;
hence thesis by A26,A28,Lm6;
end;
end;
hence thesis;
end;
then reconsider
a9 = a, b9 = b as Element of the carrier of Polynom-Ring(
n,L) by POLYNOM1:def 11;
reconsider a9,b9 as Element of Polynom-Ring(n,L);
G-Ideal = P-Ideal & a9,b9 are_convertible_wrt RG by A2,A24,IDEAL_1:44
,REWRITE1:37;
then a9,b9 are_congruent_mod P-Ideal by POLYRED:57;
hence a,b are_convertible_wrt R by POLYRED:58;
end;
end;
hence a,b are_convertible_wrt R;
end;
hence thesis by A3;
end;
hence thesis by REWRITE1:def 28;
end;
theorem
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, p,q being Element of Polynom-Ring(n,L),
G being non empty Subset of Polynom-Ring(n,L) st G is_Groebner_basis_wrt T
holds p,q are_congruent_mod G-Ideal iff nf(p,PolyRedRel(G,T)) = nf(q,PolyRedRel
(G,T))
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, p,q be Element of Polynom-Ring(n,L), G be non empty
Subset of Polynom-Ring(n,L);
set R = PolyRedRel(G,T);
assume G is_Groebner_basis_wrt T;
then
A1: PolyRedRel(G,T) is locally-confluent;
now
nf(q,R) is_a_normal_form_of q,R by A1,REWRITE1:54;
then R reduces q,nf(q,R) by REWRITE1:def 6;
then
A2: nf(q,R),q are_convertible_wrt R by REWRITE1:25;
nf(p,R) is_a_normal_form_of p,R by A1,REWRITE1:54;
then R reduces p,nf(p,R) by REWRITE1:def 6;
then
A3: p,nf(p,R) are_convertible_wrt R by REWRITE1:25;
assume nf(p,PolyRedRel(G,T)) = nf(q,PolyRedRel(G,T));
hence p,q are_congruent_mod G-Ideal by A3,A2,POLYRED:57,REWRITE1:30;
end;
hence thesis by A1,POLYRED:58,REWRITE1:55;
end;
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, f being Polynomial of n,L, P being non
empty Subset of Polynom-Ring(n,L) st P is_Groebner_basis_wrt T holds f in P
-Ideal iff PolyRedRel(P,T) reduces f,0_(n,L)
by Th15,POLYRED:60;
Lm7: for n being Ordinal, T being connected TermOrder of n, L being Abelian
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, I
being LeftIdeal of Polynom-Ring(n,L), G being non empty Subset of Polynom-Ring(
n,L) st G c= I holds (for f being Polynomial of n,L st f in I holds PolyRedRel(
G,T) reduces f,0_(n,L)) implies G-Ideal = I
proof
let n be Ordinal, T be connected TermOrder of n, L be Abelian
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, I
be LeftIdeal of Polynom-Ring(n,L), G be non empty Subset of Polynom-Ring(n,L);
assume
A1: G c= I;
A2: now
let u be object;
assume
A3: u in G-Ideal;
G-Ideal c= I by A1,IDEAL_1:def 14;
hence u in I by A3;
end;
assume
A4: for f being Polynomial of n,L st f in I holds PolyRedRel(G,T)
reduces f,0_(n,L);
now
let u be object;
assume
A5: u in I;
then reconsider u9 = u as Element of Polynom-Ring(n,L);
reconsider u9 as Polynomial of n,L by POLYNOM1:def 11;
PolyRedRel(G,T) reduces u9,0_(n,L) by A4,A5;
hence u in G-Ideal by POLYRED:60;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th24: :: theorem 5.38 (o) ==> (i), p. 207
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, I being Subset of Polynom-Ring(n,L),
G being non empty Subset of Polynom-Ring(n,L) holds G is_Groebner_basis_of I,T
implies (for f being Polynomial of n,L st f in I holds PolyRedRel(G,T) reduces
f,0_(n,L))
by Th15;
theorem Th25: :: theorem 5.38 (i) ==> (ii), p. 207
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, G,
I being Subset of Polynom-Ring(n,L) holds (for f being Polynomial of n,L st f
in I holds PolyRedRel(G,T) reduces f,0_(n,L)) implies (for f being non-zero
Polynomial of n,L st f in I holds f is_reducible_wrt G,T)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, G,I be Subset
of Polynom-Ring(n,L);
assume
A1: for f being Polynomial of n,L st f in I holds PolyRedRel(G,T)
reduces f,0_(n,L);
now
let f be non-zero Polynomial of n,L;
assume f in I;
then
A2: PolyRedRel(G,T) reduces f,0_(n,L) by A1;
f <> 0_(n,L) by POLYNOM7:def 1;
then ex g being Polynomial of n,L st f reduces_to g,G,T & PolyRedRel(G,T)
reduces g,0_(n,L) by A2,Lm5;
hence f is_reducible_wrt G,T by POLYRED:def 9;
end;
hence thesis;
end;
theorem Th26: :: theorem 5.38 (ii) ==> (iii), p. 207
for n being Element of NAT, T being admissible connected
TermOrder of n, L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian almost_left_invertible
non degenerated non empty doubleLoopStr, I being add-closed left-ideal Subset
of Polynom-Ring(n,L), G being Subset of Polynom-Ring(n,L) st G c= I holds (for
f being non-zero Polynomial of n,L st f in I holds f is_reducible_wrt G,T)
implies (for f being non-zero Polynomial of n,L st f in I holds f
is_top_reducible_wrt G,T)
proof
let n be Element of NAT, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, I being add-closed left-ideal Subset of Polynom-Ring(n,L)
, P be Subset of Polynom-Ring(n,L);
assume
A1: P c= I;
assume
A2: for f being non-zero Polynomial of n,L st f in I holds f
is_reducible_wrt P,T;
thus for f being non-zero Polynomial of n,L st f in I holds f
is_top_reducible_wrt P,T
proof
set H = {g where g is non-zero Polynomial of n,L : g in I & not(g
is_top_reducible_wrt P,T)};
let f be non-zero Polynomial of n,L;
assume
A3: f in I;
assume not f is_top_reducible_wrt P,T;
then
A4: f in H by A3;
now
let u be object;
assume u in H;
then ex g9 being non-zero Polynomial of n,L st u = g9 & g9 in I & not g9
is_top_reducible_wrt P,T;
hence u in the carrier of Polynom-Ring(n,L);
end;
then reconsider H as non empty Subset of Polynom-Ring(n,L) by A4,
TARSKI:def 3;
consider p being Polynomial of n,L such that
A5: p in H and
A6: for q being Polynomial of n,L st q in H holds p <= q,T by POLYRED:31;
A7: ex p9 being non-zero Polynomial of n,L st p9 = p & p9 in I & not p9
is_top_reducible_wrt P,T by A5;
then reconsider p as non-zero Polynomial of n,L;
p is_reducible_wrt P,T by A2,A7;
then consider q being Polynomial of n,L such that
A8: p reduces_to q,P,T by POLYRED:def 9;
consider u being Polynomial of n,L such that
A9: u in P and
A10: p reduces_to q,u,T by A8,POLYRED:def 7;
ex b being bag of n st p reduces_to q,u,b,T by A10,POLYRED:def 6;
then
A11: u <> 0_(n,L) by POLYRED:def 5;
then reconsider u as non-zero Polynomial of n,L by POLYNOM7:def 1;
consider b being bag of n such that
A12: p reduces_to q,u,b,T by A10,POLYRED:def 6;
A13: now
assume b = HT(p,T);
then p top_reduces_to q,u,T by A12,POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A7,A9,POLYRED:def 12;
end;
consider m being Monomial of n,L such that
A14: q = p - m *' u by A10,Th1;
reconsider uu = u, pp = p, mm = m as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider uu,pp,mm as Element of Polynom-Ring(n,L);
mm * uu in I by A1,A9,IDEAL_1:def 2;
then -(mm * uu) in I by IDEAL_1:13;
then
A15: pp + -(mm * uu) in I by A7,IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 11;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then
A16: q in I by A14,A15;
A17: q < p,T by A10,POLYRED:43;
A18: p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then
A19: HT(p,T) in Support p by TERMORD:def 6;
b in Support p by A12,POLYRED:def 5;
then b <= HT(p,T),T by TERMORD:def 6;
then b < HT(p,T),T by A13,TERMORD:def 3;
then
A20: HT(p,T) in Support q by A19,A12,POLYRED:40;
now
per cases;
case
A21: q <> 0_(n,L);
then reconsider q as non-zero Polynomial of n,L by POLYNOM7:def 1;
Support q <> {} by A21,POLYNOM7:1;
then HT(q,T) in Support q by TERMORD:def 6;
then
A22: HT(q,T) <= HT(p,T),T by A10,POLYRED:42;
HT(p,T) <= HT(q,T),T by A20,TERMORD:def 6;
then
A23: HT(q,T) = HT(p,T) by A22,TERMORD:7;
now
assume not q is_top_reducible_wrt P,T;
then q in H by A16;
then p <= q,T by A6;
hence contradiction by A17,POLYRED:29;
end;
then consider u9 being Polynomial of n,L such that
A24: u9 in P and
A25: q is_top_reducible_wrt u9,T by POLYRED:def 12;
consider q9 being Polynomial of n,L such that
A26: q top_reduces_to q9,u9,T by A25,POLYRED:def 11;
A27: p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then
A28: HT(p,T) in Support p by TERMORD:def 6;
A29: q reduces_to q9,u9,HT(q,T),T by A26,POLYRED:def 10;
then consider s being bag of n such that
A30: s + HT(u9,T) = HT(q,T) and
q9 = q - (q.(HT(q,T))/HC(u9,T)) * (s *' u9) by POLYRED:def 5;
set qq = p - (p.(HT(p,T))/HC(u9,T)) * (s *' u9);
u9 <> 0_(n,L) by A29,POLYRED:def 5;
then p reduces_to qq,u9,HT(p,T),T by A23,A30,A27,A28,POLYRED:def 5;
then p top_reduces_to qq,u9,T by POLYRED:def 10;
then p is_top_reducible_wrt u9,T by POLYRED:def 11;
hence contradiction by A7,A24,POLYRED:def 12;
end;
case
q = 0_(n,L);
then
A31: m *' u = (p - m *' u) + m *' u by A14,POLYRED:2
.= (p + -(m *' u)) + m *' u by POLYNOM1:def 7
.= p + (-(m *' u) + m *' u) by POLYNOM1:21
.= p + 0_(n,L) by POLYRED:3
.= p by POLYNOM1:23;
m <> 0_(n,L) by A31,POLYRED:5,POLYNOM7:def 1;
then reconsider m as non-zero Polynomial of n,L by POLYNOM7:def 1;
set pp = p - (p.(HT(p,T))/HC(u,T)) * (HT(m,T) *' u);
HT(p,T) = HT(m,T) + HT(u,T) by A31,TERMORD:31;
then p reduces_to pp,u,HT(p,T),T by A11,A18,A19,POLYRED:def 5;
then p top_reduces_to pp,u,T by POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A7,A9,POLYRED:def 12;
end;
end;
hence thesis;
end;
end;
theorem Th27: :: theorem 5.38 (iii) ==> (iv), p. 207
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, G,
I being Subset of Polynom-Ring(n,L) holds (for f being non-zero Polynomial of n
,L st f in I holds f is_top_reducible_wrt G,T) implies (for b being bag of n st
b in HT(I,T) ex b9 being bag of n st b9 in HT(G,T) & b9 divides b)
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P,I be Subset
of Polynom-Ring(n,L);
assume
A1: for f being non-zero Polynomial of n,L st f in I holds f
is_top_reducible_wrt P,T;
now
let b be bag of n;
assume b in HT(I,T);
then consider p being Polynomial of n,L such that
A2: b = HT(p,T) and
A3: p in I and
A4: p <> 0_(n,L);
reconsider p as non-zero Polynomial of n,L by A4,POLYNOM7:def 1;
p is_top_reducible_wrt P,T by A1,A3;
then consider u being Polynomial of n,L such that
A5: u in P and
A6: p is_top_reducible_wrt u,T by POLYRED:def 12;
consider q being Polynomial of n,L such that
A7: p top_reduces_to q,u,T by A6,POLYRED:def 11;
A8: p reduces_to q,u,HT(p,T),T by A7,POLYRED:def 10;
then u <> 0_(n,L) by POLYRED:def 5;
then
A9: HT(u,T) in {HT(r,T) where r is Polynomial of n,L : r in P & r <> 0_(n
,L)} by A5;
ex s being bag of n st s + HT(u,T) = HT(p,T) & q = p - ( p.(HT(p,T))/
HC(u,T)) * (s *' u) by A8,POLYRED:def 5;
hence ex b9 being bag of n st b9 in HT(P,T) & b9 divides b by A2,A9,
PRE_POLY:50;
end;
hence thesis;
end;
theorem Th28: :: theorem 5.38 (iv) ==> (v), p. 207
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, G,
I being Subset of Polynom-Ring(n,L) holds (for b being bag of n st b in HT(I,T)
ex b9 being bag of n st b9 in HT(G,T) & b9 divides b) implies HT(I,T) c=
multiples(HT(G,T))
proof
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P,I being
Subset of Polynom-Ring(n,L);
assume
A1: for b being bag of n st b in HT(I,T) ex b9 being bag of n st b9 in
HT(P,T) & b9 divides b;
let u be object;
assume
A2: u in HT(I,T);
then reconsider u9 = u as Element of Bags n;
ex b9 being bag of n st b9 in HT(P,T) & b9 divides u9 by A1,A2;
hence u in multiples(HT(P,T));
end;
theorem Th29: :: theorem 5.38 (v) ==> (o), p. 207
for n being Element of NAT, T being connected admissible
TermOrder of n, L being Abelian add-associative right_complementable
right_zeroed commutative associative well-unital distributive
almost_left_invertible non degenerated non empty doubleLoopStr, I being
add-closed left-ideal non empty Subset of Polynom-Ring(n,L), G being non empty
Subset of Polynom-Ring(n,L) st G c= I holds HT(I,T) c= multiples(HT(G,T))
implies G is_Groebner_basis_of I,T
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I being add-closed left-ideal non empty Subset of
Polynom-Ring(n,L), P be non empty Subset of Polynom-Ring(n,L);
assume
A1: P c= I;
set R = PolyRedRel(P,T);
assume
A2: HT(I,T) c= multiples(HT(P,T));
A3: for f being Polynomial of n,L st f in I & f <> 0_(n,L) holds f
is_reducible_wrt P,T
proof
let f be Polynomial of n,L;
assume that
A4: f in I and
A5: f <> 0_(n,L);
HT(f,T) in {HT(p,T) where p is Polynomial of n,L : p in I & p <> 0_(n,
L)} by A4,A5;
then HT(f,T) in multiples(HT(P,T)) by A2;
then ex b being Element of Bags n st b = HT(f,T) & ex b9 being bag of n st
b9 in HT(P,T) & b9 divides b;
then consider b9 being bag of n such that
A6: b9 in HT(P,T) and
A7: b9 divides HT(f,T);
consider p being Polynomial of n,L such that
A8: b9 = HT(p,T) and
A9: p in P and
A10: p <> 0_(n,L) by A6;
consider s being bag of n such that
A11: b9 + s = HT(f,T) by A7,TERMORD:1;
set g = f - (f.(HT(f,T))/HC(p,T)) * (s *' p);
Support f <> {} by A5,POLYNOM7:1;
then HT(f,T) in Support f by TERMORD:def 6;
then f reduces_to g,p,HT(f,T),T by A5,A8,A10,A11,POLYRED:def 5;
then f reduces_to g,p,T by POLYRED:def 6;
then f reduces_to g,P,T by A9,POLYRED:def 7;
hence thesis by POLYRED:def 9;
end;
A12: PolyRedRel(P,T) c= PolyRedRel(I,T) by A1,Th4;
A13: for f being Polynomial of n,L st f in I holds R reduces f,0_(n,L)
proof
let f be Polynomial of n,L;
assume
A14: f in I;
per cases;
suppose
f = 0_(n,L);
hence thesis by REWRITE1:12;
end;
suppose
f <> 0_(n,L);
then f is_reducible_wrt P,T by A3,A14;
then consider v being Polynomial of n,L such that
A15: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in R by A15,POLYRED:def 13;
then f in field R by RELAT_1:15;
then f has_a_normal_form_wrt R by REWRITE1:def 14;
then consider g being object such that
A16: g is_a_normal_form_of f,R by REWRITE1:def 11;
A17: R reduces f,g by A16,REWRITE1:def 6;
then reconsider g9 = g as Polynomial of n,L by Lm4;
reconsider ff = f, gg = g9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider ff,gg as Element of Polynom-Ring(n,L);
f - g9 = ff - gg by Lm2;
then ff - gg in I-Ideal by A12,A17,POLYRED:59,REWRITE1:22;
then ff - gg in I by IDEAL_1:44;
then
A18: (ff - gg) - ff in I by A14,IDEAL_1:16;
(ff - gg) - ff = (ff + -gg) - ff
.= (ff + -gg) + -ff
.= (ff + -ff) + -gg by RLVECT_1:def 3
.= 0.(Polynom-Ring(n,L)) + -gg by RLVECT_1:5
.= - gg by ALGSTR_1:def 2;
then --gg in I by A18,IDEAL_1:14;
then
A19: g in I by RLVECT_1:17;
assume not R reduces f,0_(n,L);
then g <> 0_(n,L) by A16,REWRITE1:def 6;
then g9 is_reducible_wrt P,T by A3,A19;
then consider u being Polynomial of n,L such that
A20: g9 reduces_to u,P,T by POLYRED:def 9;
A21: [g9,u] in R by A20,POLYRED:def 13;
g is_a_normal_form_wrt R by A16,REWRITE1:def 6;
hence contradiction by A21,REWRITE1:def 5;
end;
end;
then
A22: P-Ideal = I by A1,Lm7;
now
let a,b,c being object;
assume that
A23: [a,b] in R and
A24: [a,c] in R;
consider a9,b9 being object such that
a9 in (NonZero Polynom-Ring(n,L)) and
A25: b9 in the carrier of Polynom-Ring(n,L) and
A26: [a,b] = [a9,b9] by A23,ZFMISC_1:def 2;
A27: b9 = b by A26,XTUPLE_0:1;
a,b are_convertible_wrt R by A23,REWRITE1:29;
then
A28: b,a are_convertible_wrt R by REWRITE1:31;
consider aa,c9 being object such that
aa in (NonZero Polynom-Ring(n,L)) and
A29: c9 in the carrier of Polynom-Ring(n,L) and
A30: [a,c] = [aa,c9] by A24,ZFMISC_1:def 2;
A31: c9 = c by A30,XTUPLE_0:1;
reconsider b9, c9 as Polynomial of n,L by A25,A29,POLYNOM1:def 11;
reconsider bb = b9, cc = c9 as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider bb,cc as Element of Polynom-Ring(n,L);
a,c are_convertible_wrt R by A24,REWRITE1:29;
then bb,cc are_congruent_mod I by A22,A27,A31,A28,POLYRED:57,REWRITE1:30;
then
A32: bb - cc in I by POLYRED:def 14;
b9 - c9 = bb - cc by Lm2;
hence b,c are_convergent_wrt R by A13,A27,A31,A32,POLYRED:50;
end;
then PolyRedRel(P,T) is locally-confluent by REWRITE1:def 24;
hence thesis by A22;
end;
begin :: Existence of Groebner Bases
theorem Th30:
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 trivial doubleLoopStr holds {0_(n,L)} is_Groebner_basis_of {0_(n,L)},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 trivial
doubleLoopStr;
set I = {0_(n,L)}, G = {0_(n,L)}, R = PolyRedRel(G,T);
A1: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
now
let a,b,c be object;
assume that
A2: [a,b] in R and
[a,c] in R;
consider p,q being object such that
A3: p in NonZero Polynom-Ring(n,L) and
A4: q in the carrier of Polynom-Ring(n,L) and
A5: [a,b] = [p,q] by A2,ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A4,POLYNOM1:def 11;
not p in {0_(n,L)} by A1,A3,XBOOLE_0:def 5;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L by A3,POLYNOM1:def 11
,POLYNOM7:def 1;
p reduces_to q,G,T by A2,A5,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A6: g in G and
A7: p reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A6,TARSKI:def 1;
then p is_reducible_wrt 0_(n,L),T by A7,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
then
A8: PolyRedRel(G,T) is locally-confluent by REWRITE1:def 24;
0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
then G-Ideal = I by IDEAL_1:44;
hence thesis by A8;
end;
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
trivial doubleLoopStr, p being Polynomial of n,L holds {p}
is_Groebner_basis_of {p}-Ideal,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 trivial
doubleLoopStr, p be Polynomial of n,L;
per cases;
suppose
A1: p = 0_(n,L);
0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
then {p}-Ideal = {0_(n,L)} by A1,IDEAL_1:44;
hence thesis by A1,Th30;
end;
suppose
p <> 0_(n,L);
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 1;
PolyRedRel({p},T) is locally-confluent by Th10;
hence thesis;
end;
end;
theorem
for T being admissible connected TermOrder of {}, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, I being add-closed left-ideal non empty Subset of
Polynom-Ring({},L), P being non empty Subset of Polynom-Ring({},L) st P c= I &
P <> {0_({},L)} holds P is_Groebner_basis_of I,T
proof
now
set j = the Element of {i where i is Element of NAT: i < 0};
assume {i where i is Element of NAT: i < 0} <> {};
then j in {i where i is Element of NAT: i < 0};
then ex i being Element of NAT st i = j & i < 0;
hence contradiction;
end;
then reconsider n = {} as Element of NAT;
let T be admissible connected TermOrder of {}, L be add-associative
right_complementable right_zeroed commutative associative well-unital
distributive Abelian almost_left_invertible non degenerated non empty
doubleLoopStr, I be add-closed left-ideal non empty Subset of Polynom-Ring({},
L), P be non empty Subset of Polynom-Ring({},L);
assume that
A1: P c= I and
A2: P <> {0_({},L)};
reconsider T as admissible connected TermOrder of n;
reconsider P as non empty Subset of Polynom-Ring(n,L);
reconsider I as add-closed left-ideal non empty Subset of Polynom-Ring(n,L);
A3: ex q being Element of P st q <> 0_(n,L)
proof
assume
A4: not(ex q being Element of P st q <> 0_(n,L));
A5: now
let u be object;
assume u in {0_(n,L)};
then
A6: u = 0_(n,L) by TARSKI:def 1;
now
assume not u in P;
then for v being object holds not v in P by A4,A6;
hence thesis by XBOOLE_0:def 1;
end;
hence u in P;
end;
now
let u be object;
assume u in P;
then u = 0_(n,L) by A4;
hence u in {0_(n,L)} by TARSKI:def 1;
end;
hence thesis by A2,A5,TARSKI:2;
end;
now
consider p being Element of P such that
A7: p <> 0_(n,L) by A3;
reconsider p as Polynomial of n,L by POLYNOM1:def 11;
reconsider p as non-zero Polynomial of n,L by A7,POLYNOM7:def 1;
let f be non-zero Polynomial of n,L;
assume f in I;
f <> 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 HT(p,T) = EmptyBag n & EmptyBag n in Support f;
then f is_reducible_wrt p,T by POLYRED:36;
then consider g being Polynomial of n,L such that
A8: f reduces_to g,p,T by POLYRED:def 8;
f reduces_to g,P,T by A8,POLYRED:def 7;
hence f is_reducible_wrt P,T by POLYRED:def 9;
end;
then for f being non-zero Polynomial of n,L st f in I holds f
is_top_reducible_wrt P,T by A1,Th26;
then
for b being bag of n st b in HT(I,T) ex b9 being bag of n st b9 in HT(P
,T) & b9 divides b by Th27;
then HT(I,T) c= multiples(HT(P,T)) by Th28;
hence thesis by A1,Th29;
end;
theorem
for n being non empty Ordinal, T being admissible connected TermOrder
of n, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr ex P be Subset of Polynom-Ring(n,L) st not(P
is_Groebner_basis_wrt T)
proof
let n be non empty Ordinal, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non degenerated non empty
doubleLoopStr;
set 1bag = (EmptyBag n)+*({},1);
reconsider 1bag as Element of Bags n by PRE_POLY:def 12;
set p = ((1.L) |(n,L))+*(1bag,1.L);
reconsider p as Function of Bags n,L;
reconsider p as Series of n,L;
A1: 1.L <> 0.L;
set q = (0.L |(n,L))+*(1bag,1.L);
reconsider q as Function of Bags n,L;
reconsider q as Series of n,L;
A2: now
let u be bag of n;
assume that
A3: u <> EmptyBag n and
A4: u <> 1bag;
p.u = ((1.L) |(n,L)).u by A4,FUNCT_7:32;
then p.u = (1_(n,L)).u by POLYNOM7:20;
hence p.u = 0.L by A3,POLYNOM1:25;
end;
A5: now
let u9 be object;
assume
A6: u9 in Support p;
then reconsider u = u9 as Element of Bags n;
A7: p.u <> 0.L by A6,POLYNOM1:def 4;
now
assume not u in {EmptyBag n,1bag};
then u <> EmptyBag n & u <> 1bag by TARSKI:def 2;
hence contradiction by A2,A7;
end;
hence u9 in {EmptyBag n,1bag};
end;
{} in n & dom EmptyBag n = n by ORDINAL1:14,PARTFUN1:def 2;
then 1bag.{} = 1 by FUNCT_7:31;
then
A8: EmptyBag n <> 1bag by PBOOLE:5;
then
A9: q.(EmptyBag n) = (0.L |(n,L)).(EmptyBag n) by FUNCT_7:32
.= (0_(n,L)).(EmptyBag n) by POLYNOM7:19
.= 0.L by POLYNOM1:22;
A10: now
let u be bag of n;
assume u <> 1bag;
then q.u = (0.L |(n,L)).u by FUNCT_7:32;
then q.u = (0_(n,L)).u by POLYNOM7:19;
hence q.u = 0.L by POLYNOM1:22;
end;
A11: now
let u9 be object;
assume
A12: u9 in Support q;
then reconsider u = u9 as Element of Bags n;
A13: q.u <> 0.L by A12,POLYNOM1:def 4;
now
assume not u in {1bag};
then u <> 1bag by TARSKI:def 1;
hence contradiction by A10,A13;
end;
hence u9 in {1bag};
end;
dom(0.L |(n,L)) = Bags n by FUNCT_2:def 1;
then
A14: q.(1bag) = 1.L by FUNCT_7:31;
then
A15: q <> 0_(n,L) by POLYNOM1:22;
now
let u be object;
assume u in {1bag};
then u = 1bag by TARSKI:def 1;
hence u in Support q by A14,POLYNOM1:def 4;
end;
then
A16: Support q = {1bag} by A11,TARSKI:2;
then reconsider q as Polynomial of n,L by POLYNOM1:def 5;
reconsider q as non-zero Polynomial of n,L by A15,POLYNOM7:def 1;
set q1 = q - (q.HT(q,T)/HC(q,T)) * ((EmptyBag n) *' q);
Support q <> {} by A15,POLYNOM7:1;
then
A17: HT(q,T) in Support q by TERMORD:def 6;
EmptyBag n + HT(q,T) = HT(q,T) by PRE_POLY:53;
then q reduces_to q1,q,HT(q,T),T by A15,A17,POLYRED:def 5;
then
A18: q reduces_to q1,q,T by POLYRED:def 6;
A19: q1 = q - (HC(q,T)/HC(q,T)) * ((EmptyBag n) *' q) by TERMORD:def 7
.= q - (HC(q,T)*(HC(q,T))") * ((EmptyBag n) *' q)
.= q - 1.L * ((EmptyBag n) *' q) by VECTSP_1:def 10
.= q - 1.L * q by POLYRED:17
.= q - (1.L) |(n,L) *' q by POLYNOM7:27
.= q - 1_(n,L) *' q by POLYNOM7:20
.= q - q by POLYNOM1:30
.= 0_(n,L) by POLYNOM1:24;
A20: dom((1.L) |(n,L)) = Bags n by FUNCT_2:def 1;
then
A21: p.(1bag) = 1.L by FUNCT_7:31;
then
A22: p <> 0_(n,L) by A1,POLYNOM1:22;
A23: p.(EmptyBag n) = ((1.L) |(n,L)).(EmptyBag n) by A8,FUNCT_7:32
.= (1_(n,L)).(EmptyBag n) by POLYNOM7:20
.= 1.L by POLYNOM1:25;
now
let u be object;
assume
A24: u in {EmptyBag n,1bag};
now
per cases by A24,TARSKI:def 2;
case
u = EmptyBag n;
hence u in Support p by A1,A23,POLYNOM1:def 4;
end;
case
u = 1bag;
hence u in Support p by A1,A21,POLYNOM1:def 4;
end;
end;
hence u in Support p;
end;
then
A25: Support p = {EmptyBag n,1bag} by A5,TARSKI:2;
then reconsider p as Polynomial of n,L by POLYNOM1:def 5;
reconsider p as non-zero Polynomial of n,L by A22,POLYNOM7:def 1;
A26: EmptyBag n + HT(p,T) = HT(p,T) by PRE_POLY:53;
A27: now
A28: EmptyBag n <= 1bag,T by TERMORD:9;
assume
A29: HT(p,T) = EmptyBag n;
1bag in Support p by A25,TARSKI:def 2;
then 1bag <= EmptyBag n,T by A29,TERMORD:def 6;
hence contradiction by A8,A28,TERMORD:7;
end;
set p1 = q - (q.HT(p,T)/HC(p,T)) * ((EmptyBag n) *' p);
Support p <> {} by A22,POLYNOM7:1;
then
A30: HT(p,T) in Support p by TERMORD:def 6;
then
A31: HT(p,T) = 1bag by A25,A27,TARSKI:def 2;
then HT(p,T) in Support q by A16,TARSKI:def 1;
then q reduces_to p1,p,HT(p,T),T by A22,A15,A26,POLYRED:def 5;
then
A32: q reduces_to p1,p,T by POLYRED:def 6;
A33: now
assume Support q = Support p;
then EmptyBag n in {1bag} by A25,A16,TARSKI:def 2;
hence contradiction by A8,TARSKI:def 1;
end;
A34: now
assume q - p = 0_(n,L);
then p = (q-p)+p by POLYRED:2
.= (q+-p)+p by POLYNOM1:def 7
.= q+(-p+p) by POLYNOM1:21
.= q + 0_(n,L) by POLYRED:3;
hence contradiction by A33,POLYNOM1:23;
end;
set P = {p,q};
now
let u be object;
assume u in P;
then u = p or u = q by TARSKI:def 2;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
then reconsider P as Subset of Polynom-Ring(n,L) by TARSKI:def 3;
reconsider P as Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
take P;
A35: p in P by TARSKI:def 2;
q in P by TARSKI:def 2;
then q reduces_to 0_(n,L),P,T by A18,A19,POLYRED:def 7;
then
A36: [q,0_(n,L)] in R by POLYRED:def 13;
p1 = q - (1.L/p.1bag) * ((EmptyBag n) *' p) by A14,A31,TERMORD:def 7
.= q - (1.L/1.L) * ((EmptyBag n) *' p) by A20,FUNCT_7:31
.= q - (1.L*(1.L)") * ((EmptyBag n) *' p)
.= q - 1.L * ((EmptyBag n) *' p) by VECTSP_1:def 10
.= q - 1.L * p by POLYRED:17
.= q - (1.L) |(n,L) *' p by POLYNOM7:27
.= q - 1_(n,L) *' p by POLYNOM7:20
.= q - p by POLYNOM1:30;
then q reduces_to q-p,P,T by A32,A35,POLYRED:def 7;
then
A37: [q,q-p] in R by POLYRED:def 13;
now
A38: now
let u be object;
now
let u be object;
assume u in {1bag};
then u = 1bag by TARSKI:def 1;
hence u in {EmptyBag n,1bag} by TARSKI:def 2;
end;
then {1bag} c= {EmptyBag n,1bag};
then
A39: {1bag} \/ {EmptyBag n,1bag} = {EmptyBag n,1bag} by XBOOLE_1:12;
A40: (q-p).1bag = (q+-p).1bag by POLYNOM1:def 7
.= q.1bag + (-p).1bag by POLYNOM1:15
.= q.1bag + -(p.1bag) by POLYNOM1:17
.= 1.L + -1.L by A20,A14,FUNCT_7:31
.= 0.L by RLVECT_1:5;
Support(q-p) = Support (q+-p) by POLYNOM1:def 7;
then Support(q-p) c= Support(q) \/ Support(-p) by POLYNOM1:20;
then
A41: Support(q-p) c= {1bag} \/ {EmptyBag n,1bag} by A25,A16,Th5;
assume
A42: u in Support(q-p);
then (q-p).u <> 0.L by POLYNOM1:def 4;
then u = EmptyBag n by A42,A41,A39,A40,TARSKI:def 2;
hence u in {EmptyBag n} by TARSKI:def 1;
end;
assume R is locally-confluent;
then 0_(n,L),q-p are_convergent_wrt R by A37,A36,REWRITE1:def 24;
then consider c being object such that
A43: R reduces 0_(n,L),c and
A44: R reduces q-p,c by REWRITE1:def 7;
reconsider c as Polynomial of n,L by A43,Lm4;
consider s being FinSequence such that
A45: len s > 0 and
A46: s.1 = 0_(n,L) and
A47: s.len s = c and
A48: for i being Nat st i in dom s & i+1 in dom s holds [s.
i, s.(i+1)] in R by A43,REWRITE1:11;
now
A49: 0 + 1 <= len s by A45,NAT_1:13;
A50: dom s = Seg(len s) by FINSEQ_1:def 3;
assume len s <> 1;
then 1 < len s by A49,XXREAL_0:1;
then 1+1 <= len s by NAT_1:13;
then
A51: 1+1 in dom s by A50,FINSEQ_1:1;
A52: 1 in dom s by A49,A50,FINSEQ_1:1;
then consider f9,h9 being object such that
A53: [0_(n,L),s.2] = [f9,h9] and
f9 in NonZero Polynom-Ring(n,L) and
A54: h9 in (the carrier of Polynom-Ring(n,L)) by A46,A48,A51,RELSET_1:2;
s.2 = h9 by A53,XTUPLE_0:1;
then reconsider c9 = s.2 as Polynomial of n,L by A54,POLYNOM1:def 11;
[s.1,s.2] in R by A48,A52,A51;
then 0_(n,L) reduces_to c9,P,T by A46,POLYRED:def 13;
then consider g being Polynomial of n,L such that
g in P and
A55: 0_(n,L) reduces_to c9,g,T by POLYRED:def 7;
0_(n,L) is_reducible_wrt g,T by A55,POLYRED:def 8;
hence contradiction by POLYRED:37;
end;
then consider s being FinSequence such that
A56: len s > 0 and
A57: s.1 = q-p and
A58: s.len s = 0_(n,L) and
A59: for i being Nat st i in dom s & i+1 in dom s holds [s
.i, s.(i+1)] in R by A44,A46,A47,REWRITE1:11;
A60: now
assume -1.L = 0.L;
then --1.L = 0.L by RLVECT_1:12;
hence contradiction by RLVECT_1:17;
end;
now
let u be object;
assume
A61: u in {EmptyBag n};
then reconsider u9 = u as Element of Bags n by TARSKI:def 1;
(q-p).u9 = (q+-p).u9 by POLYNOM1:def 7
.= q.u9 + (-p).u9 by POLYNOM1:15
.= q.u9 + -(p.u9) by POLYNOM1:17
.= 0.L + -(p.u9) by A9,A61,TARSKI:def 1
.= 0.L + -1.L by A23,A61,TARSKI:def 1
.= -1.L by ALGSTR_1:def 2;
hence u in Support(q-p) by A60,POLYNOM1:def 4;
end;
then
A62: Support(q-p) = {EmptyBag n} by A38,TARSKI:2;
A63: now
assume q-p is_reducible_wrt P,T;
then consider g being Polynomial of n,L such that
A64: q-p reduces_to g,P,T by POLYRED:def 9;
consider h being Polynomial of n,L such that
A65: h in P and
A66: q-p reduces_to g,h,T by A64,POLYRED:def 7;
ex b being bag of n st q-p reduces_to g,h,b,T by A66,POLYRED:def 6;
then h <> 0_(n,L) by POLYRED:def 5;
then reconsider h as non-zero Polynomial of n,L by POLYNOM7:def 1;
q-p is_reducible_wrt h,T by A66,POLYRED:def 8;
then consider b9 being bag of n such that
A67: b9 in Support(q-p) and
A68: HT(h,T) divides b9 by POLYRED:36;
A69: HT(h,T) = 1bag
proof
now
per cases by A65,TARSKI:def 2;
case
h = p;
hence thesis by A25,A30,A27,TARSKI:def 2;
end;
case
h = q;
hence thesis by A16,A17,TARSKI:def 1;
end;
end;
hence thesis;
end;
b9 = EmptyBag n by A62,A67,TARSKI:def 1;
hence contradiction by A8,A68,A69,PRE_POLY:58;
end;
now
A70: 0 + 1 <= len s by A56,NAT_1:13;
A71: dom s = Seg(len s) by FINSEQ_1:def 3;
assume len s <> 1;
then 1 < len s by A70,XXREAL_0:1;
then 1+1 <= len s by NAT_1:13;
then
A72: 1+1 in dom s by A71,FINSEQ_1:1;
A73: 1 in dom s by A70,A71,FINSEQ_1:1;
then consider f9,h9 being object such that
A74: [q-p,s.2] = [f9,h9] and
f9 in NonZero Polynom-Ring(n,L) and
A75: h9 in (the carrier of Polynom-Ring(n,L)) by A57,A59,A72,RELSET_1:2;
s.2 = h9 by A74,XTUPLE_0:1;
then reconsider c9 = s.2 as Polynomial of n,L by A75,POLYNOM1:def 11;
[q-p,s.2] in R by A57,A59,A73,A72;
then q-p reduces_to c9,P,T by POLYRED:def 13;
hence contradiction by A63,POLYRED:def 9;
end;
hence contradiction by A34,A57,A58;
end;
hence thesis;
end;
Lm8: for n being Ordinal, b1,b2,b3 being bag of n holds b1 divides b2 & b2
divides b3 implies b1 divides b3
proof
let n be Ordinal, b1,b2,b3 be bag of n;
assume
A1: b1 divides b2 & b2 divides b3;
now
let k be object;
b1.k <= b2.k & b2.k <= b3.k by A1,PRE_POLY:def 11;
hence b1.k <= b3.k by XXREAL_0:2;
end;
hence thesis by PRE_POLY:def 11;
end;
definition :: definition preceeding 5.1, p. 189
let n be Ordinal;
func DivOrder(n) -> Order of Bags n means
:Def5:
for b1,b2 being bag of n holds [b1,b2] in it iff b1 divides b2;
existence
proof
defpred P[object,object] means
ex b1, b2 being Element of Bags n st $1 = b1 & $2
= b2 & b1 divides b2;
consider BO being Relation of Bags n, Bags n such that
A1: for x,y being object holds [x,y] in BO iff x in Bags n & y in Bags n
& P[x,y] from RELSET_1:sch 1;
A2: BO is_transitive_in Bags n
proof
let x,y,z be object such that
x in Bags n and
y in Bags n and
z in Bags n and
A3: [x,y] in BO and
A4: [y,z] in BO;
consider b1,b2 being Element of Bags n such that
A5: x = b1 and
A6: y = b2 & b1 divides b2 by A1,A3;
consider b11, b22 being Element of Bags n such that
A7: y = b11 and
A8: z = b22 and
A9: b11 divides b22 by A1,A4;
reconsider B1 = b1, B29 = b22 as bag of n;
B1 divides B29 by A6,A7,A9,Lm8;
hence thesis by A1,A5,A8;
end;
A10: BO is_reflexive_in Bags n
by A1;
then
A11: dom BO = Bags n & field BO = Bags n by ORDERS_1:13;
BO is_antisymmetric_in Bags n
proof
let x,y be object;
assume that
x in Bags n and
y in Bags n and
A12: [x,y] in BO and
A13: [y,x] in BO;
consider b19, b29 being Element of Bags n such that
A14: y = b19 & x = b29 and
A15: b19 divides b29 by A1,A13;
consider b11, b22 being Element of Bags n such that
A16: x = b11 & y = b22 and
A17: b11 divides b22 by A1,A12;
reconsider b11, b22 as bag of n;
A18: now
let k be object;
assume k in dom b11;
b11.k <= b22.k & b19.k <= b29.k by A17,A15,PRE_POLY:def 11;
hence b11.k = b22.k by A16,A14,XXREAL_0:1;
end;
dom b11 = n by PARTFUN1:def 2
.= dom b22 by PARTFUN1:def 2;
hence thesis by A16,A18,FUNCT_1:2;
end;
then reconsider BO as Order of Bags n by A10,A2,A11,PARTFUN1:def 2
,RELAT_2:def 9,def 12,def 16;
take BO;
let p, q be bag of n;
hereby
assume [p, q] in BO;
then ex b19, b29 being Element of Bags n st p = b19 & q = b29 & b19
divides b29 by A1;
hence p divides q;
end;
p in Bags n & q in Bags n by PRE_POLY:def 12;
hence thesis by A1;
end;
uniqueness
proof
let B1, B2 be Order of Bags n such that
A19: for p,q being bag of n holds [p, q] in B1 iff p divides q and
A20: for p,q being bag of n holds [p, q] in B2 iff p divides q;
let a, b be object;
hereby
assume
A21: [a,b] in B1;
then consider b1, b2 being object such that
A22: [a,b] = [b1,b2] and
A23: b1 in Bags n & b2 in Bags n by RELSET_1:2;
reconsider b1, b2 as bag of n by A23;
b1 divides b2 by A19,A21,A22;
hence [a,b] in B2 by A20,A22;
end;
assume
A24: [a,b] in B2;
then consider b1, b2 being object such that
A25: [a,b] = [b1,b2] and
A26: b1 in Bags n & b2 in Bags n by RELSET_1:2;
reconsider b1, b2 as bag of n by A26;
b1 divides b2 by A20,A24,A25;
hence thesis by A19,A25;
end;
end;
registration :: theorem 5.2, p. 189
let n be Element of NAT;
cluster RelStr(#Bags n, DivOrder n#) -> Dickson;
coherence
proof
set R = RelStr(#Bags n, DivOrder n#);
set S = product Carrier (n --> OrderedNAT), SJ = Carrier (n --> OrderedNAT
);
set P = product (n --> OrderedNAT), J = n --> OrderedNAT;
defpred Q[object,object] means
$1 in S & (ex b being bag of n st b = $2 & b = $1);
A1: for x being set st x in S for g being Function st x = g holds dom g =
n & for y being set st y in dom g holds g.y in NAT
proof
let x be set;
assume x in S;
then consider g being Function such that
A2: x = g and
A3: dom g = dom SJ and
A4: for y being object st y in dom SJ holds g.y in SJ.y by CARD_3:def 5;
let g9 be Function;
assume
A5: x = g9;
hence dom g9 = n by A2,A3,PARTFUN1:def 2;
thus for y being set st y in dom g9 holds g9.y in NAT
proof
let y be set;
assume
A6: y in dom g9;
then
A7: y in n by A5,A2,A3;
then consider R being 1-sorted such that
A8: R = J.y and
A9: SJ.y = the carrier of R by PRALG_1:def 15;
g.y in the carrier of R by A5,A2,A3,A4,A6,A9;
hence thesis by A5,A2,A7,A8,DICKSON:def 15,FUNCOP_1:7;
end;
end;
A10: for x being object st x in S ex y being object st Q[x,y]
proof
let x be object;
assume
A11: x in S;
then consider g being Function such that
A12: x = g and
dom g = dom SJ and
for y being object st y in dom SJ holds g.y in SJ.y by CARD_3:def 5;
defpred QQ[object,object] means $2 = g.$1;
A13: for x being object st x in n ex y being object st QQ[x,y];
consider b being Function such that
A14: dom b = n & for x being object st x in n holds QQ[x,b.x] from
CLASSES1:sch 1(A13);
reconsider b as ManySortedSet of n by A14,PARTFUN1:def 2,RELAT_1:def 18;
A15: dom g = n by A1,A11,A12;
now
let u be object;
assume u in rng b;
then consider x being object such that
A16: x in dom b & u = b.x by FUNCT_1:def 3;
u = g.x & x in dom g by A15,A14,A16;
hence u in NAT by A1,A11,A12;
end;
then rng b c= NAT;
then reconsider b as bag of n by VALUED_0:def 6;
take b;
thus x in S by A11;
take b;
thus b = b;
b = g by A15,A14,FUNCT_1:2;
hence thesis by A12;
end;
consider i being Function such that
A17: dom i = S & for x being object st x in S holds Q[x,i.x] from
CLASSES1:sch 1(A10);
A18: for x being Element of R holds ex u being Element of P st u in dom i
& i.u = x
proof
let x be Element of R;
reconsider g = x as bag of n;
A19: now
let x be object;
assume x in dom(Carrier J);
then
A20: x in n;
then consider L being 1-sorted such that
A21: L = J.x and
A22: (Carrier J).x = the carrier of L by PRALG_1:def 15;
the carrier of L = NAT by A20,A21,DICKSON:def 15,FUNCOP_1:7;
hence g.x in (Carrier J).x by A22, ORDINAL1:def 12;
end;
A23: dom g = n by PARTFUN1:def 2
.= dom(Carrier J) by PARTFUN1:def 2;
then
A24: g in product Carrier J by A19,CARD_3:def 5;
then reconsider g as Element of P by YELLOW_1:def 4;
take g;
thus g in dom i by A17,A23,A19,CARD_3:def 5;
Q[g,i.g] by A17,A24;
hence thesis;
end;
A25: now
let v be set;
assume v in rng i;
then consider u being object such that
A26: u in dom i and
A27: v = i.u by FUNCT_1:def 3;
ex b being bag of n st b = i.u & b = u by A17,A26;
hence v in Bags n by A27,PRE_POLY:def 12;
end;
now
let N be Subset of R;
set N9 = i"N;
A28: N9 c= S by A17,RELAT_1:132;
then reconsider N9 as Subset of P by YELLOW_1:def 4;
consider B9 being set such that
A29: B9 is_Dickson-basis_of N9,P and
A30: B9 is finite by DICKSON:def 10;
set B = i.:B9;
A31: B9 c= N9 by A29,DICKSON:def 9;
A32: for a,b being Element of P, ta,tb being Element of Bags n st a = ta
& b = tb & a in S holds a <= b implies ta divides tb
proof
let a,b being Element of P, ta,tb being Element of Bags n;
assume that
A33: a = ta & b = tb and
A34: a in S;
assume a <= b;
then consider f,g being Function such that
A35: f = a & g = b and
A36: for i be object st i in n ex R being RelStr, ai,bi being Element
of R st R = J.i & ai = f.i & bi = g.i & ai <= bi by A34,YELLOW_1:def 4;
now
let k be object;
assume
A37: k in n;
then consider R being RelStr, ak,bk being Element of R such that
A38: R = J.k and
A39: ak = f.k & bk = g.k and
A40: ak <= bk by A36;
J.k = OrderedNAT by A37,FUNCOP_1:7;
then [ak,bk] in NATOrd by A38,A40,DICKSON:def 15,ORDERS_2:def 5;
then consider a9,b9 being Element of NAT such that
A41: [a9,b9] = [ak,bk] and
A42: a9 <= b9 by DICKSON:def 14;
A43: b9 = bk by A41,XTUPLE_0:1;
a9 = ak by A41,XTUPLE_0:1;
hence ta.k <= tb.k by A33,A35,A39,A42,A43;
end;
hence thesis by PRE_POLY:46;
end;
A44: for a being Element of R st a in N ex b being Element of R st b in
B & b <= a
proof
let a be Element of R;
consider a9 being Element of P such that
A45: a9 in dom i and
A46: i.a9 = a by A18;
A47: ex b being bag of n st b = i.a9 & b = a9 by A17,A45;
assume a in N;
then a9 in N9 by A45,A46,FUNCT_1:def 7;
then consider b9 being Element of P such that
A48: b9 in B9 and
A49: b9 <= a9 by A29,DICKSON:def 9;
set b = i.b9;
A50: B9 c= S by A28,A31;
then b in rng i by A17,A48,FUNCT_1:def 3;
then reconsider b as Element of Bags n by A25;
reconsider b as Element of R;
take b;
thus b in B by A17,A48,A50,FUNCT_1:def 6;
reconsider aa = a, bb = b as Element of Bags n;
ex b1 being bag of n st b1 = i.b9 & b1 = b9 by A17,A48,A50;
then bb divides aa by A32,A46,A47,A48,A49,A50;
then [b,a] in DivOrder(n) by Def5;
hence thesis by ORDERS_2:def 5;
end;
now
let u be object;
assume u in B;
then ex v being object st v in dom i & v in B9 & u = i.v
by FUNCT_1:def 6;
hence u in N by A31,FUNCT_1:def 7;
end;
then B c= N;
then B is_Dickson-basis_of N,R by A44,DICKSON:def 9;
hence ex B being set st B is_Dickson-basis_of N,R & B is finite by A30;
end;
hence thesis by DICKSON:def 10;
end;
end;
theorem Th34: :: theorem 5.2, p. 189
for n being Element of NAT, N being Subset of RelStr(#Bags n,
DivOrder n#) ex B being finite Subset of Bags n st B is_Dickson-basis_of N,
RelStr(#Bags n, DivOrder n#)
proof
let n be Element of NAT, N be Subset of RelStr(#Bags n, DivOrder n#);
consider B being set such that
A1: B is_Dickson-basis_of N,RelStr(#Bags n, DivOrder n#) and
A2: B is finite by DICKSON:def 10;
now
let u be object;
assume
A3: u in B;
B c= N by A1,DICKSON:def 9;
hence u in N by A3;
end;
then reconsider B as finite Subset of N by A2,TARSKI:def 3;
reconsider B as finite Subset of Bags n by XBOOLE_1:1;
take B;
thus thesis by A1;
end;
theorem Th35: :: theorem 5.41, p. 208
for n being Element of NAT, T being connected admissible
TermOrder of n, L being Abelian add-associative right_complementable
right_zeroed commutative associative well-unital distributive
almost_left_invertible non degenerated non empty doubleLoopStr, I being
add-closed left-ideal non empty Subset of Polynom-Ring(n,L) ex G being finite
Subset of Polynom-Ring(n,L) st G is_Groebner_basis_of I,T
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of
Polynom-Ring(n,L);
A1: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
per cases;
suppose
A2: I = {0_(n,L)};
set G = {0_(n,L)}, R = PolyRedRel(G,T);
take G;
now
let a,b,c be object;
assume that
A3: [a,b] in R and
[a,c] in R;
consider p,q being object such that
A4: p in NonZero Polynom-Ring(n,L) and
A5: q in the carrier of Polynom-Ring(n,L) and
A6: [a,b] = [p,q] by A3,ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A5,POLYNOM1:def 11;
not p in {0_(n,L)} by A1,A4,XBOOLE_0:def 5;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L by A4,POLYNOM1:def 11
,POLYNOM7:def 1;
p reduces_to q,G,T by A3,A6,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A7: g in G and
A8: p reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A7,TARSKI:def 1;
then p is_reducible_wrt 0_(n,L),T by A8,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
then
A9: PolyRedRel(G,T) is locally-confluent by REWRITE1:def 24;
G-Ideal = I by A2,IDEAL_1:44;
hence thesis by A9;
end;
suppose
A10: I <> {0_(n,L)};
ex q being Element of I st q <> 0_(n,L)
proof
assume
A11: not(ex q being Element of I st q <> 0_(n,L));
A12: now
let u be object;
assume u in {0_(n,L)};
then
A13: u = 0_(n,L) by TARSKI:def 1;
now
assume not u in I;
then for v being object holds not v in I by A11,A13;
hence thesis by XBOOLE_0:def 1;
end;
hence u in I;
end;
now
let u be object;
assume u in I;
then u = 0_(n,L) by A11;
hence u in {0_(n,L)} by TARSKI:def 1;
end;
hence thesis by A10,A12,TARSKI:2;
end;
then consider q being Element of I such that
A14: q <> 0_(n,L);
set R = RelStr(#Bags n, DivOrder n#), hti = HT(I,T);
reconsider hti as Subset of R;
consider S being finite Subset of Bags n such that
A15: S is_Dickson-basis_of hti,R by Th34;
set M = { {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p <> 0_
(n,L)} where s is Element of Bags n : s in S};
set s = the Element of S;
reconsider q as Polynomial of n,L by POLYNOM1:def 11;
set hq = HT(q,T);
reconsider hq as Element of R;
hq in {HT(p,T) where p is Polynomial of n,L : p in I & p <> 0_(n,L) }
by A14;
then ex b being Element of R st b in S & b <= hq by A15,DICKSON:def 9;
then s in S;
then
{r where r is Polynomial of n,L : r in I & HT(r,T) = s & r <> 0_(n,L)
} in { {p where p is Polynomial of n,L : p in I & HT(p,T) = s9 & p <> 0_(n,L)}
where s9 is Element of Bags n : s9 in S};
then reconsider M as non empty set;
A16: for x,y being set st x in M & y in M & x <> y holds x misses y
proof
let x,y be set;
assume that
A17: x in M and
A18: y in M and
A19: x <> y;
consider t being Element of Bags n such that
A20: y = {p where p is Polynomial of n,L : p in I & HT(p,T) = t & p
<> 0_(n, L)} and
t in S by A18;
consider s being Element of Bags n such that
A21: x = {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p
<> 0_(n, L)} and
s in S by A17;
reconsider x,y as set;
now
set u = the Element of x /\ y;
assume
A22: x /\ y <> {};
then u in y by XBOOLE_0:def 4;
then
A23: ex v being Polynomial of n,L st u = v & v in I & HT(v,T ) = t & v
<> 0_(n,L) by A20;
u in x by A22,XBOOLE_0:def 4;
then ex r being Polynomial of n,L st u = r & r in I & HT(r,T ) = s & r
<> 0_(n,L) by A21;
hence contradiction by A19,A21,A20,A23;
end;
hence thesis by XBOOLE_0:def 7;
end;
A24: S c= hti by A15,DICKSON:def 9;
for x being set st x in M holds x <> {}
proof
let x be set;
assume x in M;
then consider s being Element of Bags n such that
A25: x = {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p
<> 0_(n, L)} and
A26: s in S;
s in hti by A24,A26;
then consider q being Polynomial of n,L such that
A27: s = HT(q,T) & q in I & q <> 0_(n,L);
q in x by A25,A27;
hence thesis;
end;
then consider G9 being set such that
A28: for x being set st x in M ex y being object st G9 /\ x = {y} by A16,
WELLORD2:18;
set xx = the Element of M;
A29: M is finite
proof
defpred P[object,object] means
$2 = {p where p is Polynomial of n,L : p in I &
HT(p,T) = $1 & p <> 0_(n,L)};
A30: for x being object st x in S ex y being object st P[x,y];
consider f being Function such that
A31: dom f = S & for x being object st x in S holds P[x,f.x] from
CLASSES1:sch 1(A30);
A32: now
let u be object;
assume u in rng f;
then consider s being object such that
A33: s in dom f and
A34: u = f.s by FUNCT_1:def 3;
u = {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p <>
0_(n,L)} by A31,A33,A34;
hence u in M by A31,A33;
end;
now
let u be object;
assume u in M;
then consider s being Element of Bags n such that
A35: u = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n, L)} and
A36: s in S;
f.s in rng f by A31,A36,FUNCT_1:3;
hence u in rng f by A31,A35,A36;
end;
then rng f = M by A32,TARSKI:2;
hence thesis by A31,FINSET_1:8;
end;
A37: ex y being object st G9 /\ xx = {y} by A28;
set xx = the Element of M;
reconsider G9 as non empty set by A37;
set G = { x where x is Element of G9 : ex y being set st y in M & G9 /\ y
= {x}};
now
let u be object;
assume u in G;
then consider x being Element of G9 such that
A38: u = x and
A39: ex y being set st y in M & G9 /\ y = {x};
consider y being set such that
A40: y in M and
A41: G9 /\ y = {x} by A39;
consider s being Element of Bags n such that
A42: y = {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p
<> 0_(n, L)} and
s in S by A40;
x in (G9 /\ y) by A41,TARSKI:def 1;
then x in y by XBOOLE_0:def 4;
then
ex q being Polynomial of n,L st x = q & q in I & HT(q,T ) = s & q <>
0_(n,L) by A42;
hence u in the carrier of Polynom-Ring(n,L) by A38;
end;
then reconsider G as Subset of Polynom-Ring(n,L) by TARSKI:def 3;
defpred P[object,object] means
ex D1 being set st D1 = $1 & G9 /\ D1 = {$2} & $2 in G;
A43: for x being object st x in M ex y being object st P[x,y]
proof
let x be object;
assume
A44: x in M;
reconsider xx=x as set by TARSKI:1;
consider y being object such that
A45: G9 /\ xx = {y} by A28,A44;
y in (G9 /\ xx) by A45,TARSKI:def 1;
then reconsider y as Element of G9 by XBOOLE_0:def 4;
y in G by A44,A45;
hence thesis by A45;
end;
consider f being Function such that
A46: dom f = M & for x being object st x in M holds P[x,f.x] from
CLASSES1:sch 1(A43);
A47: now
let u be object;
assume u in G;
then consider x being Element of G9 such that
A48: u = x and
A49: ex y being set st y in M & G9 /\ y = {x};
consider y being set such that
A50: y in M and
A51: G9 /\ y = {x} by A49;
P[y,f.y] by A46,A50;
then G9 /\ y = {f.y};
then
A52: x in {f.y} by A51,TARSKI:def 1;
f.y in rng f by A46,A50,FUNCT_1:3;
hence u in rng f by A48,A52,TARSKI:def 1;
end;
now
let u be object;
assume u in rng f;
then consider s being object such that
A53: s in dom f & u = f.s by FUNCT_1:def 3;
P[s,f.s] by A46,A53;
hence u in G by A53;
end;
then
A54: rng f = G by A47,TARSKI:2;
consider y being object such that
A55: G9 /\ xx = {y} by A28;
y in G9 /\ xx by A55,TARSKI:def 1;
then y in G9 by XBOOLE_0:def 4;
then y in G by A55;
then G is non empty finite by A29,A46,A54,FINSET_1:8;
then reconsider G as non empty finite Subset of Polynom-Ring(n,L);
for b being bag of n st b in HT(I,T) ex b9 being bag of n st b9 in
HT(G,T) & b9 divides b
proof
let b be bag of n;
reconsider bb = b as Element of R by PRE_POLY:def 12;
assume b in HT(I,T);
then consider bb9 being Element of R such that
A56: bb9 in S and
A57: bb9 <= bb by A15,DICKSON:def 9;
set N = {p where p is Polynomial of n,L : p in I & HT(p,T) = bb9 & p <>
0_(n,L)};
A58: N in M by A56;
then consider y being object such that
A59: G9 /\ N = {y} by A28;
reconsider b9 = bb9 as bag of n;
take b9;
A60: [bb9,bb] in DivOrder(n) by A57,ORDERS_2:def 5;
A61: y in (G9 /\ N) by A59,TARSKI:def 1;
then reconsider y as Element of G9 by XBOOLE_0:def 4;
y in N by A61,XBOOLE_0:def 4;
then
A62: ex r being Polynomial of n,L st y = r & r in I & HT(r,T ) = bb9 & r
<> 0_(n,L);
y in G by A58,A59;
hence thesis by A60,A62,Def5;
end;
then
A63: HT(I,T) c= multiples(HT(G,T)) by Th28;
take G;
now
let u be object;
assume u in G;
then consider x being Element of G9 such that
A64: u = x and
A65: ex y being set st y in M & G9 /\ y = {x};
consider y being set such that
A66: y in M and
A67: G9 /\ y = {x} by A65;
consider s being Element of Bags n such that
A68: y = {p where p is Polynomial of n,L : p in I & HT(p,T) = s & p
<> 0_(n,L)} and
s in S by A66;
x in (G9 /\ y) by A67,TARSKI:def 1;
then x in y by XBOOLE_0:def 4;
then ex q being Polynomial of n,L st x = q & q in I & HT(q,T ) = s & q
<> 0_(n,L) by A68;
hence u in I by A64;
end;
then G c= I;
hence thesis by A63,Th29;
end;
end;
Lm9: for L being add-associative left_zeroed right_zeroed right_complementable
associative distributive well-unital non empty doubleLoopStr, A,B being non
empty Subset of L st B = A \ {0.L} for f being LinearCombination of A, u being
set st u = Sum f holds ex g being LinearCombination of B st u = Sum g
proof
let L be add-associative left_zeroed right_zeroed right_complementable
associative distributive well-unital non empty doubleLoopStr, A,B be non
empty Subset of L;
defpred P[Nat] means for f being LinearCombination of A st len f
= $1 for u being set st u = Sum f holds ex g being LinearCombination of B st u
= Sum g;
assume
A1: B = A\{0.L};
A2: now
let k be Nat;
assume
A3: P[k];
for f being LinearCombination of A st len f = k+1 for u being set st
u = Sum f holds ex g being LinearCombination of B st u = Sum g
proof
let f be LinearCombination of A;
set g = f|(Seg k);
reconsider g as FinSequence by FINSEQ_1:15;
A4: rng f c= the carrier of L by FINSEQ_1:def 4;
set h = f/.(len f);
assume
A5: len f = k+1;
then 1 <= len f by NAT_1:12;
then len f in Seg(len f) by FINSEQ_1:1;
then
A6: len f in dom f by FINSEQ_1:def 3;
then
A7: h = f.(len f) by PARTFUN1:def 6;
A8: k <= k + 1 by NAT_1:12;
then
A9: len g = k by A5,FINSEQ_1:17;
A10: dom g = Seg k by A5,A8,FINSEQ_1:17;
A11: dom f = Seg(k+1) by A5,FINSEQ_1:def 3;
then
A12: dom g c= dom f by A8,A10,FINSEQ_1:5;
now
let u be object;
assume u in rng g;
then consider x being object such that
A13: x in dom g and
A14: u = g.x by FUNCT_1:def 3;
g.x = f.x by A13,FUNCT_1:47;
then u in rng f by A12,A13,A14,FUNCT_1:def 3;
hence u in the carrier of L by A4;
end;
then rng g c= the carrier of L;
then reconsider g as FinSequence of the carrier of L by FINSEQ_1:def 4;
for i being set st i in dom g ex u,v being Element of L,a being
Element of A st g/.i = u*a*v
proof
let i be set;
assume
A15: i in dom g;
then reconsider i as Element of NAT;
i <= k by A10,A15,FINSEQ_1:1;
then
A16: i <= k + 1 by NAT_1:12;
1 <= i by A10,A15,FINSEQ_1:1;
then
A17: i in dom f by A11,A16,FINSEQ_1:1;
g/.i = g.i by A15,PARTFUN1:def 6
.= f.i by A15,FUNCT_1:47
.= f/.i by A17,PARTFUN1:def 6;
hence thesis by A17,IDEAL_1:def 8;
end;
then reconsider g as LinearCombination of A by IDEAL_1:def 8;
consider g9 being LinearCombination of B such that
A18: Sum g = Sum g9 by A3,A9;
let u be set;
assume
A19: u = Sum f;
A20: len f = len g + 1 by A5,A8,FINSEQ_1:17;
then
A21: Sum f = Sum(g) + h by A10,A7,RLVECT_1:38;
now
per cases;
case
h = 0.L;
hence Sum f = Sum g by A21,RLVECT_1:def 4;
end;
case
A22: h <> 0.L;
set l = g9^<*h*>;
for i being set st i in dom l ex u,v being Element of L,a being
Element of B st l/.i = u*a*v
proof
let i be set;
assume
A23: i in dom l;
then reconsider i as Element of NAT;
A24: len l = len(g9) + len(<*h*>) by FINSEQ_1:22
.= len(g9) + 1 by FINSEQ_1:39;
now
per cases;
case
A25: i = len l;
consider u,v being Element of L,a being Element of A such that
A26: f/.(len f) = u*a*v by A6,IDEAL_1:def 8;
A27: now
assume not a in B;
then a in {0.L} by A1,XBOOLE_0:def 5;
then a = 0.L by TARSKI:def 1;
then u * a * v = 0.L * v
.= 0.L;
hence contradiction by A22,A26;
end;
l/.i = l.i by A23,PARTFUN1:def 6
.= h by A24,A25,FINSEQ_1:42;
hence thesis by A26,A27;
end;
case
A28: i <> len l;
A29: i in Seg(len l) by A23,FINSEQ_1:def 3;
then i <= len l by FINSEQ_1:1;
then i < len l by A28,XXREAL_0:1;
then
A30: i <= len(g9) by A24,NAT_1:13;
1 <= i by A29,FINSEQ_1:1;
then i in Seg(len(g9)) by A30,FINSEQ_1:1;
then
A31: i in dom(g9) by FINSEQ_1:def 3;
l/.i = l.i by A23,PARTFUN1:def 6
.= (g9).i by A31,FINSEQ_1:def 7
.= (g9)/.i by A31,PARTFUN1:def 6;
hence thesis by A31,IDEAL_1:def 8;
end;
end;
hence thesis;
end;
then reconsider l as LinearCombination of B by IDEAL_1:def 8;
Sum l = Sum(g9) + Sum(<*h*>) by RLVECT_1:41
.= Sum f by A10,A18,A7,A20,RLVECT_1:38,44;
hence thesis by A19;
end;
end;
hence thesis by A19,A18;
end;
hence P[k+1];
end;
let f be LinearCombination of A, u be set;
assume
A32: u = Sum f;
A33: ex n being Element of NAT st len f = n;
A34: P[ 0 ]
proof
set g = <*>the carrier of L;
reconsider g as FinSequence of the carrier of L;
for i being set st i in dom g ex u,v being Element of L,a being
Element of B st g/.i = u*a*v;
then reconsider g as LinearCombination of B by IDEAL_1:def 8;
let f be LinearCombination of A;
A35: g = <*>(the carrier of L);
assume len f = 0;
then
A36: f = <*>(the carrier of L);
let u be set;
assume u = Sum f;
hence thesis by A36,A35;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A34,A2);
hence thesis by A32,A33;
end;
theorem
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, I being add-closed left-ideal non empty
Subset of Polynom-Ring(n,L) st I <> {0_(n,L)} ex G being finite Subset of
Polynom-Ring(n,L) st G is_Groebner_basis_of I,T & not(0_(n,L) in G)
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of
Polynom-Ring(n,L);
assume
A1: I <> {0_(n,L)};
A2: 0_(n,L) = 0.Polynom-Ring(n,L) by POLYNOM1:def 11;
consider G being finite Subset of Polynom-Ring(n,L) such that
A3: G is_Groebner_basis_of I,T by Th35;
set R = PolyRedRel(G,T);
A4: G-Ideal = I by A3;
A5: PolyRedRel(G,T) is locally-confluent by A3;
set G9 = G \ {0_(n,L)}, R9 = PolyRedRel(G9,T);
reconsider G9 as finite Subset of Polynom-Ring(n,L);
A6: now
per cases;
case
A7: G9 = {};
now
per cases;
case
G = {};
hence G9-Ideal = I by A3;
end;
case
A8: G <> {};
A9: now
let u be object;
assume u in {0_(n,L)};
then
A10: u = 0_(n,L) by TARSKI:def 1;
A11: G c= {0_(n,L)} by A7,XBOOLE_1:37;
now
assume not u in G;
then for v being object holds not v in G by A10,A11,TARSKI:def 1;
hence G = {} by XBOOLE_0:def 1;
end;
hence u in G by A8;
end;
A12: 0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 11;
now
let u be object;
assume
A13: u in G;
G c= {0_(n,L)} by A7,XBOOLE_1:37;
hence u in {0_(n,L)} by A13;
end;
then G = {0_(n,L)} by A9,TARSKI:2;
hence G9-Ideal = I by A1,A4,A12,IDEAL_1:44;
end;
end;
hence G9-Ideal = I;
end;
case
G9 <> {};
then reconsider
GG = G,GG9 = G9 as non empty Subset of Polynom-Ring(n,L);
A14: 0.(Polynom-Ring(n,L)) = 0_(n,L) by POLYNOM1:def 11;
A15: now
let u be object;
assume u in G-Ideal;
then ex f being LinearCombination of GG st u = Sum f by IDEAL_1:60;
then ex g being LinearCombination of GG9 st u = Sum g by A14,Lm9;
hence u in G9-Ideal by IDEAL_1:60;
end;
now
let u be object;
A16: GG9-Ideal c= GG-Ideal by IDEAL_1:57,XBOOLE_1:36;
assume u in G9-Ideal;
hence u in G-Ideal by A16;
end;
hence G9-Ideal = I by A4,A15,TARSKI:2;
end;
end;
A17: now
assume 0_(n,L) in G9;
then not(0_(n,L)) in {0_(n,L)} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A18: for u being object holds u in R implies u in R9
proof
let u be object;
assume
A19: u in R;
then consider p,q being object such that
A20: p in NonZero Polynom-Ring(n,L) and
A21: q in the carrier of Polynom-Ring(n,L) and
A22: u = [p,q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A21,POLYNOM1:def 11;
not p in {0_(n,L)} by A2,A20,XBOOLE_0:def 5;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L by A20,POLYNOM1:def 11
,POLYNOM7:def 1;
p reduces_to q,G,T by A19,A22,POLYRED:def 13;
then consider f being Polynomial of n,L such that
A23: f in G and
A24: p reduces_to q,f,T by POLYRED:def 7;
ex b being bag of n st p reduces_to q,f,b,T by A24,POLYRED:def 6;
then f <> 0_(n,L) by POLYRED:def 5;
then not f in {0_(n,L)} by TARSKI:def 1;
then f in G9 by A23,XBOOLE_0:def 5;
then p reduces_to q,G9,T by A24,POLYRED:def 7;
hence thesis by A22,POLYRED:def 13;
end;
R9 c= R by Th4,XBOOLE_1:36;
then for u being object holds u in R9 implies u in R;
then R9 is locally-confluent by A5,A18,TARSKI:2;
then G9 is_Groebner_basis_of I,T by A6;
hence thesis by A17;
end;
definition
let n be Ordinal, T be connected TermOrder of n, L be non empty
multLoopStr_0, p be Polynomial of n,L;
pred p is_monic_wrt T means
:Def6:
HC(p,T) = 1.L;
end;
definition :: definition 5.29, p. 203
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be
Subset of Polynom-Ring(n,L);
pred P is_reduced_wrt T means
for p being Polynomial of n,L st p in P
holds p is_monic_wrt T & p is_irreducible_wrt P\{p},T;
end;
notation :: definition 5.29, p. 203
let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be
Subset of Polynom-Ring(n,L);
synonym P is_autoreduced_wrt T for P is_reduced_wrt T;
end;
theorem Th37: :: lemma 5.42, p. 208
for n being Ordinal, T being admissible connected TermOrder of n
, L being add-associative right_complementable right_zeroed commutative
associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, I being add-closed left-ideal Subset of
Polynom-Ring(n,L), m being Monomial of n,L, f,g being Polynomial of n,L st f in
I & g in I & HM(f,T) = m & HM(g,T) = m holds not(ex p being Polynomial of n,L
st p in I & p < f,T & HM(p,T) = m) & not(ex p being Polynomial of n,L st p in I
& p < g,T & HM(p,T) = m) implies f = g
proof
let n be Ordinal, T be admissible connected TermOrder of n, L be
add-associative right_complementable right_zeroed commutative associative
well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, I be add-closed left-ideal Subset of Polynom-Ring(n,L), m
be Monomial of n,L, f,g be Polynomial of n,L;
assume that
A1: f in I and
A2: g in I and
A3: HM(f,T) = m and
A4: HM(g,T) = m;
A5: HT(f,T) = term(HM(f,T)) by TERMORD:22
.= HT(g,T) by A3,A4,TERMORD:22;
A6: HC(f,T) = f.(HT(f,T)) by TERMORD:def 7
.= (HM(f,T)).(HT(f,T)) by TERMORD:18
.= g.(HT(g,T)) by A3,A4,A5,TERMORD:18
.= HC(g,T) by TERMORD:def 7;
assume that
A7: not(ex p being Polynomial of n,L st p in I & p < f,T & HM(p,T) = m) and
A8: not(ex p being Polynomial of n,L st p in I & p < g,T & HM(p,T) = m);
reconsider I as LeftIdeal of Polynom-Ring(n,L) by A1;
per cases;
suppose
f - g = 0_(n,L);
hence g = (f - g) + g by POLYRED:2
.= (f + -g) + g by POLYNOM1:def 7
.= f + (-g + g) by POLYNOM1:21
.= f + 0_(n,L) by POLYRED:3
.= f by POLYNOM1:23;
end;
suppose
A9: f - g <> 0_(n,L);
now
per cases;
case
A10: f = 0_(n,L);
then HC(g,T) = 0.L by A6,TERMORD:17;
hence thesis by A10,TERMORD:17;
end;
case
A11: g = 0_(n,L);
then HC(f,T) = 0.L by A6,TERMORD:17;
hence thesis by A11,TERMORD:17;
end;
case
A12: f <> 0_(n,L) & g <> 0_(n,L);
set s = HT(f-g,T);
set d = f.s - g.s;
set c = f.s * d";
set h = f - c * (f - g);
A13: Support(f-g) <> {} by A9,POLYNOM7:1;
then
A14: HT(f-g,T) in Support(f-g) by TERMORD:def 6;
A15: now
assume HT(f-g,T) = HT(f,T);
then (f-g).HT(f-g,T) = (f+-g).HT(f,T) by POLYNOM1:def 7
.= f.HT(f,T) + (-g).HT(g,T) by A5,POLYNOM1:15
.= f.HT(f,T) + -(g.HT(g,T)) by POLYNOM1:17
.= HC(f,T) + -(g.HT(g,T)) by TERMORD:def 7
.= HC(f,T) + -HC(g,T) by TERMORD:def 7
.= 0.L by A6,RLVECT_1:5;
hence contradiction by A14,POLYNOM1:def 4;
end;
HT(f-g,T) <= max(HT(f,T),HT(f,T),T),T by A5,Th7;
then HT(f-g,T) <= HT(f,T),T by TERMORD:12;
then HT(f-g,T) < HT(f,T),T by A15,TERMORD:def 3;
then not HT(f,T) <= HT(f-g,T),T by TERMORD:5;
then not HT(f,T) in Support(f-g) by TERMORD:def 6;
then
A16: (f-g).(HT(f,T)) = 0.L by POLYNOM1:def 4;
A17: h.(HT(f,T)) = (f + (-(c * (f - g)))).(HT(f,T)) by POLYNOM1:def 7
.= f.HT(f,T) + (-(c * (f - g))).(HT(f,T)) by POLYNOM1:15
.= f.HT(f,T) + -((c * (f - g)).(HT(f,T))) by POLYNOM1:17
.= f.HT(f,T) + -(c * 0.L) by A16,POLYNOM7:def 9
.= f.HT(f,T) + -0.L
.= f.HT(f,T) + 0.L by RLVECT_1:12
.= f.HT(f,T) by RLVECT_1:def 4;
Support f <> {} by A12,POLYNOM7:1;
then HT(f,T) in Support(f) by TERMORD:def 6;
then h.(HT(f,T)) <> 0.L by A17,POLYNOM1:def 4;
then
A18: HT(f,T) in Support h by POLYNOM1:def 4;
then
A19: HT(f,T) <= HT(h,T),T by TERMORD:def 6;
Support h = Support(f + -(c * (f - g))) by POLYNOM1:def 7;
then Support h c= Support f \/ Support(-(c * (f - g))) by POLYNOM1:20;
then
A20: Support h c= Support f \/ Support(c * (f - g)) by Th5;
Support f \/ Support(c * (f - g)) c= Support f \/ Support(f - g)
by POLYRED:19,XBOOLE_1:9;
then
A21: Support h c= Support f \/ Support(f - g) by A20;
not g < f,T by A2,A4,A7;
then
A22: f <= g,T by POLYRED:29;
not f < g,T by A1,A3,A8;
then g <= f,T by POLYRED:29;
then
A23: Support f = Support g by A22,POLYRED:26;
Support(f-g) = Support(f + -g) & Support(f + -g) c= Support f \/
Support(-g) by POLYNOM1:20,def 7;
then
A24: Support(f-g) c= Support f \/ Support g by Th5;
then
A25: Support f \/ Support(f - g) c= Support f \/ Support f by A23,XBOOLE_1:9
;
then
A26: Support h c= Support f by A21;
HT(h,T) in Support h by A18,TERMORD:def 6;
then HT(h,T) <= HT(f,T),T by A26,TERMORD:def 6;
then
A27: HT(h,T) = HT(f,T) by A19,TERMORD:7;
then HC(h,T) = f.(HT(f,T)) by A17,TERMORD:def 7
.= HC(f,T) by TERMORD:def 7;
then
A28: HM(h,T) = Monom(HC(f,T),HT(f,T)) by A27,TERMORD:def 8
.= m by A3,TERMORD:def 8;
reconsider cp = c |(n,L) *' (f - g) as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider cc = c |(n,L) as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider f9 = f, g9 = g as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
A29: (f-g).s = (f+-g).s by POLYNOM1:def 7
.= f.s + (-g).s by POLYNOM1:15
.= f.s + -(g.s) by POLYNOM1:17
.= f.s - g.s;
A30: s in Support(f-g) by A13,TERMORD:def 6;
A31: now
A32: (f-g).s <> 0.L by A30,POLYNOM1:def 4;
A33: -c * (f.s - g.s) = -(f.s) * ((f.s - g.s)" * (f.s - g.s)) by
GROUP_1:def 3
.= -(f.s) * 1.L by A29,A32,VECTSP_1:def 10
.= -(f.s);
assume
A34: Support h = Support f;
h.s = (f + -(c * (f - g))).s by POLYNOM1:def 7
.= f.s + (-(c * (f - g))).s by POLYNOM1:15
.= f.s + ((-c) * (f - g)).s by POLYRED:9
.= f.s + (-c) * (f - g).s by POLYNOM7:def 9
.= f.s + -(f.s) by A29,A33,VECTSP_1:9
.= 0.L by RLVECT_1:5;
hence contradiction by A23,A14,A24,A34,POLYNOM1:def 4;
end;
h <= f,T by A21,A25,Th8,XBOOLE_1:1;
then
A35: h < f,T by A31,POLYRED:def 3;
reconsider cp as Element of Polynom-Ring(n,L);
reconsider cc as Element of Polynom-Ring(n,L);
reconsider f9,g9 as Element of Polynom-Ring(n,L);
f - g = f9 - g9 by Lm2;
then
A36: cp = cc * (f9 - g9) by POLYNOM1:def 11;
f9 - g9 in I by A1,A2,IDEAL_1:15;
then
A37: cc * (f9 - g9) in I by IDEAL_1:def 2;
f9 - cp = f - c |(n,L) *' (f - g) by Lm2
.= f - c * (f - g) by POLYNOM7:27;
hence contradiction by A1,A7,A28,A35,A37,A36,IDEAL_1:15;
end;
end;
hence thesis;
end;
end;
Lm10: for n being Element of NAT, T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, p being Polynomial of n,L, I being add-closed
left-ideal non empty Subset of Polynom-Ring(n,L) st p in I & p <> 0_(n,L) ex q
being Polynomial of n,L st q in I & HM(q,T) = Monom(1.L,HT(p,T)) & q <> 0_(n,L)
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, p be Polynomial of n,L, I be add-closed left-ideal
non empty Subset of Polynom-Ring(n,L);
assume that
A1: p in I and
A2: p <> 0_(n,L);
set c = (HC(p,T))";
A3: HC(p,T) <> 0.L by A2,TERMORD:17;
now
assume c = 0.L;
then 0.L = c * HC(p,T)
.= 1.L by A3,VECTSP_1:def 10;
hence contradiction;
end;
then reconsider c as non zero Element of L by STRUCT_0:def 12;
set q = c * p;
take q;
reconsider pp = p, cc = c |(n,L) as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider pp,cc as Element of Polynom-Ring(n,L);
q = c |(n,L) *' p by POLYNOM7:27
.= cc * pp by POLYNOM1:def 11;
hence q in I by A1,IDEAL_1:def 2;
A4: HT(q,T) = HT(p,T) by POLYRED:21;
then HC(q,T) = q.HT(p,T) by TERMORD:def 7
.= c * p.HT(p,T) by POLYNOM7:def 9
.= HC(p,T) * (HC(p,T))" by TERMORD:def 7
.= 1.L by A3,VECTSP_1:def 10;
hence HM(q,T) = Monom(1.L,HT(p,T)) by A4,TERMORD:def 8;
then 1.L = coefficient(HM(q,T)) by POLYNOM7:9
.= HC(q,T) by TERMORD:22;
then HC(q,T) <> 0.L;
hence thesis by TERMORD:17;
end;
theorem
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, I being add-closed left-ideal non empty
Subset of Polynom-Ring(n,L), G being Subset of Polynom-Ring(n,L), p being
Polynomial of n,L, q being non-zero Polynomial of n,L st p in G & q in G & p <>
q & HT(q,T) divides HT(p,T) holds G is_Groebner_basis_of I,T implies G\{p}
is_Groebner_basis_of I,T
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of
Polynom-Ring(n,L), G be Subset of Polynom-Ring(n,L), p be Polynomial of n,L, q
be non-zero Polynomial of n,L;
assume that
A1: p in G and
A2: q in G and
A3: p <> q and
A4: HT(q,T) divides HT(p,T);
reconsider GG = G as non empty Subset of Polynom-Ring(n,L) by A1;
assume
A5: G is_Groebner_basis_of I,T;
set G9 = G\{p};
A6: not q in {p} by A3,TARSKI:def 1;
then q <> 0_(n,L) & q in G9 by A2,POLYNOM7:def 1,XBOOLE_0:def 5;
then
A7: HT(q,T) in {HT(u,T) where u is Polynomial of n,L : u in G9 & u <> 0_(n,
L)};
GG c= GG-Ideal by IDEAL_1:def 14;
then
A8: G c= I by A5;
for f being Polynomial of n,L st f in I holds PolyRedRel(G,T) reduces f,
0_(n,L) by A1,A5,Th24;
then for f being non-zero Polynomial of n,L st f in I holds f
is_reducible_wrt G,T by Th25;
then
A9: for f being non-zero Polynomial of n,L st f in I holds f
is_top_reducible_wrt G,T by A8,Th26;
for b being bag of n st b in HT(I,T) ex b9 being bag of n st b9 in HT(
G9,T) & b9 divides b
proof
let b be bag of n;
assume b in HT(I,T);
then consider bb being bag of n such that
A10: bb in HT(G,T) and
A11: bb divides b by A9,Th27;
consider r being Polynomial of n,L such that
A12: bb = HT(r,T) and
A13: r in G and
A14: r <> 0_(n,L) by A10;
now
per cases;
case
r = p;
hence thesis by A4,A7,A11,A12,Lm8;
end;
case
r <> p;
then not r in {p} by TARSKI:def 1;
then r in G9 by A13,XBOOLE_0:def 5;
then
bb in {HT(u,T) where u is Polynomial of n,L : u in G9 & u <> 0_(n
,L)} by A12,A14;
hence thesis by A11;
end;
end;
hence thesis;
end;
then
A15: HT(I,T) c= multiples(HT(G9,T)) by Th28;
G9 c= G by XBOOLE_1:36;
then
A16: G9 c= I by A8;
G9 <> {} by A2,A6,XBOOLE_0:def 5;
hence thesis by A16,A15,Th29;
end;
theorem :: theorem 5.43, p. 209
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, I being add-closed left-ideal non empty
Subset of Polynom-Ring(n,L) st I <> {0_ (n,L)} ex G being finite Subset of
Polynom-Ring(n,L) st G is_Groebner_basis_of I,T & G is_reduced_wrt T
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of
Polynom-Ring(n,L);
set R = RelStr(#Bags n, DivOrder n#);
assume
A1: I <> {0_ (n,L)};
ex q being Element of I st q <> 0_(n,L)
proof
assume
A2: not(ex q being Element of I st q <> 0_(n,L));
A3: now
let u be object;
assume u in {0_(n,L)};
then
A4: u = 0_(n,L) by TARSKI:def 1;
now
assume not u in I;
then for v being object holds not v in I by A2,A4;
hence thesis by XBOOLE_0:def 1;
end;
hence u in I;
end;
now
let u be object;
assume u in I;
then u = 0_(n,L) by A2;
hence u in {0_(n,L)} by TARSKI:def 1;
end;
hence thesis by A1,A3,TARSKI:2;
end;
then consider q being Element of I such that
A5: q <> 0_(n,L);
reconsider q as Polynomial of n,L by POLYNOM1:def 11;
HT(q,T) in {HT(p,T) where p is Polynomial of n,L : p in I & p <> 0_(n,L
)} by A5;
then reconsider hti = HT(I,T) as non empty Subset of R;
set hq = HT(q,T);
consider S being set such that
A6: S is_Dickson-basis_of hti,R and
A7: for C being set st C is_Dickson-basis_of hti,R holds S c= C by DICKSON:34;
reconsider hq as Element of R;
A8: now
A9: ex B being set st B is_Dickson-basis_of hti,R & B is finite by
DICKSON:def 10;
assume S is non finite;
hence contradiction by A7,A9,FINSET_1:1;
end;
A10: S c= hti by A6,DICKSON:def 9;
now
let u be object;
assume u in S;
then u in hti by A10;
hence u in Bags n;
end;
then reconsider S as finite Subset of Bags n by A8,TARSKI:def 3;
set M = {{p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,s) &
p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T & q <> 0_(n
,L) & HM(q,T) = Monom(1.L,s))} where s is Element of Bags n : s in S};
set s = the Element of S;
hq in {HT(p,T) where p is Polynomial of n,L : p in I & p <> 0_(n,L) } by A5;
then
A11: ex b being Element of R st b in S & b <= hq by A6,DICKSON:def 9;
then s in S;
then reconsider s as Element of Bags n;
{p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,s) & p
<> 0_(n,L) & not(ex r being Polynomial of n,L st r in I & r < p,T & r <> 0_(n,L
) & HM(r,T) = Monom(1.L,s))} in M by A11;
then reconsider M as non empty set;
set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r
} };
A12: for x being set st x in M ex q being Polynomial of n,L st q in I & x =
{q} & q <> 0_(n,L)
proof
let x be set;
assume x in M;
then consider s being Element of Bags n such that
A13: x = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.
L,s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T & q
<> 0_(n,L) & HM(q,T) = Monom(1.L,s))} and
A14: s in S;
s in hti by A10,A14;
then consider q being Polynomial of n,L such that
A15: s = HT(q,T) and
A16: q in I & q <> 0_(n,L);
consider qq being Polynomial of n,L such that
A17: qq in I & HM(qq,T) = Monom(1.L,HT(q,T)) & qq <> 0_(n,L) by A16,Lm10;
set M9 = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,s)
& p <> 0_(n,L)};
A18: now
let u be object;
assume u in M9;
then ex pp being Polynomial of n,L st u = pp & pp in I & HM( pp,T) =
Monom(1.L,s) & pp <> 0_(n,L);
hence u in the carrier of Polynom-Ring(n,L);
end;
qq in M9 by A15,A17;
then reconsider M9 as non empty Subset of Polynom-Ring(n,L) by A18,
TARSKI:def 3;
reconsider M9 as non empty Subset of Polynom-Ring(n,L);
consider p being Polynomial of n,L such that
A19: p in M9 and
A20: for r being Polynomial of n,L st r in M9 holds p <= r,T by POLYRED:31;
consider p9 being Polynomial of n,L such that
A21: p9 = p and
A22: p9 in I and
A23: HM(p9,T) = Monom(1.L,s) and
A24: p9 <> 0_(n,L) by A19;
A25: now
assume ex q being Polynomial of n,L st q in I & q < p9,T & q <> 0_(n,L
) & HM(q,T) = Monom(1.L,s);
then consider q being Polynomial of n,L such that
A26: q in I and
A27: q < p9,T and
A28: q <> 0_(n,L) & HM(q,T) = Monom(1.L,s);
q in M9 by A26,A28;
then p <= q,T by A20;
hence contradiction by A21,A27,POLYRED:29;
end;
A29: now
A30: 1.L <> 0.L;
assume ex q being Polynomial of n,L st q in I & q < p9,T & HM(q,T) =
Monom(1.L,s);
then consider q being Polynomial of n,L such that
A31: q in I & q < p9,T and
A32: HM(q,T) = Monom(1.L,s);
HC(q,T) = coefficient(Monom(1.L,s)) by A32,TERMORD:22
.= 1.L by POLYNOM7:9;
then q <> 0_(n,L) by A30,TERMORD:17;
hence contradiction by A25,A31,A32;
end;
A33: now
let u be object;
assume u in x;
then consider u9 being Polynomial of n,L such that
A34: u9 = u and
A35: u9 in I & HM(u9,T) = Monom(1.L,s) and
u9 <> 0_(n,L) and
A36: not(ex q being Polynomial of n,L st q in I & q < u9,T & q <> 0_
(n,L ) & HM(q,T) = Monom(1.L,s)) by A13;
now
A37: 1.L <> 0.L;
assume ex q being Polynomial of n,L st q in I & q < u9,T & HM(q,T) =
Monom(1.L,s);
then consider q being Polynomial of n,L such that
A38: q in I & q < u9,T and
A39: HM(q,T) = Monom(1.L,s);
HC(q,T) = coefficient(Monom(1.L,s)) by A39,TERMORD:22
.= 1.L by POLYNOM7:9;
then q <> 0_(n,L) by A37,TERMORD:17;
hence contradiction by A36,A38,A39;
end;
then u9 = p9 by A22,A23,A29,A35,Th37;
hence u in {p9} by A34,TARSKI:def 1;
end;
take p9;
p9 in x by A13,A22,A23,A24,A25;
then for u being object holds u in {p9} implies u in x by TARSKI:def 1;
hence thesis by A22,A24,A33,TARSKI:2;
end;
now
let u be object;
assume u in G;
then consider r being Polynomial of n,L such that
A40: u = r and
A41: ex x being Element of M st x = {r};
consider x being Element of M such that
A42: x = {r} by A41;
consider r9 being Polynomial of n,L such that
A43: r9 in I and
A44: x = {r9} and
r9 <> 0_(n,L) by A12;
r9 in {r} by A42,A44,TARSKI:def 1;
hence u in I by A40,A43,TARSKI:def 1;
end;
then
A45: G c= I;
A46: M is finite
proof
defpred P[object,object] means
$2 = {p where p is Polynomial of n,L : ex b being
bag of n st b = $1 & p in I & HM(p,T) = Monom(1.L,b) & p <> 0_(n,L) & not(ex q
being Polynomial of n,L st q in I & q < p,T & q <> 0_(n,L) & HM(q,T) = Monom(1.
L,b))};
A47: for x being object st x in S ex y being object st P[x,y];
consider f being Function such that
A48: dom f = S & for x being object st x in S holds P[x,f.x] from
CLASSES1:sch 1(A47);
A49: now
let u be object;
assume u in rng f;
then consider s being object such that
A50: s in dom f and
A51: u = f.s by FUNCT_1:def 3;
reconsider s as Element of Bags n by A48,A50;
set V = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,s
) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T & q <>
0_(n,L) & HM(q,T) = Monom(1.L,s))};
A52: ex b being bag of n st f.s = {p where p is Polynomial of n,L : ex b
being bag of n st b = s & p in I & HM(p,T) = Monom(1.L,b) & p <> 0_( n,L) & not
(ex q being Polynomial of n,L st q in I & q < p,T & q <> 0_(n,L) & HM (q,T) =
Monom(1.L,b))} by A48,A50;
A53: now
let v be object;
assume v in V;
then
ex p being Polynomial of n,L st v = p & p in I & HM(p,T ) = Monom(
1.L,s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T &
q <> 0_(n,L) & HM(q,T) = Monom(1.L,s));
hence v in f.s by A52;
end;
now
let v be object;
assume v in f.s;
then
ex p being Polynomial of n,L st v = p & ex b being bag of n st b =
s & p in I & HM(p,T) = Monom(1.L,b) & p <> 0_(n,L) & not(ex q being Polynomial
of n,L st q in I & q < p,T & q <> 0_(n,L ) & HM(q,T) = Monom(1.L,b)) by A52;
hence v in V;
end;
then
u = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,
s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T & q <>
0_(n,L) & HM(q,T) = Monom(1.L,s))} by A51,A53,TARSKI:2;
hence u in M by A48,A50;
end;
now
let u be object;
reconsider uu=u as set by TARSKI:1;
assume u in M;
then consider s being Element of Bags n such that
A54: u = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(
1.L,s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T &
q <> 0_(n,L) & HM(q,T) = Monom(1.L,s))} and
A55: s in S;
A56: ex b being bag of n st f.s = {p where p is Polynomial of n,L : ex b
being bag of n st b = s & p in I & HM(p,T) = Monom(1.L,b) & p <> 0_( n,L) & not
(ex q being Polynomial of n,L st q in I & q < p,T & q <> 0_(n,L) & HM (q,T) =
Monom(1.L,b))} by A48,A55;
A57: now
let v be object;
assume v in uu;
then
ex p being Polynomial of n,L st v = p & p in I & HM(p,T ) = Monom(
1.L,s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T &
q <> 0_(n,L) & HM(q,T) = Monom(1.L,s)) by A54;
hence v in f.s by A56;
end;
A58: now
let v be object;
assume v in f.s;
then
ex p being Polynomial of n,L st v = p & ex b being bag of n st b =
s & p in I & HM(p,T) = Monom(1.L,b) & p <> 0_(n,L) & not(ex q being Polynomial
of n,L st q in I & q < p,T & q <> 0_(n,L ) & HM(q,T) = Monom(1.L,b)) by A56;
hence v in uu by A54;
end;
f.s in rng f by A48,A55,FUNCT_1:3;
hence u in rng f by A57,A58,TARSKI:2;
end;
then rng f = M by A49,TARSKI:2;
hence thesis by A48,FINSET_1:8;
end;
A59: G is finite
proof
defpred P[object,object] means
ex p being Polynomial of n,L, x being Element of
M st $1 = x & $2 = p & x = {p};
A60: for x being object st x in M ex y being object st P[x,y]
proof
let x be object;
assume
A61: x in M;
then reconsider x9 = x as Element of M;
consider q being Polynomial of n,L such that
q in I and
A62: x = {q} and
q <> 0_(n,L) by A12,A61;
take q;
take q,x9;
thus x = x9;
thus q = q;
thus thesis by A62;
end;
consider f being Function such that
A63: dom f = M & for x being object st x in M holds P[x,f.x] from
CLASSES1:sch 1(A60);
A64: now
let u be object;
assume u in G;
then consider r being Polynomial of n,L such that
A65: u = r and
A66: ex x being Element of M st x = {r};
consider x being Element of M such that
A67: x = {r} by A66;
P[x,f.x] by A63;
then consider
p9 being Polynomial of n,L, x9 being Element of M such that
x9 = x and
A68: p9 = f.x and
A69: x = {p9};
A70: f.x in rng f by A63,FUNCT_1:3;
p9 in {r} by A67,A69,TARSKI:def 1;
hence u in rng f by A65,A70,A68,TARSKI:def 1;
end;
now
let u be object;
assume u in rng f;
then consider s being object such that
A71: s in dom f and
A72: u = f.s by FUNCT_1:def 3;
reconsider s as Element of M by A63,A71;
ex p9 being Polynomial of n,L, x9 being Element of M st x9 = s & p9
= f.s & x9 = {p9} by A63;
hence u in G by A72;
end;
then rng f = G by A64,TARSKI:2;
hence thesis by A46,A63,FINSET_1:8;
end;
now
let u be object;
assume u in G;
then ex r being Polynomial of n,L st u = r & ex x being Element of M st x
= {r};
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
end;
then reconsider G as Subset of Polynom-Ring(n,L) by TARSKI:def 3;
G <> {}
proof
set z = the Element of M;
consider r being Polynomial of n,L such that
r in I and
A73: z = {r} and
r <> 0_(n,L) by A12;
r in G by A73;
hence thesis;
end;
then reconsider G as non empty finite Subset of Polynom-Ring(n,L) by A59;
take G;
for b being bag of n st b in HT(I,T) ex b9 being bag of n st b9 in HT(
G,T) & b9 divides b
proof
let b be bag of n;
reconsider bb = b as Element of R by PRE_POLY:def 12;
assume b in HT(I,T);
then consider bb9 being Element of R such that
A74: bb9 in S and
A75: bb9 <= bb by A6,DICKSON:def 9;
A76: [bb9,bb] in DivOrder(n) by A75,ORDERS_2:def 5;
reconsider b9 = bb9 as bag of n;
set N = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(1.L,b9)
& p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T & q <> 0_
(n,L) & HM(q,T) = Monom(1.L,b9))};
N in M by A74;
then reconsider N as Element of M;
take b9;
consider r being Polynomial of n,L such that
r in I and
A77: N = {r} and
r <> 0_(n,L) by A12;
r in N by A77,TARSKI:def 1;
then consider r9 being Polynomial of n,L such that
A78: r = r9 and
r9 in I and
A79: HM(r9,T) = Monom(1.L,b9) and
A80: r9 <> 0_(n,L) and
not(ex q being Polynomial of n,L st q in I & q < r9,T & q <> 0_(n, L)
& HM(q,T) = Monom(1.L,b9));
A81: r9 in G by A77,A78;
b9 = term(HM(r9,T)) by A79,POLYNOM7:10
.= HT(r9,T) by TERMORD:22;
hence thesis by A76,A80,A81,Def5;
end;
then HT(I,T) c= multiples(HT(G,T)) by Th28;
hence G is_Groebner_basis_of I,T by A45,Th29;
now
let q be Polynomial of n,L;
assume
A82: q in G;
then consider rr being Polynomial of n,L such that
A83: q = rr and
A84: ex x being Element of M st x = {rr};
consider x being Element of M such that
A85: x = {rr} by A84;
x in M;
then consider s being Element of Bags n such that
A86: x = {p where p is Polynomial of n,L : p in I & HM(p,T) = Monom(
1.L,s) & p <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q < p,T &
q <> 0_ (n,L) & HM(q,T) = Monom(1.L,s))} and
A87: s in S;
rr in x by A85,TARSKI:def 1;
then consider p being Polynomial of n,L such that
A88: rr = p and
p in I and
A89: HM(p,T) = Monom(1.L,s) and
p <> 0_(n,L) and
A90: not(ex q being Polynomial of n,L st q in I & q < p,T & q <> 0_(n
,L ) & HM(q,T) = Monom(1.L,s)) by A86;
A91: 1.L = coefficient(HM(rr,T)) by A88,A89,POLYNOM7:9
.= HC(rr,T) by TERMORD:22;
hence q is_monic_wrt T by A83;
A92: s = term(HM(rr,T)) by A88,A89,POLYNOM7:10
.= HT(q,T) by A83,TERMORD:22;
now
reconsider htq = HT(q,T) as Element of R;
assume q is_reducible_wrt G\{q},T;
then consider pp being Polynomial of n,L such that
A93: q reduces_to pp,G\{q},T by POLYRED:def 9;
consider g being Polynomial of n,L such that
A94: g in G\{q} and
A95: q reduces_to pp,g,T by A93,POLYRED:def 7;
A96: g in G by A94,XBOOLE_0:def 5;
A97: not g in {q} by A94,XBOOLE_0:def 5;
reconsider htg = HT(g,T) as Element of R;
consider b being bag of n such that
A98: q reduces_to pp,g,b,T by A95,POLYRED:def 6;
A99: b in Support q by A98,POLYRED:def 5;
A100: ex s being bag of n st s + HT(g,T) = b & pp = q - (q.b/HC(g,T)) *
(s *' g) by A98,POLYRED:def 5;
now
per cases;
case
A101: b = HT(q,T);
set S9 = S \ {htq};
consider z being Polynomial of n,L such that
A102: g = z and
A103: ex x being Element of M st x = {z} by A96;
consider x1 being Element of M such that
A104: x1 = {z} by A103;
x1 in M;
then consider t being Element of Bags n such that
A105: x1 = {u where u is Polynomial of n,L : u in I & HM(u,T) =
Monom(1.L,t) & u <> 0_(n,L) & not(ex q being Polynomial of n,L st q in I & q <
u,T & q <> 0_ (n,L) & HM(q,T) = Monom(1.L,t))} and
A106: t in S;
z in x1 by A104,TARSKI:def 1;
then consider p1 being Polynomial of n,L such that
A107: z = p1 and
p1 in I and
A108: HM(p1,T) = Monom(1.L,t) and
p1 <> 0_(n,L) and
not(ex q being Polynomial of n,L st q in I & q < p1,T & q <> 0_(
n, L) & HM(q,T) = Monom(1.L,t)) by A105;
A109: t = term(HM(p1,T)) by A108,POLYNOM7:10
.= htg by A102,A107,TERMORD:22;
now
assume htg in {htq};
then t = s by A92,A109,TARSKI:def 1;
hence contradiction by A83,A85,A86,A97,A102,A104,A105,TARSKI:def 1;
end;
then
A110: htg in S9 by A106,A109,XBOOLE_0:def 5;
HT(g,T) divides HT(q,T) by A100,A101,PRE_POLY:50;
then [htg,htq] in DivOrder(n) by Def5;
then
A111: htg <= htq by ORDERS_2:def 5;
A112: now
let a be Element of R;
assume a in hti;
then consider b being Element of R such that
A113: b in S and
A114: b <= a by A6,DICKSON:def 9;
now
per cases;
case
b in S9;
hence ex b being Element of R st b in S9 & b <= a by A114;
end;
case
not b in S9;
then b in {htq} by A113,XBOOLE_0:def 5;
then htg <= b by A111,TARSKI:def 1;
hence ex b being Element of R st b in S9 & b <= a by A110,A114,
ORDERS_2:3;
end;
end;
hence ex b being Element of R st b in S9 & b <= a;
end;
A115: now
assume htq in S9;
then not htq in {htq} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
S9 c= S by XBOOLE_1:36;
then S9 c= hti by A10;
then S9 is_Dickson-basis_of hti,R by A112,DICKSON:def 9;
then S c= S9 by A7;
hence q is_irreducible_wrt G\{q},T by A87,A92,A115;
end;
case
A116: b <> HT(q,T);
b <= HT(q,T),T by A99,TERMORD:def 6;
then b < HT(q,T),T by A116,TERMORD:def 3;
then
A117: pp.HT(q,T) = q.HT(q,T) by A98,POLYRED:41
.= 1.L by A83,A91,TERMORD:def 7;
1.L <> 0.L;
then
A118: HT(q,T) in Support pp by A117,POLYNOM1:def 4;
now
A119: b <= HT(q,T),T by A99,TERMORD:def 6;
assume
A120: HT(q,T) < HT(pp,T),T;
then HT(q,T) <= HT(pp,T),T by TERMORD:def 3;
then b <= HT(pp,T),T & b <> HT(pp,T) by A116,A119,TERMORD:7,8;
then b < HT(pp,T),T by TERMORD:def 3;
then HT(pp,T) in Support q iff HT(pp,T) in Support pp by A98,
POLYRED:40;
then HT(pp,T) <= HT(q,T),T by A118,TERMORD:def 6;
hence contradiction by A120,TERMORD:5;
end;
then
A121: HT(pp,T) <= HT(q,T),T by TERMORD:5;
HT(q,T) <= HT(pp,T),T by A118,TERMORD:def 6;
then HT(pp,T) = HT(q,T) by A121,TERMORD:7;
then Monom(HC(pp,T),HT(pp,T)) = Monom(1.L,s) by A92,A117,
TERMORD:def 7;
then
A122: HM(pp,T) = HM(q,T) by A83,A88,A89,TERMORD:def 8;
A123: now
assume pp = 0_(n,L);
then 0.L = HC(pp,T) by TERMORD:17
.= coefficient(HM(pp,T)) by TERMORD:22
.= 1.L by A83,A91,A122,TERMORD:22;
hence contradiction;
end;
consider m being Monomial of n,L such that
A124: pp = q - m *' g by A95,Th1;
reconsider gg = g, qq = q, mm = m as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider gg,qq,mm as Element of Polynom-Ring(n,L);
g in G by A94,XBOOLE_0:def 5;
then mm * gg in I by A45,IDEAL_1:def 2;
then -(mm * gg) in I by IDEAL_1:13;
then
A125: qq + -(mm * gg) in I by A45,A82,IDEAL_1:def 1;
mm * gg = m *' g by POLYNOM1:def 11;
then q - (m *' g) = qq - (mm * gg) by Lm2;
then pp in I by A124,A125;
hence contradiction by A83,A88,A89,A90,A95,A122,A123,POLYRED:43;
end;
end;
hence q is_irreducible_wrt G\{q},T;
end;
hence q is_irreducible_wrt G\{q},T;
end;
hence thesis;
end;
theorem :: theorem 5.43, p. 209
for n being Element of NAT, T being connected admissible TermOrder of
n, L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, I being add-closed left-ideal non empty
Subset of Polynom-Ring(n,L), G1,G2 being non empty finite Subset of
Polynom-Ring(n,L) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2
is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds G1 = G2
proof
let n be Element of NAT, T be connected admissible TermOrder of n, L be
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of
Polynom-Ring(n,L), G,H be finite non empty Subset of Polynom-Ring(n,L);
assume that
A1: G is_Groebner_basis_of I,T and
A2: G is_reduced_wrt T and
A3: H is_Groebner_basis_of I,T and
A4: H is_reduced_wrt T;
A5: H-Ideal = I by A3;
set GH = (G \/ H) \ (G /\ H);
assume
A6: G <> H;
now
assume GH = {};
then
A7: (G \/ H) c= (G /\ H) by XBOOLE_1:37;
A8: now
let u be object;
assume u in H;
then u in G \/ H by XBOOLE_0:def 3;
hence u in G by A7,XBOOLE_0:def 4;
end;
now
let u be object;
assume u in G;
then u in G \/ H by XBOOLE_0:def 3;
hence u in H by A7,XBOOLE_0:def 4;
end;
hence contradiction by A6,A8,TARSKI:2;
end;
then reconsider GH as non empty Subset of Polynom-Ring(n,L);
A9: now
let u be object;
assume
A10: u in GH;
then
A11: not u in G /\ H by XBOOLE_0:def 5;
A12: u in G \/ H by A10,XBOOLE_0:def 5;
u in G \ H or u in H \ G
proof
assume
A13: not u in G \ H;
now
per cases by A13,XBOOLE_0:def 5;
case
not u in G;
hence not u in G & u in H by A12,XBOOLE_0:def 3;
end;
case
u in H;
hence u in H & not u in G by A11,XBOOLE_0:def 4;
end;
end;
hence thesis by XBOOLE_0:def 5;
end;
hence u in (G \ H) \/ (H \ G) by XBOOLE_0:def 3;
end;
consider g being Polynomial of n,L such that
A14: g in GH and
A15: for q being Polynomial of n,L st q in GH holds g <= q,T by POLYRED:31;
A16: G-Ideal = I by A1;
A17: now
let u be set;
assume
A18: u in G or u in H;
now
per cases by A18;
case
A19: u in G;
then reconsider u9 = u as Element of Polynom-Ring(n,L);
reconsider u9 as Polynomial of n,L by POLYNOM1:def 11;
u9 is_monic_wrt T by A2,A19;
then
A20: HC(u9,T) = 1.L;
1.L <> 0.L;
hence u is Polynomial of n,L & u <> 0_(n,L) by A20,TERMORD:17;
end;
case
A21: u in H;
then reconsider u9 = u as Element of Polynom-Ring(n,L);
reconsider u9 as Polynomial of n,L by POLYNOM1:def 11;
u9 is_monic_wrt T by A4,A21;
then
A22: HC(u9,T) = 1.L;
1.L <> 0.L;
hence u is Polynomial of n,L & u <> 0_(n,L) by A22,TERMORD:17;
end;
end;
hence u is Polynomial of n,L & u <> 0_(n,L);
end;
PolyRedRel(G,T) is locally-confluent by A1;
then for f being Polynomial of n,L st f in G-Ideal holds PolyRedRel(G,T)
reduces f,0_(n,L) by Th15;
then for f being non-zero Polynomial of n,L st f in G-Ideal holds f
is_reducible_wrt G,T by Th16;
then
A23: for f being non-zero Polynomial of n,L st f in G-Ideal holds f
is_top_reducible_wrt G,T by Th17;
A24: for u being Polynomial of n,L st u in G or u in H
holds HC(u,T) = 1.L by Def6,A2,A4;
A25: now
let u be set;
assume
A26: u in GH;
then not u in G /\ H by XBOOLE_0:def 5;
then
A27: not u in G or not u in H by XBOOLE_0:def 4;
A28: u in G \/ H by A26,XBOOLE_0:def 5;
now
per cases by A28,XBOOLE_0:def 3;
case
u in G;
hence u in G\H by A27,XBOOLE_0:def 5;
end;
case
u in H;
hence u in H\G by A27,XBOOLE_0:def 5;
end;
end;
hence u in G\H or u in H\G;
end;
now
let u be object;
assume
A29: u in (G \ H) \/ (H \ G);
now
per cases by A29,XBOOLE_0:def 3;
case
u in (G \ H);
then u in G & not u in H by XBOOLE_0:def 5;
hence u in G \/ H & not u in G /\ H by XBOOLE_0:def 3,def 4;
end;
case
u in (H \ G);
then u in H & not u in G by XBOOLE_0:def 5;
hence u in G \/ H & not u in G /\ H by XBOOLE_0:def 3,def 4;
end;
end;
hence u in GH by XBOOLE_0:def 5;
end;
then
A30: GH = (G \ H) \/ (H \ G) by A9,TARSKI:2;
PolyRedRel(H,T) is locally-confluent by A3;
then for f being Polynomial of n,L st f in H-Ideal holds PolyRedRel(H,T)
reduces f,0_(n,L) by Th15;
then for f being non-zero Polynomial of n,L st f in H-Ideal holds f
is_reducible_wrt H,T by Th16;
then
A31: for f being non-zero Polynomial of n,L st f in H-Ideal holds f
is_top_reducible_wrt H,T by Th17;
per cases by A25,A14;
suppose
A32: g in G\H;
then
A33: g in G by XBOOLE_0:def 5;
then
A34: g <> 0_(n,L) by A17;
then reconsider g as non-zero Polynomial of n,L by POLYNOM7:def 1;
A35: G c= G-Ideal by IDEAL_1:def 14;
then HT(g,T) in HT(H-Ideal,T) by A16,A5,A33,A34;
then consider b9 being bag of n such that
A36: b9 in HT(H,T) and
A37: b9 divides HT(g,T) by A31,Th18;
consider h being Polynomial of n,L such that
A38: b9 = HT(h,T) and
A39: h in H and
A40: h <> 0_(n,L) by A36;
reconsider h as non-zero Polynomial of n,L by A40,POLYNOM7:def 1;
set f = g - h;
A41: h <> g by A32,A39,XBOOLE_0:def 5;
A42: now
assume
A43: f = 0_(n,L);
h = 0_(n,L) + h by POLYRED:2
.= (g + -h) + h by A43,POLYNOM1:def 7
.= g + (-h + h) by POLYNOM1:21
.= g + 0_(n,L) by POLYRED:3;
hence contradiction by A41,POLYNOM1:23;
end;
Support g <> {} by A34,POLYNOM7:1;
then HT(g,T) in Support g by TERMORD:def 6;
then
A44: g is_reducible_wrt h,T by A37,A38,POLYRED:36;
then
A45: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;
now
assume not h in H\G;
then
A46: h in G by A39,XBOOLE_0:def 5;
not h in {g} by A41,TARSKI:def 1;
then h in G\{g} by A46,XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A47: h in G\{g} & g reduces_to r,h,T by A45;
A48: g reduces_to r,G\{g},T by A47,POLYRED:def 7;
g is_irreducible_wrt G\{g},T by A2,A33;
hence contradiction by A48,POLYRED:def 9;
end;
then h in GH by A30,XBOOLE_0:def 3;
then g <= h,T by A15;
then not h < g,T by POLYRED:29;
then not HT(h,T) < HT(g,T),T by POLYRED:32;
then
A49: HT(g,T) <= HT(h,T),T by TERMORD:5;
HT(h,T) <= HT(g,T),T by A44,Th9;
then
A50: HT(h,T) = HT(g,T) by A49,TERMORD:7;
reconsider f as non-zero Polynomial of n,L by A42,POLYNOM7:def 1;
Support f <> {} by A42,POLYNOM7:1;
then
A51: HT(f,T) in Support f by TERMORD:def 6;
f.(HT(g,T)) = (g + -h).HT(g,T) by POLYNOM1:def 7
.= g.HT(g,T) + (-h).HT(g,T) by POLYNOM1:15
.= g.HT(g,T) + -(h.HT(h,T)) by A50,POLYNOM1:17
.= HC(g,T) + -(h.HT(h,T)) by TERMORD:def 7
.= HC(g,T) + - HC(h,T) by TERMORD:def 7
.= 1.L + - HC(h,T) by A24,A33
.= 1.L + - 1.L by A24,A39
.= 0.L by RLVECT_1:5;
then
A52: HT(f,T) <> HT(g,T) by A51,POLYNOM1:def 4;
HT(f,T) <= max(HT(g,T),HT(h,T),T),T by Th7;
then
A53: HT(f,T) <= HT(g,T),T by A50,TERMORD:12;
reconsider g9 = g, h9 = h as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider g9, h9 as Element of Polynom-Ring(n,L);
H c= H-Ideal by IDEAL_1:def 14;
then g9 - h9 in I by A16,A5,A33,A35,A39,IDEAL_1:15;
then f in I by Lm2;
then
A54: HT(f,T) in HT(I,T) by A42;
Support(g + -h) c= Support g \/ Support(-h) by POLYNOM1:20;
then Support f c= Support g \/ Support(-h) by POLYNOM1:def 7;
then
A55: Support f c= Support g \/ Support h by Th5;
now
per cases by A51,A55,XBOOLE_0:def 3;
case
A56: HT(f,T) in Support g;
consider b9 being bag of n such that
A57: b9 in HT(G,T) and
A58: b9 divides HT(f,T) by A16,A23,A54,Th18;
consider q being Polynomial of n,L such that
A59: b9 = HT(q,T) and
A60: q in G and
A61: q <> 0_(n,L) by A57;
reconsider q as non-zero Polynomial of n,L by A61,POLYNOM7:def 1;
g is_reducible_wrt q,T by A56,A58,A59,POLYRED:36;
then consider r being Polynomial of n,L such that
A62: g reduces_to r,q,T by POLYRED:def 8;
HT(q,T) <= HT(f,T),T by A58,A59,TERMORD:10;
then q <> g by A53,A52,TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in G\{g} by A60,XBOOLE_0:def 5;
then g reduces_to r,G\{g},T by A62,POLYRED:def 7;
then g is_reducible_wrt G\{g},T by POLYRED:def 9;
hence contradiction by A2,A33;
end;
case
A63: HT(f,T) in Support h;
consider b9 being bag of n such that
A64: b9 in HT(H,T) and
A65: b9 divides HT(f,T) by A5,A31,A54,Th18;
consider q being Polynomial of n,L such that
A66: b9 = HT(q,T) and
A67: q in H and
A68: q <> 0_(n,L) by A64;
reconsider q as non-zero Polynomial of n,L by A68,POLYNOM7:def 1;
h is_reducible_wrt q,T by A63,A65,A66,POLYRED:36;
then consider r being Polynomial of n,L such that
A69: h reduces_to r,q,T by POLYRED:def 8;
HT(q,T) <= HT(f,T),T by A65,A66,TERMORD:10;
then q <> h by A50,A53,A52,TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in H\{h} by A67,XBOOLE_0:def 5;
then h reduces_to r,H\{h},T by A69,POLYRED:def 7;
then h is_reducible_wrt H\{h},T by POLYRED:def 9;
hence contradiction by A4,A39;
end;
end;
hence thesis;
end;
suppose
A70: g in H\G;
then
A71: not g in G by XBOOLE_0:def 5;
A72: g in H by A70,XBOOLE_0:def 5;
then
A73: g <> 0_(n,L) by A17;
then reconsider g as non-zero Polynomial of n,L by POLYNOM7:def 1;
A74: H c= H-Ideal by IDEAL_1:def 14;
then HT(g,T) in HT(G-Ideal,T) by A16,A5,A72,A73;
then consider b9 being bag of n such that
A75: b9 in HT(G,T) and
A76: b9 divides HT(g,T) by A23,Th18;
consider h being Polynomial of n,L such that
A77: b9 = HT(h,T) and
A78: h in G and
A79: h <> 0_(n,L) by A75;
reconsider h as non-zero Polynomial of n,L by A79,POLYNOM7:def 1;
set f = g - h;
A80: now
assume
A81: f = 0_(n,L);
h = 0_(n,L) + h by POLYRED:2
.= (g + -h) + h by A81,POLYNOM1:def 7
.= g + (-h + h) by POLYNOM1:21
.= g + 0_(n,L) by POLYRED:3;
hence contradiction by A71,A78,POLYNOM1:23;
end;
Support g <> {} by A73,POLYNOM7:1;
then HT(g,T) in Support g by TERMORD:def 6;
then
A82: g is_reducible_wrt h,T by A76,A77,POLYRED:36;
then
A83: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;
now
assume not h in G\H;
then
A84: h in H by A78,XBOOLE_0:def 5;
not h in {g} by A71,A78,TARSKI:def 1;
then h in H\{g} by A84,XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A85: h in H\{g} & g reduces_to r,h,T by A83;
A86: g reduces_to r,H\{g},T by A85,POLYRED:def 7;
g is_irreducible_wrt H\{g},T by A4,A72;
hence contradiction by A86,POLYRED:def 9;
end;
then h in GH by A30,XBOOLE_0:def 3;
then g <= h,T by A15;
then not h < g,T by POLYRED:29;
then not HT(h,T) < HT(g,T),T by POLYRED:32;
then
A87: HT(g,T) <= HT(h,T),T by TERMORD:5;
HT(h,T) <= HT(g,T),T by A82,Th9;
then
A88: HT(h,T) = HT(g,T) by A87,TERMORD:7;
reconsider f as non-zero Polynomial of n,L by A80,POLYNOM7:def 1;
Support f <> {} by A80,POLYNOM7:1;
then
A89: HT(f,T) in Support f by TERMORD:def 6;
f.(HT(g,T)) = (g + -h).HT(g,T) by POLYNOM1:def 7
.= g.HT(g,T) + (-h).HT(g,T) by POLYNOM1:15
.= g.HT(g,T) + -(h.HT(h,T)) by A88,POLYNOM1:17
.= HC(g,T) + -(h.HT(h,T)) by TERMORD:def 7
.= HC(g,T) + - HC(h,T) by TERMORD:def 7
.= 1.L + - HC(h,T) by A24,A72
.= 1.L + - 1.L by A24,A78
.= 0.L by RLVECT_1:5;
then
A90: HT(f,T) <> HT(g,T) by A89,POLYNOM1:def 4;
HT(f,T) <= max(HT(g,T),HT(h,T),T),T by Th7;
then
A91: HT(f,T) <= HT(g,T),T by A88,TERMORD:12;
reconsider g9 = g, h9 = h as Element of Polynom-Ring(n,L) by
POLYNOM1:def 11;
reconsider g9, h9 as Element of Polynom-Ring(n,L);
G c= G-Ideal by IDEAL_1:def 14;
then g9 - h9 in I by A16,A5,A72,A74,A78,IDEAL_1:15;
then f in I by Lm2;
then
A92: HT(f,T) in HT(I,T) by A80;
Support(g + -h) c= Support g \/ Support(-h) by POLYNOM1:20;
then Support f c= Support g \/ Support(-h) by POLYNOM1:def 7;
then
A93: Support f c= Support g \/ Support h by Th5;
now
per cases by A89,A93,XBOOLE_0:def 3;
case
A94: HT(f,T) in Support g;
consider b9 being bag of n such that
A95: b9 in HT(H,T) and
A96: b9 divides HT(f,T) by A5,A31,A92,Th18;
consider q being Polynomial of n,L such that
A97: b9 = HT(q,T) and
A98: q in H and
A99: q <> 0_(n,L) by A95;
reconsider q as non-zero Polynomial of n,L by A99,POLYNOM7:def 1;
g is_reducible_wrt q,T by A94,A96,A97,POLYRED:36;
then consider r being Polynomial of n,L such that
A100: g reduces_to r,q,T by POLYRED:def 8;
HT(q,T) <= HT(f,T),T by A96,A97,TERMORD:10;
then q <> g by A91,A90,TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in H\{g} by A98,XBOOLE_0:def 5;
then g reduces_to r,H\{g},T by A100,POLYRED:def 7;
then g is_reducible_wrt H\{g},T by POLYRED:def 9;
hence contradiction by A4,A72;
end;
case
A101: HT(f,T) in Support h;
consider b9 being bag of n such that
A102: b9 in HT(G,T) and
A103: b9 divides HT(f,T) by A16,A23,A92,Th18;
consider q being Polynomial of n,L such that
A104: b9 = HT(q,T) and
A105: q in G and
A106: q <> 0_(n,L) by A102;
reconsider q as non-zero Polynomial of n,L by A106,POLYNOM7:def 1;
h is_reducible_wrt q,T by A101,A103,A104,POLYRED:36;
then consider r being Polynomial of n,L such that
A107: h reduces_to r,q,T by POLYRED:def 8;
HT(q,T) <= HT(f,T),T by A103,A104,TERMORD:10;
then HT(q,T) <> HT(h,T) by A88,A91,A90,TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in G\{h} by A105,XBOOLE_0:def 5;
then h reduces_to r,G\{h},T by A107,POLYRED:def 7;
then h is_reducible_wrt G\{h},T by POLYRED:def 9;
hence contradiction by A2,A78;
end;
end;
hence thesis;
end;
end;