Copyright (c) 2003 Association of Mizar Users
environ
vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, RELAT_1, VECTSP_1, RLVECT_1,
ORDINAL1, LATTICES, ANPROJ_1, VECTSP_2, ALGSTR_1, ARYTM_1, REALSET1,
GROUP_1, BINOP_1, ARYTM_3, TERMORD, IDEAL_1, RELAT_2, DICKSON, MCART_1,
FINSEQ_1, FINSEQ_4, BHSP_3, REWRITE1, ORDERS_1, INT_1, BINOM, TARSKI,
FINSET_1, FUNCOP_1, FILTER_2, PBOOLE, POLYRED, RLVECT_2, CARD_3, CAT_3,
SQUARE_1, FUNCT_4, CARD_1, BAGORDER, GROEB_1, PARTFUN1;
notation TARSKI, RELAT_1, XBOOLE_0, RELAT_2, XREAL_0, RELSET_1, FUNCT_1,
ORDINAL1, ALGSTR_1, RLVECT_1, PARTFUN1, FINSEQ_4, FINSET_1, DICKSON,
CARD_3, CARD_1, SUBSET_1, MCART_1, REALSET1, FINSEQ_1, YELLOW_1, PRALG_1,
VECTSP_2, VECTSP_1, POLYNOM7, REAL_1, BINOM, PBOOLE, PRE_CIRC, ORDERS_1,
POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, STRUCT_0, TERMORD, GROUP_1,
NUMBERS, NAT_1, POLYRED;
constructors REWRITE1, REAL_1, IDEAL_1, DICKSON, TERMORD, YELLOW_1, PRE_CIRC,
MONOID_0, DOMAIN_1, POLYRED, BAGORDER;
clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, ORDINAL1, VECTSP_2,
CARD_1, GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, NAT_1, INT_1, REWRITE1,
BINOM, ORDERS_1, POLYNOM7, TERMORD, IDEAL_1, YELLOW_1, SUBSET_1, DICKSON,
POLYRED, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions RELAT_2, RELAT_1;
theorems TARSKI, RELSET_1, FINSEQ_1, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1,
REAL_1, FINSEQ_4, RLVECT_1, NAT_1, ALGSTR_1, MCART_1, POLYNOM7, REWRITE1,
AXIOMS, XBOOLE_0, IDEAL_1, TERMORD, INT_1, FUNCT_1, ORDERS_1, FINSET_1,
WELLORD2, XBOOLE_1, CARD_3, DICKSON, FUNCOP_1, PBOOLE, PRALG_1, SEQM_3,
YELLOW_1, FUNCT_7, FUNCT_2, CARD_1, CARD_2, BAGORDER, POLYNOM2, XCMPLX_0,
ORDINAL1, VECTSP_2, POLYRED, XCMPLX_1, RELAT_2, PARTFUN1;
schemes RELSET_1, NAT_1, FUNCT_1;
begin :: Preliminaries
definition
let n be Ordinal,
L be right_zeroed add-associative right_complementable
unital distributive (non trivial doubleLoopStr),
p be Polynomial of n,L;
redefine func {p} -> non empty finite Subset of Polynom-Ring(n,L);
coherence
proof
now let u be set;
assume u in {p};
then u = p by TARSKI:def 1;
hence u in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 27;
end;
then {p} c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
hence thesis;
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
Field-like (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
Field-like (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
A2: s + HT(p,T) = b & 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 Field-like 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
Field-like 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;
A2: p <> 0_(n,L) by A1,POLYRED:def 5;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider s being bag of n such that
A3: s + HT(p,T) = b & g = f - (f.b/HC(p,T)) * (s *' p) by A1,POLYRED:def 5;
A4: (f.b/HC(p,T)) * (s *' p) = Monom(f.b/HC(p,T),s) *' p by POLYRED:22;
A5: not(b in Support g) by A1,POLYRED:39;
set m = Monom(f.b/HC(p,T),s);
b in Support f by A1,POLYRED:def 5;
then A6: f.b <> 0.L by POLYNOM1:def 9;
HC(p,T) <> 0.L by A2,TERMORD:17;
then A7: HC(p,T)" <> 0.L by VECTSP_1:74;
f.b/HC(p,T) = f.b * (HC(p,T)") by VECTSP_1:def 23;
then A8: f.b/HC(p,T) <> 0.L by A6,A7,VECTSP_2:def 5;
then A9: f.b/HC(p,T) is non-zero by RLVECT_1:def 13;
coefficient(m) <> 0.L by A8,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 2;
A10: 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 A9,POLYNOM7:10;
then HT(m*'p,T) in Support f by A1,A3,POLYRED:def 5;
then HT(m*'p,T) <= HT(f,T),T by TERMORD:def 6;
hence thesis by A3,A4,A5,A10;
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;
assume A1: p in P;
then reconsider P' = P as non empty Subset of L;
set f = <*p*>;
now let i be set;
assume A2: i in dom f;
dom f = {1} by FINSEQ_1:4,55;
then i = 1 by A2,TARSKI:def 1;
then f/.i = f.1 by A2,FINSEQ_4:def 4
.= p by FINSEQ_1:57
.= 1_ L * p by VECTSP_1:def 19
.= 1_ L * p * 1_ L by VECTSP_1:def 13;
hence ex u,v being Element of L, a being Element of P' st f/.i = u*a*v by A1
;
end;
then reconsider f as LinearCombination of P' by IDEAL_1:def 9;
Sum f = p by RLVECT_1:61;
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
Field-like 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
Field-like non degenerated (non empty doubleLoopStr),
p,q be Polynomial of n,L,
f,g be Element of Polynom-Ring(n,L);
assume A1: f = p & g = q;
reconsider x = -q as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider x as Element of Polynom-Ring(n,L);
x + g = -q + q by A1,POLYNOM1:def 27
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then A2: -q = -g by RLVECT_1:19;
thus p - q = p + (-q) by POLYNOM1:def 23
.= f + (-g) by A1,A2,POLYNOM1:def 27
.= f - g by RLVECT_1:def 11;
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
Field-like (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
Field-like (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;
consider b being bag of n such that
A2: f reduces_to g,0_(n,L),b,T by A1,POLYRED:def 6;
thus thesis by A2,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
Field-like (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
Field-like (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 consider p being Polynomial of n,L such that
A2: p in P & f reduces_to g,p,T by POLYRED:def 7;
thus thesis by A1,A2,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
Field-like (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
Field-like (non trivial doubleLoopStr),
P,Q being Subset of Polynom-Ring(n,L);
assume A1: P c= Q;
now let u be set;
assume A2: u in PolyRedRel(P,T);
then consider p,q being set such that
A3: p in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
q in the carrier of Polynom-Ring(n,L) & u = [p,q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A3,POLYNOM1:def 27;
A4: p in the carrier of Polynom-Ring(n,L) by A3,XBOOLE_0:def 4;
not(p in {0_(n,L)}) by A3,XBOOLE_0:def 4;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L
by A4,POLYNOM1:def 27,POLYNOM7:def 2;
p reduces_to q,P,T by A2,A3,POLYRED:def 13;
then p reduces_to q,Q,T by A1,Th3;
hence u in PolyRedRel(Q,T) by A3,POLYRED:def 13;
end;
hence thesis by TARSKI:def 3;
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 set;
assume A2: u in Support(p);
then reconsider u' = u as Element of Bags n;
A3: p.u' <> 0.L by A2,POLYNOM1:def 9;
now assume (-p).u' = 0.L;
then (-p).u' = -(-(0.L)) by RLVECT_1:30;
then -(p.u') = -(-(0.L)) by POLYNOM1:def 22
.= 0.L by RLVECT_1:30;
then p.u' = -(0.L) by RLVECT_1:30;
hence contradiction by A3,RLVECT_1:25;
end;
hence u in Support(-p) by POLYNOM1:def 9;
end;
now let u be set;
assume A4: u in Support(-p);
then reconsider u' = u as Element of Bags n;
A5: (-p).u' <> 0.L by A4,POLYNOM1:def 9;
now assume A6: p.u' = 0.L;
(-p).u' = -(p.u') by POLYNOM1:def 22;
hence contradiction by A5,A6,RLVECT_1:25;
end;
hence u in Support(p) by POLYNOM1:def 9;
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
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
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 27;
reconsider x as Element of Polynom-Ring(n,L);
A2: -(0_(n,L)) = -(0_(n,L)) + 0_(n,L) by POLYNOM1:82
.= 0_(n,L) by POLYRED:3;
0.(Polynom-Ring(n,L)) = 0_(n,L) by POLYNOM1:def 27;
then x + 0.(Polynom-Ring(n,L))
= (-p) + 0_(n,L) by POLYNOM1:def 27
.= 0_(n,L) by A1,A2,POLYNOM1:82
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then -p = -(0.Polynom-Ring(n,L)) by RLVECT_1:19
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:25
.= p by A1,POLYNOM1:def 27;
hence thesis;
suppose p <> 0_(n,L);
then A3: Support(p) <> {} by POLYNOM7:1;
then A4: HT(p,T) in Support(p) &
for b being bag of n st b in Support p holds b <= HT(p,T),T
by TERMORD:def 6;
Support(-p) <> {} by A3,Th5;
then HT(-p,T) in Support(-p) &
for b being bag of n st b in Support(-p) holds b <= HT(-p,T),T
by TERMORD:def 6;
then HT(p,T) in Support(-p) & HT(-p,T) in Support(p) by A4,Th5;
then HT(p,T) <= HT(-p,T),T & HT(-p,T) <= HT(p,T),T
by TERMORD:def 6;
hence thesis by TERMORD:7;
end;
theorem Th7:
for n being Ordinal,
T being admissible connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty 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
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 23;
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
Field-like (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
Field-like (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: P[0]
proof let f,g be Polynomial of n,L;
assume Support f c= Support g & Card(Support f) = 0;
then Support f,{} are_equipotent by CARD_1:def 5;
then Support f = {} by CARD_1:46;
then f = 0_(n,L) by POLYNOM7:1;
hence f <= g,T by POLYRED:30;
end;
A3: now let k be Nat;
assume A4: P[k];
now let f,g be Polynomial of n,L;
assume A5: Support f c= Support g & Card(Support f) = k+1;
set rf = Red(f,T), rg = Red(g,T);
set R = RelStr(# Bags n, T#);
now assume Support f = {};
then Card(Support f) = 0 by CARD_1:def 5;
hence contradiction by A5;
end;
then A6: HT(f,T) in Support f by TERMORD:def 6;
then g <> 0_(n,L) & f <> 0_(n,L) by A5,POLYNOM7:1;
then A7: g is non-zero & f is non-zero by POLYNOM7:def 2;
now per cases;
case A8: HT(f,T) = HT(g,T);
A9: Support(rf) = Support(f) \ {HT(f,T)} &
Support(rg) = Support(g) \ {HT(g,T)} by TERMORD:36;
now let u be set;
assume u in Support(rf);
then u in Support f & not(u in {HT(f,T)}) by A9,XBOOLE_0:def 4;
hence u in Support(rg) by A5,A8,A9,XBOOLE_0:def 4;
end;
then A10: Support(rf) c= Support(rg) by TARSKI:def 3;
A11: Support(rf,T) = Support rf & Support(rg,T) = Support rg &
Support(f,T) = Support f & Support(g,T) = Support g
by POLYRED:def 4;
for u being set holds u in {HT(f,T)}
implies u in Support f by A6,TARSKI:def 1;
then A12: {HT(f,T)} c= Support f by TARSKI:def 3;
A13: Support(rf) \/ {HT(f,T)}
= Support f \/ {HT(f,T)} by A9,XBOOLE_1:39
.= Support f by A12,XBOOLE_1:12;
HT(f,T) in {HT(f,T)} by TARSKI:def 1;
then not(HT(f,T) in Support Red(f,T)) by A9,XBOOLE_0:def 4;
then card(Support(Red(f,T))) + 1 = k + 1 by A5,A13,CARD_2:54;
then card(Support(Red(f,T))) = k by XCMPLX_1:2;
then rf <= rg,T by A4,A10;
then [Support rf,Support rg] in FinOrd RelStr(# Bags n, T#)
by POLYRED:def 2;
then A14: [Support(rf,T),Support(rg,T)] in union rng FinOrd-Approx R
by A11,BAGORDER:def 17;
A15: Support(f,T) <> {} & Support(g,T) <> {} by A5,A6,POLYRED:def 4;
A16: PosetMax(Support(f,T)) = HT(g,T) by A7,A8,POLYRED:24
.= PosetMax(Support(g,T)) by A7,POLYRED:24;
A17: Support(f,T)\{PosetMax(Support(f,T))} = Support(rf,T)
by A7,A9,A11,POLYRED:24;
Support(g,T)\{PosetMax(Support(g,T))} = Support(rg,T)
by A7,A9,A11,POLYRED:24;
then [Support(f,T),Support(g,T)] in union rng FinOrd-Approx R
by A14,A15,A16,A17,BAGORDER:36;
then [Support f,Support g] in FinOrd RelStr(# Bags n, T#)
by A11,BAGORDER:def 17;
hence f <= g,T by POLYRED:def 2;
case A18: 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 A5,A6,TERMORD:def 6;
end;
then HT(f,T) <= HT(g,T),T by TERMORD:5;
then HT(f,T) < HT(g,T),T by A18,TERMORD:def 3;
then f < g,T by POLYRED:32;
hence f <= g,T by POLYRED:def 3;
end;
hence f <= g,T;
end;
hence P[k+1];
end;
A19: for k being Nat holds P[k] from Ind(A2,A3);
consider k being Nat such that
A20: Card(Support q) = k;
thus thesis by A1,A19,A20;
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
Field-like 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
Field-like 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;
A2: b <= HT(f,T),T by A1,TERMORD:def 6;
HT(p,T) <= b,T by A1,TERMORD:10;
hence thesis by A2,TERMORD:8;
end;
begin :: Characterization of Groebner Bases
theorem Th10:
::: proposition 5.33, p. 205
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (non trivial doubleLoopStr),
p being Polynomial of n,L
holds PolyRedRel({p},T) is locally-confluent
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (non trivial doubleLoopStr),
p be Polynomial of n,L;
set R = PolyRedRel({p},T);
per cases;
suppose A1: p = 0_(n,L);
now let a,b,c be set;
assume A2: [a,b] in R & [a,c] in R;
then consider p',q being set such that
A3: p' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
q in the carrier of Polynom-Ring(n,L) & [a,b] = [p',q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A3,POLYNOM1:def 27;
A4: p' in the carrier of Polynom-Ring(n,L) by A3,XBOOLE_0:def 4;
not(p' in {0_(n,L)}) by A3,XBOOLE_0:def 4;
then p' <> 0_(n,L) by TARSKI:def 1;
then reconsider p' as non-zero Polynomial of n,L
by A4,POLYNOM1:def 27,POLYNOM7:def 2;
p' reduces_to q,{p},T by A2,A3,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A5: g in {p} & p' reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A1,A5,TARSKI:def 1;
then p' is_reducible_wrt 0_(n,L),T by A5,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
hence PolyRedRel({p},T) is locally-confluent by REWRITE1:def 24;
suppose p <> 0_(n,L);
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 2;
now let a,b,c being set;
assume A6: [a,b] in R & [a,c] in R;
then consider pa,pb being set such that
A7: pa in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
pb in the carrier of Polynom-Ring(n,L) & [a,b] = [pa,pb]
by ZFMISC_1:def 2;
reconsider pb as Polynomial of n,L by A7,POLYNOM1:def 27;
A8: pa in the carrier of Polynom-Ring(n,L) by A7,XBOOLE_0:def 4;
not(pa in {0_(n,L)}) by A7,XBOOLE_0:def 4;
then pa <> 0_(n,L) by TARSKI:def 1;
then reconsider pa as non-zero Polynomial of n,L
by A8,POLYNOM1:def 27,POLYNOM7:def 2;
A9: pa = [a,b]`1 by A7,MCART_1:def 1 .= a by MCART_1:def 1;
A10: pb = [a,b]`2 by A7,MCART_1:def 2 .= b by MCART_1:def 2;
then pa reduces_to pb,{p},T by A6,A9,POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A11: p' in {p} & pa reduces_to pb,p',T by POLYRED:def 7;
A12: pa reduces_to pb,p,T by A11,TARSKI:def 1;
consider pa',pc being set such that
A13: pa' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
pc in the carrier of Polynom-Ring(n,L) & [a,c] = [pa',pc]
by A6,ZFMISC_1:def 2;
reconsider pc as Polynomial of n,L by A13,POLYNOM1:def 27;
A15: pc = [a,c]`2 by A13,MCART_1:def 2 .= c by MCART_1:def 2;
then pa reduces_to pc,{p},T by A6,A9,POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A16: p' in {p} & pa reduces_to pc,p',T by POLYRED:def 7;
A17: pa reduces_to pc,p,T by A16,TARSKI:def 1;
A18: p in {p} by TARSKI:def 1;
now per cases;
case A19: pb = 0_(n,L);
then consider mb being Monomial of n,L such that
A20: 0_(n,L) = pa - mb *' p by A12,Th1;
0_(n,L) + mb*'p = (pa + -(mb*'p)) + mb*'p by A20,POLYNOM1:def 23;
then mb*'p = (pa + -(mb*'p)) + mb*'p by POLYRED:2;
then mb*'p = pa + (-(mb*'p) + mb*'p) by POLYNOM1:80;
then mb*'p = pa + 0_(n,L) by POLYRED:3;
then mb*'p = pa by POLYNOM1:82;
then consider mc being Monomial of n,L such that
A21: pc = mb *' p - mc *' p by A17,Th1;
pc = mb *' p + -(mc *' p) by A21,POLYNOM1:def 23;
then pc = mb *' p + (-mc) *' p by POLYRED:6;
then pc = (mb + -mc) *' p by POLYNOM1:85;
then A22: pc = (mb - mc) *' p by POLYNOM1:def 23;
now per cases;
case mb = mc;
then pc = 0_(n,L) *'p by A22,POLYNOM1:83;
then pc = 0_(n,L) by POLYRED:5;
then R reduces pb,0_(n,L) & R reduces pc,0_(n,L) by A19,REWRITE1:13;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15;
case A23: mb <> mc;
now assume mb - mc = 0_(n,L);
then (mb + -mc) + mc = 0_(n,L) + mc by POLYNOM1:def 23;
then mb + (-mc + mc) = 0_(n,L) + mc by POLYNOM1:80;
then mb + 0_(n,L) = 0_(n,L) + mc by POLYRED:3;
then mb + 0_(n,L) = mc by POLYRED:2;
hence contradiction by A23,POLYNOM1:82;
end;
then reconsider hh = mb - mc as non-zero Polynomial of n,L
by POLYNOM7:def 2;
A24: R reduces hh*'p,0_(n,L) by A18,POLYRED:45;
R reduces pb,0_(n,L) by A19,REWRITE1:13;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15,A22,
A24;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
case A25: pc = 0_(n,L);
then consider mc being Monomial of n,L such that
A26: 0_(n,L) = pa - mc *' p by A17,Th1;
0_(n,L) + mc*'p = (pa + -(mc*'p)) + mc*'p by A26,POLYNOM1:def 23;
then mc*'p = (pa + -(mc*'p)) + mc*'p by POLYRED:2;
then mc*'p = pa + (-(mc*'p) + mc*'p) by POLYNOM1:80;
then mc*'p = pa + 0_(n,L) by POLYRED:3;
then mc*'p = pa by POLYNOM1:82;
then consider mb being Monomial of n,L such that
A27: pb = mc *' p - mb *' p by A12,Th1;
pb = mc *' p + -(mb *' p) by A27,POLYNOM1:def 23;
then pb = mc *' p + (-mb) *' p by POLYRED:6;
then pb = (mc + -mb) *' p by POLYNOM1:85;
then A28: pb = (mc - mb) *' p by POLYNOM1:def 23;
now per cases;
case mb = mc;
then pb = 0_(n,L) *'p by A28,POLYNOM1:83;
then pb = 0_(n,L) by POLYRED:5;
then R reduces pb,0_(n,L) & R reduces pc,0_(n,L) by A25,REWRITE1:13;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15;
case A29: mb <> mc;
now assume mc - mb = 0_(n,L);
then (mc + -mb) + mb = 0_(n,L) + mb by POLYNOM1:def 23;
then mc + (-mb + mb) = 0_(n,L) + mb by POLYNOM1:80;
then mc + 0_(n,L) = 0_(n,L) + mb by POLYRED:3;
then mc + 0_(n,L) = mb by POLYRED:2;
hence contradiction by A29,POLYNOM1:82;
end;
then reconsider hh = mc - mb as non-zero Polynomial of n,L
by POLYNOM7:def 2;
A30: R reduces hh*'p,0_(n,L) by A18,POLYRED:45;
R reduces pc,0_(n,L) by A25,REWRITE1:13;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15,A28,
A30;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
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 2;
now per cases;
case pb = pc;
then R reduces pb,pb & R reduces pc,pb by REWRITE1:13;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15;
case A31: pb <> pc;
now assume pb - pc = 0_(n,L);
then (pb + -pc) + pc = 0_(n,L) + pc by POLYNOM1:def 23;
then pb + (-pc + pc) = 0_(n,L) + pc by POLYNOM1:80;
then pb + 0_(n,L) = 0_(n,L) + pc by POLYRED:3;
then pb + 0_(n,L) = pc by POLYRED:2;
hence contradiction by A31,POLYNOM1:82;
end;
then reconsider h = pb-pc as non-zero Polynomial of n,L
by POLYNOM7:def 2;
consider mb being Monomial of n,L such that
A32: pb = pa - mb *' p by A12,Th1;
consider mc being Monomial of n,L such that
A33: pc = pa - mc *' p by A17,Th1;
now assume -mb + mc = 0_(n,L);
then mc + (-mb + mb) = 0_(n,L) + mb by POLYNOM1:80;
then mc + 0_(n,L) = 0_(n,L) + mb by POLYRED:3;
then mc + 0_(n,L) = mb by POLYRED:2;
hence contradiction by A31,A32,A33,POLYNOM1:82;
end;
then reconsider hh = -mb + mc as non-zero Polynomial of n,L
by POLYNOM7:def 2;
h = (pa - mb *' p) + -(pa - mc *' p) by A32,A33,POLYNOM1:def 23
.= (pa - mb *' p) + -(pa + -(mc *' p)) by POLYNOM1:def 23
.= (pa - mb *' p) + (-pa + --(mc *' p)) by POLYRED:1
.= (pa + -(mb *' p)) + (-pa + --(mc *' p)) by POLYNOM1:def 23
.= ((pa + -(mb *' p)) + -pa) + (mc *' p) by POLYNOM1:80
.= ((pa + -pa) + -(mb *' p)) + (mc *' p) by POLYNOM1:80
.= (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:85;
then PolyRedRel({p},T) reduces h,0_(n,L) by A18,POLYRED:45;
then consider f1,g1 being Polynomial of n,L such that
A34: f1 - g1 = 0_(n,L) &
R reduces pb,f1 & R reduces pc,g1 by POLYRED:49;
(f1 + -g1) + g1 = 0_(n,L) + g1 by A34,POLYNOM1:def 23;
then f1 + (-g1 + g1) = 0_(n,L) + g1 by POLYNOM1:80;
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:82;
hence ex d being set st R reduces b,d & R reduces c,d by A10,A15,A34;
end;
hence ex d being set st R reduces b,d & R reduces c,d;
end;
hence b,c are_convergent_wrt R by REWRITE1:def 7;
end;
hence thesis by REWRITE1:def 24;
end;
theorem
::: corollary 5.34, p. 205
for n being Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
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 & P-Ideal = {p}-Ideal;
set R = PolyRedRel(P,T);
now let a,b,c being set;
assume A2: [a,b] in R & [a,c] in R;
then consider pa,pb being set such that
A3: pa in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
pb in the carrier of Polynom-Ring(n,L) & [a,b] = [pa,pb]
by ZFMISC_1:def 2;
reconsider pb as Polynomial of n,L by A3,POLYNOM1:def 27;
A4: pb = [a,b]`2 by A3,MCART_1:def 2 .= b by MCART_1:def 2;
consider pa',pc being set such that
A5: pa' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
pc in the carrier of Polynom-Ring(n,L) & [a,c] = [pa',pc]
by A2,ZFMISC_1:def 2;
reconsider pc as Polynomial of n,L by A5,POLYNOM1:def 27;
A7: pc = [a,c]`2 by A5,MCART_1:def 2 .= c by MCART_1:def 2;
A8: a,b are_convertible_wrt R & a,c are_convertible_wrt R by A2,REWRITE1:30;
then b,a are_convertible_wrt R by REWRITE1:32;
then A9: pb,pc are_convertible_wrt R by A4,A7,A8,REWRITE1:31;
reconsider pb' = pb, pc' = pc as Element of
Polynom-Ring(n,L) by POLYNOM1:def 27;
reconsider pc',pb' as Element of Polynom-Ring(n,L);
pb',pc' are_congruent_mod {p}-Ideal by A1,A9,POLYRED:57;
then A10: pb,pc are_convertible_wrt PolyRedRel({p},T) by POLYRED:58;
set Rp = PolyRedRel({p},T);
reconsider Rp as locally-confluent strongly-normalizing Relation
by Th10;
b,c are_convergent_wrt Rp by A4,A7,A10,REWRITE1:def 23;
then consider d being set such that
A11: Rp reduces b,d & Rp reduces c,d by REWRITE1:def 7;
for u being set holds u in {p} implies u in P by A1,TARSKI:def 1;
then {p} c= P by TARSKI:def 3;
then Rp c= R by Th4;
then R reduces b,d & R reduces c,d by A11,REWRITE1:23;
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
unital distributive non trivial (non empty doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
func HT(P,T) -> Subset of Bags n equals :Def1:
{ 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 set;
assume u in M;
then consider p being Polynomial of n,L such that
A1: u = HT(p,T) & p in P & p <> 0_(n,L);
thus u in Bags n by A1;
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 :Def2:
{ b where b is Element of Bags n :
ex b' being bag of n st b' in S & b' divides b };
coherence
proof
set M = {b where b is Element of Bags n :
ex b' being bag of n st b' in S & b' divides b};
now let u be set;
assume u in M;
then consider b being Element of Bags n such that
A1: u = b & ex b' being bag of n st b' in S & b' divides b;
thus u in Bags n by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th12:
::: theorem 5.35 (i) ==> (ii), p. 206
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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
proof
let n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
P being Subset of Polynom-Ring(n,L);
assume PolyRedRel(P,T) is locally-confluent;
then reconsider R = PolyRedRel(P,T) as
strongly-normalizing locally-confluent Relation;
R is confluent;
hence thesis;
end;
theorem Th13:
::: 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
Field-like (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
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
assume PolyRedRel(P,T) is confluent;
then reconsider R = PolyRedRel(P,T) as confluent Relation;
R is with_UN_property;
hence thesis;
end;
theorem Th14:
::: theorem 5.35 (iii) ==> (iv), p. 206
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
assume PolyRedRel(P,T) is with_UN_property;
then reconsider R = PolyRedRel(P,T) as
with_UN_property weakly-normalizing Relation;
R is with_Church-Rosser_property;
hence thesis;
end;
Lm4:
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
f being Polynomial of n,L,
g being set,
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
Field-like (non trivial doubleLoopStr),
f be Polynomial of n,L,
g be set,
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 & p.len p = g by REWRITE1:def 3;
len p > 0 by REWRITE1:def 2;
then A2: 1 <= len(p) by RLVECT_1:99;
then reconsider l = len p - 1 as Nat by INT_1:18;
A3: l + 1 = (len p + -1) + 1 by XCMPLX_0:def 8
.= len p + (-1 + 1) by XCMPLX_1:1
.= len p + 0;
then 1 <= l + 1 & l + 1 <= len p by NAT_1:37;
then l + 1 in Seg(len p) by FINSEQ_1:3;
then A4: l + 1 in dom p by FINSEQ_1:def 3;
set h = p.l;
per cases;
suppose len p = 1;
hence thesis by A1;
suppose len p <> 1;
then 1 < len p by A2,REAL_1:def 5;
then 1 + -1 < len p + -1 by REAL_1:67;
then 1 - 1 < len p - 1 by XCMPLX_0:def 8;
then 0 + 1 < l + 1 by REAL_1:67;
then 1 <= l & l <= l + 1 by NAT_1:38;
then l in Seg(len p) by A3,FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A1,A3,A4,REWRITE1:def 2;
then consider h',g' being set such that
A5: [h,g] = [h',g'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
g' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
g = [h',g']`2 by A5,MCART_1:def 2 .= g' by MCART_1:def 2;
hence g is Polynomial of n,L by A5,POLYNOM1:def 27;
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
Field-like (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
Field-like (non trivial doubleLoopStr),
f,g be Polynomial of n,L,
P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume A1: PolyRedRel(P,T) reduces f,g & g <> f;
then consider p being RedSequence of R such that
A2: p.1 = f & p.len p = g by REWRITE1:def 3;
len p > 0 &
for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R
by REWRITE1:def 2;
then len p + 1 > 0 + 1 by REAL_1:67;
then A3: 1 <= len p by NAT_1:38;
then 1 < len p by A1,A2,AXIOMS:21;
then A4: 1 + 1 <= len p by NAT_1:38;
then A5: 1 + 1 in Seg(len p) by FINSEQ_1:3;
1 in Seg(len p) by A3,FINSEQ_1:3;
then A6: 1 in dom p & 1 + 1 in dom p by A5,FINSEQ_1:def 3;
set h = p.2;
A7: [f,h] in R by A2,A6,REWRITE1:def 2;
then consider f',h' being set such that
A8: [f,h] = [f',h'] &
f' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
h' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
h = [f',h']`2 by A8,MCART_1:def 2 .= h' by MCART_1:def 2;
then reconsider h as Polynomial of n,L by A8,POLYNOM1:def 27;
A9: f reduces_to h,P,T by A7,POLYRED:def 13;
len p in Seg(len p) by A3,FINSEQ_1:3;
then len p in dom p by FINSEQ_1:def 3;
then PolyRedRel(P,T) reduces h,g by A2,A4,A6,REWRITE1:18;
hence thesis by A9;
end;
theorem Th15:
::: theorem 5.35 (iv) ==> (v), p. 206
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
P be non empty Subset of Polynom-Ring(n,L);
assume A1: PolyRedRel(P,T) is with_Church-Rosser_property;
set R = PolyRedRel(P,T);
now let f be Polynomial of n,L;
assume A2: f in P-Ideal;
reconsider f' = f as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider f' as Element of Polynom-Ring(n,L);
reconsider e = 0_(n,L) as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider e as Element of Polynom-Ring(n,L);
f - 0_(n,L) = f' - e by Lm2;
then f' - e in P-Ideal by A2,POLYRED:4;
then f',e are_congruent_mod P-Ideal by POLYRED:def 14;
then f',e are_convertible_wrt R by POLYRED:58;
then f',e are_convergent_wrt R by A1,REWRITE1:def 23;
then consider c being set such that
A3: R reduces f,c & R reduces 0_(n,L),c by REWRITE1:def 7;
reconsider c' = c as Polynomial of n,L by A3,Lm4;
now assume c' <> 0_(n,L);
then consider h being Polynomial of n,L such that
A4: 0_(n,L) reduces_to h,P,T & PolyRedRel(P,T) reduces h,c' by A3,Lm5;
consider pp being Polynomial of n,L such that
A5: pp in P & 0_(n,L) reduces_to h,pp,T by A4,POLYRED:def 7;
0_(n,L) is_reducible_wrt pp,T by A5,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
Field-like (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
Field-like (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 2;
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 Nat,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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 Nat,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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
let f be non-zero Polynomial of n,L;
assume A2: f in P-Ideal;
set H = {g where g is non-zero Polynomial of n,L :
g in P-Ideal & not(g is_top_reducible_wrt P,T)};
assume not(f is_top_reducible_wrt P,T);
then A3: f in H by A2;
now let u be set;
assume u in H;
then consider g' being non-zero Polynomial of n,L such that
A4: u = g' & g' in P-Ideal & not(g' is_top_reducible_wrt P,T);
thus u in the carrier of Polynom-Ring(n,L) by A4;
end;
then H c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
then reconsider H as non empty Subset of Polynom-Ring(n,L)
by A3;
consider p being Polynomial of n,L such that
A5: p in H &
for q being Polynomial of n,L st q in H holds p <= q,T
by POLYRED:31;
consider p' being non-zero Polynomial of n,L such that
A6: p' = p & p' in P-Ideal & not(p' is_top_reducible_wrt P,T) by A5;
reconsider p as non-zero Polynomial of n,L by A6;
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 & p reduces_to q,u,T by A7,POLYRED:def 7;
consider b being bag of n such that
A9: p reduces_to q,u,b,T by A8,POLYRED:def 6;
A10: u <> 0_(n,L) by A9,POLYRED:def 5;
then reconsider u as non-zero Polynomial of n,L by POLYNOM7:def 2;
A11: q < p,T by A8,POLYRED:43;
consider m being Monomial of n,L such that
A12: q = p - m *' u by A8,Th1;
reconsider uu = u, pp = p, mm = m
as Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
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 A13: pp + -(mm * uu) in P-Ideal by A6,IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 27;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then A14: q in P-Ideal by A12,A13,RLVECT_1:def 11;
A15: p <> 0_(n,L) by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A16: HT(p,T) in Support p by TERMORD:def 6;
consider b being bag of n such that
A17: p reduces_to q,u,b,T by A8,POLYRED:def 6;
b in Support p by A17,POLYRED:def 5;
then A18: b <= HT(p,T),T by TERMORD:def 6;
now assume b = HT(p,T);
then p top_reduces_to q,u,T by A17,POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A6,A8,POLYRED:def 12;
end;
then b < HT(p,T),T by A18,TERMORD:def 3;
then A19: HT(p,T) in Support q by A16,A17,POLYRED:40;
now per cases;
case A20: q <> 0_(n,L);
then reconsider q as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support q <> {} by A20,POLYNOM7:1;
then A21: HT(q,T) in Support q by TERMORD:def 6;
A22: HT(p,T) <= HT(q,T),T by A19,TERMORD:def 6;
HT(q,T) <= HT(p,T),T by A8,A21,POLYRED:42;
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 A14;
then p <= q,T by A5;
hence contradiction by A11,POLYRED:29;
end;
then consider u' being Polynomial of n,L such that
A24: u' in P & q is_top_reducible_wrt u',T by POLYRED:def 12;
consider q' being Polynomial of n,L such that
A25: q top_reduces_to q',u',T by A24,POLYRED:def 11;
A26: q reduces_to q',u',HT(q,T),T by A25,POLYRED:def 10;
then A27: q <> 0_(n,L) & u' <> 0_(n,L) &
HT(q,T) in Support q &
ex s being bag of n
st s + HT(u',T) = HT(q,T) &
q' = q - (q.(HT(q,T))/HC(u',T)) * (s *' u')
by POLYRED:def 5;
consider s being bag of n such that
A28: s + HT(u',T) = HT(q,T) &
q' = q - (q.(HT(q,T))/HC(u',T)) * (s *' u') by A26,POLYRED:def 5;
set qq = p - (p.(HT(p,T))/HC(u',T)) * (s *' u');
A29: p <> 0_(n,L) by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then HT(p,T) in Support p by TERMORD:def 6;
then p reduces_to qq,u',HT(p,T),T by A23,A27,A28,A29,POLYRED:def 5;
then p top_reduces_to qq,u',T by POLYRED:def 10;
then p is_top_reducible_wrt u',T by POLYRED:def 11;
hence contradiction by A6,A24,POLYRED:def 12;
case q = 0_(n,L);
then A30: m *' u = (p - m *' u) + m *' u by A12,POLYRED:2
.= (p + -(m *' u)) + m *' u by POLYNOM1:def 23
.= p + (-(m *' u) + m *' u) by POLYNOM1:80
.= p + 0_(n,L) by POLYRED:3
.= p by POLYNOM1:82;
now assume A31: m = 0_(n,L);
p <> 0_(n,L) by POLYNOM7:def 2;
hence contradiction by A30,A31,POLYRED:5;
end;
then reconsider m as non-zero Polynomial of n,L by POLYNOM7:def 2;
A32: HT(p,T) = HT(m,T) + HT(u,T) by A30,TERMORD:31;
set pp = p - (p.(HT(p,T))/HC(u,T)) * (HT(m,T) *' u);
p reduces_to pp,u,HT(p,T),T by A10,A15,A16,A32,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;
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
Field-like (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 b' being bag of n st b' in HT(P,T) & b' 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
Field-like (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 b in {HT(p,T) where p is Polynomial of n,L :
p in P-Ideal & p <> 0_(n,L)} by Def1;
then consider p being Polynomial of n,L such that
A2: b = HT(p,T) & p in P-Ideal & p <> 0_(n,L);
reconsider p as non-zero Polynomial of n,L by A2,POLYNOM7:def 2;
p is_top_reducible_wrt P,T by A1,A2;
then consider u being Polynomial of n,L such that
A3: u in P & p is_top_reducible_wrt u,T by POLYRED:def 12;
consider q being Polynomial of n,L such that
A4: p top_reduces_to q,u,T by A3,POLYRED:def 11;
A5: p reduces_to q,u,HT(p,T),T by A4,POLYRED:def 10;
then consider s being bag of n such that
A6: s + HT(u,T) = HT(p,T) & q = p - (p.(HT(p,T))/HC(u,T)) * (s *' u)
by POLYRED:def 5;
u <> 0_(n,L) by A5,POLYRED:def 5;
then HT(u,T) in {HT(r,T) where r is Polynomial of n,L :
r in P & r <> 0_(n,L)} by A3;
then A7: HT(u,T) in HT(P,T) by Def1;
HT(u,T) divides b by A2,A6,POLYNOM1:54;
hence ex b' being bag of n st b' in HT(P,T) & b' divides b by A7;
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
Field-like (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 b' being bag of n st b' in HT(P,T) & b' 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
Field-like (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 b' being bag of n st b' in HT(P,T) & b' divides b;
now let u be set;
assume A2: u in HT(P-Ideal,T);
then u in {HT(p,T) where p is Polynomial of n,L :
p in P-Ideal & p <> 0_(n,L)} by Def1;
then consider p being Polynomial of n,L such that
A3: u = HT(p,T) & p in P-Ideal & p <> 0_(n,L);
reconsider u' = u as Element of Bags n by A3;
consider b' being bag of n such that
A4: b' in HT(P,T) & b' divides u' by A1,A2;
u' in { b where b is Element of Bags n :
ex b' being bag of n st b' in HT(P,T) & b' divides b} by A4;
hence u in multiples(HT(P,T)) by Def2;
end;
hence thesis by TARSKI:def 3;
end;
theorem
::: theorem 5.35 (ix) ==> (i), p. 206
for n being Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
assume A1: HT(P-Ideal,T) c= multiples(HT(P,T));
set R = PolyRedRel(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 A3: f in P-Ideal & f <> 0_(n,L);
then HT(f,T) in
{HT(p,T) where p is Polynomial of n,L : p in P-Ideal & p <> 0_(n,L)};
then HT(f,T) in HT(P-Ideal,T) by Def1;
then HT(f,T) in multiples(HT(P,T)) by A1;
then HT(f,T) in {b where b is Element of Bags n :
ex b' being bag of n st b' in HT(P,T) & b' divides b } by Def2;
then consider b being Element of Bags n such that
A4: b = HT(f,T) & ex b' being bag of n st b' in HT(P,T) & b' divides b;
consider b' being bag of n such that
A5: b' in HT(P,T) & b' divides HT(f,T) by A4;
b' in {HT(p,T) where p is Polynomial of n,L : p in P & p <> 0_(n,L)}
by A5,Def1;
then consider p being Polynomial of n,L such that
A6: b' = HT(p,T) & p in P & p <> 0_(n,L);
consider s being bag of n such that
A7: b' + s = HT(f,T) by A5,TERMORD:1;
set g = f - (f.(HT(f,T))/HC(p,T)) * (s *' p);
Support f <> {} by A3,POLYNOM7:1;
then HT(f,T) in Support f by TERMORD:def 6;
then f reduces_to g,p,HT(f,T),T by A3,A6,A7,POLYRED:def 5;
then f reduces_to g,p,T by POLYRED:def 6;
then f reduces_to g,P,T by A6,POLYRED:def 7;
hence thesis by POLYRED:def 9;
end;
A8: 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 A9: f in P-Ideal;
per cases;
suppose f = 0_(n,L);
hence thesis by REWRITE1:13;
suppose A10: f <> 0_(n,L);
assume A11: not(R reduces f,0_(n,L));
f is_reducible_wrt P,T by A2,A9,A10;
then consider v being Polynomial of n,L such that
A12: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in R by A12,POLYRED:def 13;
then f in field R by RELAT_1:30;
then f has_a_normal_form_wrt R by REWRITE1:def 14;
then consider g being set such that
A13: g is_a_normal_form_of f,R by REWRITE1:def 11;
A14: g is_a_normal_form_wrt R & R reduces f,g by A13,REWRITE1:def 6;
A15: g <> 0_(n,L) by A11,A13,REWRITE1:def 6;
reconsider g' = g as Polynomial of n,L by A14,Lm4;
reconsider ff = f, gg = g' as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider ff,gg as Element of Polynom-Ring(n,L);
f - g' = ff - gg by Lm2;
then ff - gg in P-Ideal by A14,POLYRED:59;
then A16: (ff - gg) - ff in P-Ideal by A9,IDEAL_1:16;
(ff - gg) - ff = (ff + -gg) - ff by RLVECT_1:def 11
.= (ff + -gg) + -ff by RLVECT_1:def 11
.= (ff + -ff) + -gg by RLVECT_1:def 6
.= 0.(Polynom-Ring(n,L)) + -gg by RLVECT_1:16
.= - gg by ALGSTR_1:def 5;
then --gg in P-Ideal by A16,IDEAL_1:14;
then g in P-Ideal by RLVECT_1:30;
then g' is_reducible_wrt P,T by A2,A15;
then consider u being Polynomial of n,L such that
A17: g' reduces_to u,P,T by POLYRED:def 9;
[g',u] in R by A17,POLYRED:def 13;
hence contradiction by A14,REWRITE1:def 5;
end;
now let a,b,c being set;
assume A18: [a,b] in R & [a,c] in R;
then consider a',b' being set such that
A19: a' in ((the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}) &
b' in the carrier of Polynom-Ring(n,L) &
[a,b] = [a',b'] by ZFMISC_1:def 2;
A20: b' = [a,b]`2 by A19,MCART_1:def 2 .= b by MCART_1:def 2;
consider aa,c' being set such that
A21: aa in ((the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}) &
c' in the carrier of Polynom-Ring(n,L) &
[a,c] = [aa,c'] by A18,ZFMISC_1:def 2;
A22: c' = [a,c]`2 by A21,MCART_1:def 2 .= c by MCART_1:def 2;
reconsider b', c' as Polynomial of n,L by A19,A21,POLYNOM1:def 27;
reconsider bb = b', cc = c' as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider bb,cc as Element of Polynom-Ring(n,L);
A23: b' - c' = bb - cc by Lm2;
a,b are_convertible_wrt R & a,c are_convertible_wrt R by A18,REWRITE1:30;
then b,a are_convertible_wrt R & a,c are_convertible_wrt R by REWRITE1:32;
then b,c are_convertible_wrt R by REWRITE1:31;
then bb,cc are_congruent_mod P-Ideal by A20,A22,POLYRED:57;
then bb - cc in P-Ideal by POLYRED:def 14;
then PolyRedRel(P,T) reduces b'-c',0_(n,L) by A8,A23;
hence b,c are_convergent_wrt R by A20,A22,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
Field-like (non trivial doubleLoopStr),
G be Subset of Polynom-Ring(n,L);
pred G is_Groebner_basis_wrt T means :Def3:
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
Field-like (non trivial doubleLoopStr),
G,I be Subset of Polynom-Ring(n,L);
pred G is_Groebner_basis_of I,T means :Def4:
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
Field-like (non trivial doubleLoopStr),
P being Subset of Polynom-Ring(n,L),
a,b being set 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
Field-like (non trivial doubleLoopStr),
P be Subset of Polynom-Ring(n,L),
f,g be set;
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 & p.len p = g by REWRITE1:def 3;
len p > 0 by REWRITE1:def 2;
then A3: 1 <= len(p) by RLVECT_1:99;
then reconsider l = len p - 1 as Nat by INT_1:18;
A4: l + 1 = (len p + -1) + 1 by XCMPLX_0:def 8
.= len p + (-1 + 1) by XCMPLX_1:1
.= len p + 0;
then 1 <= l + 1 & l + 1 <= len p by NAT_1:37;
then l + 1 in Seg(len p) by FINSEQ_1:3;
then A5: l + 1 in dom p by FINSEQ_1:def 3;
set q = p.(1+1), h = p.l;
now per cases;
case len p = 1;
hence f is Polynomial of n,L by A1,A2;
case len p <> 1;
then A6: 1 < len p by A3,REAL_1:def 5;
1 in Seg(len p) by A3,FINSEQ_1:3;
then A7: 1 in dom p by FINSEQ_1:def 3;
1 <= 1 + 1 & 1 + 1 <= len p by A6,NAT_1:38;
then 1 + 1 in Seg(len p) by FINSEQ_1:3;
then 1 + 1 in dom p by FINSEQ_1:def 3;
then [f,q] in R by A2,A7,REWRITE1:def 2;
then consider h',g' being set such that
A8: [f,q] = [h',g'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
g' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
A9: h' in the carrier of Polynom-Ring(n,L) by A8,XBOOLE_0:def 4;
f = [h',g']`1 by A8,MCART_1:def 1 .= h' by MCART_1:def 1;
hence f is Polynomial of n,L by A9,POLYNOM1:def 27;
end;
hence f is Polynomial of n,L;
now per cases;
case len p = 1;
hence g is Polynomial of n,L by A1,A2;
case len p <> 1;
then 1 < len p by A3,REAL_1:def 5;
then 1 + -1 < len p + -1 by REAL_1:67;
then 1 - 1 < len p - 1 by XCMPLX_0:def 8;
then 0 + 1 < l + 1 by REAL_1:67;
then 1 <= l & l <= l + 1 by NAT_1:38;
then l in Seg(len p) by A4,FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A2,A4,A5,REWRITE1:def 2;
then consider h',g' being set such that
A10: [h,g] = [h',g'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
g' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
g = [h',g']`2 by A10,MCART_1:def 2 .= g' by MCART_1:def 2;
hence g is Polynomial of n,L by A10,POLYNOM1:def 27;
end;
hence g is Polynomial of n,L;
end;
theorem
for n being Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 by Def4;
then PolyRedRel(G,T) is confluent by Th12;
then reconsider RG = PolyRedRel(G,T) as complete Relation by REWRITE1:def 25;
for a,b being set
holds a,b are_convertible_wrt R iff a,b are_convergent_wrt RG
proof
let a,b be set;
A2: G-Ideal = P by A1,Def4;
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:39;
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 & p.len p = b by REWRITE1:def 3;
len p > 0 by REWRITE1:def 2;
then A7: 1 <= len(p) by RLVECT_1:99;
then reconsider l = len p - 1 as Nat by INT_1:18;
A8: l + 1 = (len p + -1) + 1 by XCMPLX_0:def 8
.= len p + (-1 + 1) by XCMPLX_1:1
.= len p + 0;
then 1 <= l + 1 & l + 1 <= len p by NAT_1:37;
then l + 1 in Seg(len p) by FINSEQ_1:3;
then A9: l + 1 in dom p by FINSEQ_1:def 3;
set h = p.l, g = p.(1+1);
now per cases;
case len p = 1;
hence a is Polynomial of n,L & b is Polynomial of n,L by A5,A6;
case len p <> 1;
then A10: 1 < len p by A7,REAL_1:def 5;
then 1 + -1 < len p + -1 by REAL_1:67;
then 1 - 1 < len p - 1 by XCMPLX_0:def 8;
then 0 + 1 < l + 1 by REAL_1:67;
then 1 <= l & l <= l + 1 by NAT_1:38;
then l in Seg(len p) by A8,FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then A11: [h,b] in R \/ R~ by A6,A8,A9,REWRITE1:def 2;
A12: now per cases by A11,XBOOLE_0:def 2;
case [h,b] in R;
then consider h',b' being set such that
A13: [h,b] = [h',b'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
b' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
b = [h',b']`2 by A13,MCART_1:def 2 .= b' by MCART_1:def 2;
hence b is Polynomial of n,L by A13,POLYNOM1:def 27;
case [h,b] in R~;
then [b,h] in R by RELAT_1:def 7;
then consider h',b' being set such that
A14: [b,h] = [h',b'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
b' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
A15: h' in the carrier of Polynom-Ring(n,L)
by A14,XBOOLE_0:def 4;
b = [h',b']`1 by A14,MCART_1:def 1 .= h' by MCART_1:def 1;
hence b is Polynomial of n,L by A15,POLYNOM1:def 27;
end;
1 in Seg(len p) by A7,FINSEQ_1:3;
then A16: 1 in dom p by FINSEQ_1:def 3;
1 <= 1 + 1 & 1 + 1 <= len p by A10,NAT_1:38;
then 1 + 1 in Seg(len p) by FINSEQ_1:3;
then 1 + 1 in dom p by FINSEQ_1:def 3;
then A17: [a,g] in R \/ R~ by A6,A16,REWRITE1:def 2;
now per cases by A17,XBOOLE_0:def 2;
case [a,g] in R;
then consider h',b' being set such that
A18: [a,g] = [h',b'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
b' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
A19: h' in the carrier of Polynom-Ring(n,L)
by A18,XBOOLE_0:def 4;
a = [h',b']`1 by A18,MCART_1:def 1 .= h' by MCART_1:def 1;
hence a is Polynomial of n,L by A19,POLYNOM1:def 27;
case [a,g] in R~;
then [g,a] in R by RELAT_1:def 7;
then consider h',b' being set such that
A20: [g,a] = [h',b'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
b' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
a = [h',b']`2 by A20,MCART_1:def 2 .= b' by MCART_1:def 2;
hence a is Polynomial of n,L by A20,POLYNOM1:def 27;
end;
hence a is Polynomial of n, L & b is Polynomial of n,L by A12;
end;
then reconsider a' = a, b' = b
as Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
reconsider a',b' as Element of Polynom-Ring(n,L);
G-Ideal = P-Ideal by A2,IDEAL_1:44;
then a',b' are_congruent_mod G-Ideal by A4,POLYRED:57;
then a',b' are_convertible_wrt RG by POLYRED:58;
hence a,b are_convergent_wrt RG by REWRITE1:def 23;
end;
hence a,b are_convergent_wrt RG;
end;
now assume A21: a,b are_convergent_wrt RG;
now per cases;
case a = b;
hence a,b are_convertible_wrt R by REWRITE1:27;
case A22: a <> b;
consider c being set such that
A23: RG reduces a,c & RG reduces b,c by A21,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 A22,A23,Lm6;
case A24: a <> c;
now per cases;
case b = c;
hence thesis by A22,A23,Lm6;
case b <> c;
hence b is Polynomial of n,L by A23,Lm6;
end;
hence thesis by A23,A24,Lm6;
end;
hence thesis;
end;
then reconsider a' = a, b' = b as Element of
the carrier of Polynom-Ring(n,L) by POLYNOM1:def 27;
reconsider a',b' as Element of Polynom-Ring(n,L);
A25: G-Ideal = P-Ideal by A2,IDEAL_1:44;
a',b' are_convertible_wrt RG by A21,REWRITE1:38;
then a',b' are_congruent_mod P-Ideal by A25,POLYRED:57;
hence a,b are_convertible_wrt R by POLYRED:58;
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 Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 PolyRedRel(G,T) is locally-confluent by Def3;
then PolyRedRel(G,T) is confluent by Th12;
then A1: PolyRedRel(G,T) is with_UN_property by Th13;
A2: now assume p,q are_congruent_mod G-Ideal;
then p,q are_convertible_wrt PolyRedRel(G,T) by POLYRED:58;
hence nf(p,PolyRedRel(G,T)) = nf(q,PolyRedRel(G,T)) by A1,REWRITE1:56;
end;
now assume A3: nf(p,PolyRedRel(G,T)) = nf(q,PolyRedRel(G,T));
nf(p,R) is_a_normal_form_of p,R & nf(q,R) is_a_normal_form_of q,R
by A1,REWRITE1:55;
then R reduces p,nf(p,R) & R reduces q,nf(q,R) by REWRITE1:def 6;
then p,nf(p,R) are_convertible_wrt R & nf(q,R),q are_convertible_wrt R
by REWRITE1:26;
then p,q are_convertible_wrt PolyRedRel(G,T) by A3,REWRITE1:31;
hence p,q are_congruent_mod G-Ideal by POLYRED:57;
end;
hence thesis by A2;
end;
theorem
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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)
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L);
assume P is_Groebner_basis_wrt T;
then PolyRedRel(P,T) is locally-confluent by Def3;
then PolyRedRel(P,T) is confluent by Th12;
then PolyRedRel(P,T) is with_UN_property by Th13;
then PolyRedRel(P,T) is with_Church-Rosser_property by Th14;
hence thesis by Th15,POLYRED:60;
end;
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
Field-like (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
Field-like (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;
assume A2: for f being Polynomial of n,L
st f in I holds PolyRedRel(G,T) reduces f,0_(n,L);
A3: now let u be set;
assume A4: u in G-Ideal;
G-Ideal c= I by A1,IDEAL_1:def 15;
hence u in I by A4;
end;
now let u be set;
assume A5: u in I;
then reconsider u' = u as Element of Polynom-Ring(n,L);
reconsider u' as Polynomial of n,L by POLYNOM1:def 27;
PolyRedRel(G,T) reduces u',0_(n,L) by A2,A5;
hence u in G-Ideal by POLYRED:60;
end;
hence thesis by A3,TARSKI:2;
end;
theorem Th24:
::: theorem 5.38 (o) ==> (i), p. 207
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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))
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
I being Subset of Polynom-Ring(n,L),
G be non empty Subset of Polynom-Ring(n,L);
assume G is_Groebner_basis_of I,T;
then A1: G-Ideal = I & PolyRedRel(G,T) is locally-confluent
by Def4;
then PolyRedRel(G,T) is confluent by Th12;
then PolyRedRel(G,T) is with_UN_property by Th13;
then PolyRedRel(G,T) is with_Church-Rosser_property by Th14;
hence for f being Polynomial of n,L
st f in I holds PolyRedRel(G,T) reduces f,0_(n,L) by A1,Th15;
end;
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
Field-like (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
Field-like (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 2;
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 Nat,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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 Nat,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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
let f be non-zero Polynomial of n,L;
assume A3: f in I;
set H = {g where g is non-zero Polynomial of n,L :
g in I & not(g is_top_reducible_wrt P,T)};
assume not(f is_top_reducible_wrt P,T);
then A4: f in H by A3;
now let u be set;
assume u in H;
then consider g' being non-zero Polynomial of n,L such that
A5: u = g' & g' in I & not(g' is_top_reducible_wrt P,T);
thus u in the carrier of Polynom-Ring(n,L) by A5;
end;
then H c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
then reconsider H as non empty Subset of Polynom-Ring(n,L)
by A4;
consider p being Polynomial of n,L such that
A6: p in H &
for q being Polynomial of n,L st q in H holds p <= q,T
by POLYRED:31;
consider p' being non-zero Polynomial of n,L such that
A7: p' = p & p' in I & not(p' is_top_reducible_wrt P,T) by A6;
reconsider p as non-zero Polynomial of n,L by A7;
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 & p reduces_to q,u,T by A8,POLYRED:def 7;
consider b being bag of n such that
A10: p reduces_to q,u,b,T by A9,POLYRED:def 6;
A11: u <> 0_(n,L) by A10,POLYRED:def 5;
then reconsider u as non-zero Polynomial of n,L by POLYNOM7:def 2;
A12: q < p,T by A9,POLYRED:43;
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 27;
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 A14: pp + -(mm * uu) in I by A7,IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 27;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then A15: q in I by A13,A14,RLVECT_1:def 11;
A16: p <> 0_(n,L) by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A17: HT(p,T) in Support p by TERMORD:def 6;
consider b being bag of n such that
A18: p reduces_to q,u,b,T by A9,POLYRED:def 6;
b in Support p by A18,POLYRED:def 5;
then A19: b <= HT(p,T),T by TERMORD:def 6;
now assume b = HT(p,T);
then p top_reduces_to q,u,T by A18,POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A7,A9,POLYRED:def 12;
end;
then b < HT(p,T),T by A19,TERMORD:def 3;
then A20: HT(p,T) in Support q by A17,A18,POLYRED:40;
now per cases;
case A21: q <> 0_(n,L);
then reconsider q as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support q <> {} by A21,POLYNOM7:1;
then A22: HT(q,T) in Support q by TERMORD:def 6;
A23: HT(p,T) <= HT(q,T),T by A20,TERMORD:def 6;
HT(q,T) <= HT(p,T),T by A9,A22,POLYRED:42;
then A24: HT(q,T) = HT(p,T) by A23,TERMORD:7;
now assume not(q is_top_reducible_wrt P,T);
then q in H by A15;
then p <= q,T by A6;
hence contradiction by A12,POLYRED:29;
end;
then consider u' being Polynomial of n,L such that
A25: u' in P & q is_top_reducible_wrt u',T by POLYRED:def 12;
consider q' being Polynomial of n,L such that
A26: q top_reduces_to q',u',T by A25,POLYRED:def 11;
A27: q reduces_to q',u',HT(q,T),T by A26,POLYRED:def 10;
then A28: q <> 0_(n,L) & u' <> 0_(n,L) &
HT(q,T) in Support q &
ex s being bag of n
st s + HT(u',T) = HT(q,T) &
q' = q - (q.(HT(q,T))/HC(u',T)) * (s *' u')
by POLYRED:def 5;
consider s being bag of n such that
A29: s + HT(u',T) = HT(q,T) &
q' = q - (q.(HT(q,T))/HC(u',T)) * (s *' u') by A27,POLYRED:def 5;
set qq = p - (p.(HT(p,T))/HC(u',T)) * (s *' u');
A30: p <> 0_(n,L) by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then HT(p,T) in Support p by TERMORD:def 6;
then p reduces_to qq,u',HT(p,T),T by A24,A28,A29,A30,POLYRED:def 5;
then p top_reduces_to qq,u',T by POLYRED:def 10;
then p is_top_reducible_wrt u',T by POLYRED:def 11;
hence contradiction by A7,A25,POLYRED:def 12;
case q = 0_(n,L);
then A31: m *' u = (p - m *' u) + m *' u by A13,POLYRED:2
.= (p + -(m *' u)) + m *' u by POLYNOM1:def 23
.= p + (-(m *' u) + m *' u) by POLYNOM1:80
.= p + 0_(n,L) by POLYRED:3
.= p by POLYNOM1:82;
now assume A32: m = 0_(n,L);
p <> 0_(n,L) by POLYNOM7:def 2;
hence contradiction by A31,A32,POLYRED:5;
end;
then reconsider m as non-zero Polynomial of n,L by POLYNOM7:def 2;
A33: HT(p,T) = HT(m,T) + HT(u,T) by A31,TERMORD:31;
set pp = p - (p.(HT(p,T))/HC(u,T)) * (HT(m,T) *' u);
p reduces_to pp,u,HT(p,T),T by A11,A16,A17,A33,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;
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
Field-like (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 b' being bag of n st b' in HT(G,T) & b' 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
Field-like (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 b in {HT(p,T) where p is Polynomial of n,L :
p in I & p <> 0_(n,L)} by Def1;
then consider p being Polynomial of n,L such that
A2: b = HT(p,T) & p in I & p <> 0_(n,L);
reconsider p as non-zero Polynomial of n,L by A2,POLYNOM7:def 2;
p is_top_reducible_wrt P,T by A1,A2;
then consider u being Polynomial of n,L such that
A3: u in P & p is_top_reducible_wrt u,T by POLYRED:def 12;
consider q being Polynomial of n,L such that
A4: p top_reduces_to q,u,T by A3,POLYRED:def 11;
A5: p reduces_to q,u,HT(p,T),T by A4,POLYRED:def 10;
then consider s being bag of n such that
A6: s + HT(u,T) = HT(p,T) & q = p - (p.(HT(p,T))/HC(u,T)) * (s *' u)
by POLYRED:def 5;
u <> 0_(n,L) by A5,POLYRED:def 5;
then HT(u,T) in {HT(r,T) where r is Polynomial of n,L :
r in P & r <> 0_(n,L)} by A3;
then A7: HT(u,T) in HT(P,T) by Def1;
HT(u,T) divides b by A2,A6,POLYNOM1:54;
hence ex b' being bag of n st b' in HT(P,T) & b' divides b by A7;
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
Field-like (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 b' being bag of n st b' in HT(G,T) & b' 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
Field-like (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 b' being bag of n st b' in HT(P,T) & b' divides b;
now let u be set;
assume A2: u in HT(I,T);
then u in {HT(p,T) where p is Polynomial of n,L :
p in I & p <> 0_(n,L)} by Def1;
then consider p being Polynomial of n,L such that
A3: u = HT(p,T) & p in I & p <> 0_(n,L);
reconsider u' = u as Element of Bags n by A3;
consider b' being bag of n such that
A4: b' in HT(P,T) & b' divides u' by A1,A2;
u' in { b where b is Element of Bags n :
ex b' being bag of n st b' in HT(P,T) & b' divides b} by A4;
hence u in multiples(HT(P,T)) by Def2;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th29:
::: theorem 5.38 (v) ==> (o), p. 207
for n being Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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;
then A2: PolyRedRel(P,T) c= PolyRedRel(I,T) by Th4;
assume A3: HT(I,T) c= multiples(HT(P,T));
set R = PolyRedRel(P,T);
A4: 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 A5: f in I & f <> 0_(n,L);
then HT(f,T) in
{HT(p,T) where p is Polynomial of n,L : p in I & p <> 0_(n,L)};
then HT(f,T) in HT(I,T) by Def1;
then HT(f,T) in multiples(HT(P,T)) by A3;
then HT(f,T) in {b where b is Element of Bags n :
ex b' being bag of n st b' in HT(P,T) & b' divides b } by Def2;
then consider b being Element of Bags n such that
A6: b = HT(f,T) & ex b' being bag of n st b' in HT(P,T) & b' divides b;
consider b' being bag of n such that
A7: b' in HT(P,T) & b' divides HT(f,T) by A6;
b' in {HT(p,T) where p is Polynomial of n,L : p in P & p <> 0_(n,L)}
by A7,Def1;
then consider p being Polynomial of n,L such that
A8: b' = HT(p,T) & p in P & p <> 0_(n,L);
consider s being bag of n such that
A9: b' + 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,A9,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;
A10: 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 A11: f in I;
per cases;
suppose f = 0_(n,L);
hence thesis by REWRITE1:13;
suppose A12: f <> 0_(n,L);
assume A13: not(R reduces f,0_(n,L));
f is_reducible_wrt P,T by A4,A11,A12;
then consider v being Polynomial of n,L such that
A14: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in R by A14,POLYRED:def 13;
then f in field R by RELAT_1:30;
then f has_a_normal_form_wrt R by REWRITE1:def 14;
then consider g being set such that
A15: g is_a_normal_form_of f,R by REWRITE1:def 11;
A16: g is_a_normal_form_wrt R & R reduces f,g by A15,REWRITE1:def 6;
then A17: PolyRedRel(I,T) reduces f,g by A2,REWRITE1:23;
A18: g <> 0_(n,L) by A13,A15,REWRITE1:def 6;
reconsider g' = g as Polynomial of n,L by A16,Lm4;
reconsider ff = f, gg = g' as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider ff,gg as Element of Polynom-Ring(n,L);
f - g' = ff - gg by Lm2;
then ff - gg in I-Ideal by A17,POLYRED:59;
then ff - gg in I by IDEAL_1:44;
then A19: (ff - gg) - ff in I by A11,IDEAL_1:16;
(ff - gg) - ff = (ff + -gg) - ff by RLVECT_1:def 11
.= (ff + -gg) + -ff by RLVECT_1:def 11
.= (ff + -ff) + -gg by RLVECT_1:def 6
.= 0.(Polynom-Ring(n,L)) + -gg by RLVECT_1:16
.= - gg by ALGSTR_1:def 5;
then --gg in I by A19,IDEAL_1:14;
then g in I by RLVECT_1:30;
then g' is_reducible_wrt P,T by A4,A18;
then consider u being Polynomial of n,L such that
A20: g' reduces_to u,P,T by POLYRED:def 9;
[g',u] in R by A20,POLYRED:def 13;
hence contradiction by A16,REWRITE1:def 5;
end;
then A21: P-Ideal = I by A1,Lm7;
now let a,b,c being set;
assume A22: [a,b] in R & [a,c] in R;
then consider a',b' being set such that
A23: a' in ((the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}) &
b' in the carrier of Polynom-Ring(n,L) &
[a,b] = [a',b'] by ZFMISC_1:def 2;
A24: b' = [a,b]`2 by A23,MCART_1:def 2 .= b by MCART_1:def 2;
consider aa,c' being set such that
A25: aa in ((the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}) &
c' in the carrier of Polynom-Ring(n,L) &
[a,c] = [aa,c'] by A22,ZFMISC_1:def 2;
A26: c' = [a,c]`2 by A25,MCART_1:def 2 .= c by MCART_1:def 2;
reconsider b', c' as Polynomial of n,L by A23,A25,POLYNOM1:def 27;
reconsider bb = b', cc = c' as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider bb,cc as Element of Polynom-Ring(n,L);
A27: b' - c' = bb - cc by Lm2;
a,b are_convertible_wrt R & a,c are_convertible_wrt R by A22,REWRITE1:30;
then b,a are_convertible_wrt R & a,c are_convertible_wrt R by REWRITE1:32;
then b,c are_convertible_wrt R by REWRITE1:31;
then bb,cc are_congruent_mod I by A21,A24,A26,POLYRED:57;
then bb - cc in I by POLYRED:def 14;
then PolyRedRel(P,T) reduces b'-c',0_(n,L) by A10,A27;
hence b,c are_convergent_wrt R by A24,A26,POLYRED:50;
end;
then PolyRedRel(P,T) is locally-confluent by REWRITE1:def 24;
hence thesis by A21,Def4;
end;
begin :: Existence of Groebner Bases
theorem Th30:
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (non trivial doubleLoopStr)
holds {0_(n,L)} is_Groebner_basis_of {0_(n,L)},T
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (non trivial doubleLoopStr);
set I = {0_(n,L)}, G = {0_(n,L)}, R = PolyRedRel(G,T);
now let a,b,c be set;
assume A1: [a,b] in R & [a,c] in R;
then consider p,q being set such that
A2: p in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
q in the carrier of Polynom-Ring(n,L) & [a,b] = [p,q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A2,POLYNOM1:def 27;
A3: p in the carrier of Polynom-Ring(n,L) by A2,XBOOLE_0:def 4;
not(p in {0_(n,L)}) by A2,XBOOLE_0:def 4;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L
by A3,POLYNOM1:def 27,POLYNOM7:def 2;
p reduces_to q,G,T by A1,A2,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A4: g in G & p reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A4,TARSKI:def 1;
then p is_reducible_wrt 0_(n,L),T by A4,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
then A5: PolyRedRel(G,T) is locally-confluent by REWRITE1:def 24;
0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then {0_(n,L)} is Ideal of Polynom-Ring(n,L) by IDEAL_1:7;
then G-Ideal = I by IDEAL_1:44;
hence thesis by A5,Def4;
end;
theorem
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (non trivial doubleLoopStr),
p being Polynomial of n,L
holds {p} is_Groebner_basis_of {p}-Ideal,T
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like (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 27;
then {0_(n,L)} is Ideal of Polynom-Ring(n,L) by IDEAL_1:7;
then {p}-Ideal = {0_(n,L)} by A1,IDEAL_1:44;
hence thesis by A1,Th30;
suppose p <> 0_(n,L);
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 2;
PolyRedRel({p},T) is locally-confluent by Th10;
hence thesis by Def4;
end;
theorem
for T being admissible connected TermOrder of {},
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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
let T be admissible connected TermOrder of {},
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like 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 A1: P c= I & P <> {0_({},L)};
now assume A2: {i where i is Nat: i < 0} <> {};
consider j being Element of {i where i is Nat: i < 0};
j in {i where i is Nat: i < 0} by A2;
then consider i being Nat such that
A3: i = j & i < 0;
thus contradiction by A3,NAT_1:18;
end;
then reconsider n = {} as Nat;
reconsider I as add-closed left-ideal non empty Subset of Polynom-Ring(n,L);
reconsider P as non empty Subset of Polynom-Ring(n,L);
reconsider T as admissible connected TermOrder of n;
A4: ex q being Element of P st q <> 0_(n,L)
proof
assume A5: not(ex q being Element of P st q <> 0_(n,L));
A6: now let u be set;
assume u in P;
then u = 0_(n,L) by A5;
hence u in {0_(n,L)} by TARSKI:def 1;
end;
now let u be set;
assume u in {0_(n,L)};
then A7: u = 0_(n,L) by TARSKI:def 1;
now assume not(u in P);
then for v being set holds not(v in P) by A5,A7;
hence thesis by XBOOLE_0:def 1;
end;
hence u in P;
end;
hence thesis by A1,A6,TARSKI:2;
end;
now let f be non-zero Polynomial of n,L;
assume f in I;
consider p being Element of P such that
A8: p <> 0_(n,L) by A4;
reconsider p as Polynomial of n,L by POLYNOM1:def 27;
reconsider p as non-zero Polynomial of n,L by A8,POLYNOM7:def 2;
A9: HT(p,T) = EmptyBag n by POLYNOM7:3;
f <> 0_(n,L) by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then HT(f,T) in Support f by TERMORD:def 6;
then EmptyBag n in Support f by POLYNOM7:3;
then f is_reducible_wrt p,T by A9,POLYRED:36;
then consider g being Polynomial of n,L such that
A10: f reduces_to g,p,T by POLYRED:def 8;
f reduces_to g,P,T by A10,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 b' being bag of n st b' in HT(P,T) & b' 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
Field-like 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
Field-like non degenerated (non empty doubleLoopStr);
set 1bag = (EmptyBag n)+*({},1);
reconsider 1bag as Element of Bags n by POLYNOM1:def 14;
A1: {} in n by ORDINAL1:24;
dom EmptyBag n = n by PBOOLE:def 3;
then 1bag.{} = 1 by A1,FUNCT_7:33;
then A2: EmptyBag n <> 1bag by POLYNOM1:56;
set p = (1.L _(n,L))+*(1bag,1.L);
reconsider p as Function of Bags n,L;
reconsider p as Series of n,L;
1.L = 1_ L by POLYNOM2:3;
then A3: 1.L <> 0.L by VECTSP_1:def 21;
A4: dom(1.L _(n,L)) = Bags n by FUNCT_2:def 1;
then A5: p.(1bag) = 1.L by FUNCT_7:33;
then A6: p <> 0_(n,L) by A3,POLYNOM1:81;
A7: p.(EmptyBag n) = (1.L _(n,L)).(EmptyBag n) by A2,FUNCT_7:34
.= (1_(n,L)).(EmptyBag n) by POLYNOM7:20
.= 1.L by POLYNOM1:84;
A8: now let u be bag of n;
assume A9: u <> EmptyBag n & u <> 1bag;
then p.u = (1.L _(n,L)).u by FUNCT_7:34;
then p.u = (1_(n,L)).u by POLYNOM7:20;
hence p.u = 0.L by A9,POLYNOM1:84;
end;
A10: now let u be set;
assume A11: u in {EmptyBag n,1bag};
now per cases by A11,TARSKI:def 2;
case u = EmptyBag n;
hence u in Support p by A3,A7,POLYNOM1:def 9;
case u = 1bag;
hence u in Support p by A3,A5,POLYNOM1:def 9;
end;
hence u in Support p;
end;
now let u' be set;
assume A12: u' in Support p;
then reconsider u = u' as Element of Bags n;
A13: p.u <> 0.L by A12,POLYNOM1:def 9;
now assume not(u in {EmptyBag n,1bag});
then u <> EmptyBag n & u <> 1bag by TARSKI:def 2;
hence contradiction by A8,A13;
end;
hence u' in {EmptyBag n,1bag};
end;
then A14: Support p = {EmptyBag n,1bag} by A10,TARSKI:2;
then reconsider p as Polynomial of n,L by POLYNOM1:def 10;
reconsider p as non-zero Polynomial of n,L by A6,POLYNOM7:def 2;
set q = (0.L _(n,L))+*(1bag,1.L);
reconsider q as Function of Bags n,L;
reconsider q as Series of n,L;
1.L = 1_ L by POLYNOM2:3;
then A15: 1.L <> 0.L by VECTSP_1:def 21;
dom(0.L _(n,L)) = Bags n by FUNCT_2:def 1;
then A16: q.(1bag) = 1.L by FUNCT_7:33;
then A17: q <> 0_(n,L) by A15,POLYNOM1:81;
A18: q.(EmptyBag n) = (0.L _(n,L)).(EmptyBag n) by A2,FUNCT_7:34
.= (0_(n,L)).(EmptyBag n) by POLYNOM7:19
.= 0.L by POLYNOM1:81;
A19: now let u be bag of n;
assume u <> 1bag;
then q.u = (0.L _(n,L)).u by FUNCT_7:34;
then q.u = (0_(n,L)).u by POLYNOM7:19;
hence q.u = 0.L by POLYNOM1:81;
end;
A20: now let u be set;
assume u in {1bag};
then u = 1bag by TARSKI:def 1;
hence u in Support q by A15,A16,POLYNOM1:def 9;
end;
now let u' be set;
assume A21: u' in Support q;
then reconsider u = u' as Element of Bags n;
A22: q.u <> 0.L by A21,POLYNOM1:def 9;
now assume not(u in {1bag});
then u <> 1bag by TARSKI:def 1;
hence contradiction by A19,A22;
end;
hence u' in {1bag};
end;
then A23: Support q = {1bag} by A20,TARSKI:2;
then reconsider q as Polynomial of n,L by POLYNOM1:def 10;
reconsider q as non-zero Polynomial of n,L by A17,POLYNOM7:def 2;
Support p <> {} by A6,POLYNOM7:1;
then A24: HT(p,T) in Support p by TERMORD:def 6;
A25: now assume A26: HT(p,T) = EmptyBag n;
1bag in Support p by A14,TARSKI:def 2;
then A27: 1bag <= EmptyBag n,T by A26,TERMORD:def 6;
EmptyBag n <= 1bag,T by TERMORD:9;
hence contradiction by A2,A27,TERMORD:7;
end;
then A28: HT(p,T) = 1bag by A14,A24,TARSKI:def 2;
Support q <> {} by A17,POLYNOM7:1;
then A29: HT(q,T) in Support q by TERMORD:def 6;
set P = {p,q};
now let u be set;
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 27;
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;
set p1 = q - (q.HT(p,T)/HC(p,T)) * ((EmptyBag n) *' p);
A30: HT(p,T) in Support q by A23,A28,TARSKI:def 1;
EmptyBag n + HT(p,T) = HT(p,T) by POLYNOM1:57;
then q reduces_to p1,p,HT(p,T),T by A6,A17,A30,POLYRED:def 5;
then A31: q reduces_to p1,p,T by POLYRED:def 6;
A32: p1 = q - (1.L/p.1bag) * ((EmptyBag n) *' p)
by A16,A28,TERMORD:def 7
.= q - (1.L/1.L) * ((EmptyBag n) *' p) by A4,FUNCT_7:33
.= q - (1.L*(1.L)") * ((EmptyBag n) *' p) by VECTSP_1:def 23
.= q - 1_ L * ((EmptyBag n) *' p) by A15,VECTSP_1:def 22
.= q - 1_ L * p by POLYRED:17
.= q - 1.L * p by POLYNOM2:3
.= q - (1.L) _(n,L) *' p by POLYNOM7:27
.= q - 1_(n,L) *' p by POLYNOM7:20
.= q - p by POLYNOM1:89;
p in P by TARSKI:def 2;
then q reduces_to q-p,P,T by A31,A32,POLYRED:def 7;
then A33: [q,q-p] in R by POLYRED:def 13;
set q1 = q - (q.HT(q,T)/HC(q,T)) * ((EmptyBag n) *' q);
EmptyBag n + HT(q,T) = HT(q,T) by POLYNOM1:57;
then q reduces_to q1,q,HT(q,T),T by A17,A29,POLYRED:def 5;
then A34: q reduces_to q1,q,T by POLYRED:def 6;
A35: HC(q,T) <> 0.L by A17,TERMORD:17;
A36: 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) by VECTSP_1:def 23
.= q - 1_ L * ((EmptyBag n) *' q) by A35,VECTSP_1:def 22
.= q - 1_ L * q by POLYRED:17
.= q - 1.L * q by POLYNOM2:3
.= q - (1.L) _(n,L) *' q by POLYNOM7:27
.= q - 1_(n,L) *' q by POLYNOM7:20
.= q - q by POLYNOM1:89
.= 0_(n,L) by POLYNOM1:83;
q in P by TARSKI:def 2;
then q reduces_to 0_(n,L),P,T by A34,A36,POLYRED:def 7;
then A37: [q,0_(n,L)] in R by POLYRED:def 13;
A38: now assume Support q = Support p;
then EmptyBag n in {1bag} by A14,A23,TARSKI:def 2;
hence contradiction by A2,TARSKI:def 1;
end;
A39: now assume q - p = 0_(n,L);
then p = (q-p)+p by POLYRED:2
.= (q+-p)+p by POLYNOM1:def 23
.= q+(-p+p) by POLYNOM1:80
.= q + 0_(n,L) by POLYRED:3;
hence contradiction by A38,POLYNOM1:82;
end;
now assume R is locally-confluent;
then 0_(n,L),q-p are_convergent_wrt R by A33,A37,REWRITE1:def 24;
then consider c being set such that
A40: R reduces 0_(n,L),c & R reduces q-p,c by REWRITE1:def 7;
reconsider c as Polynomial of n,L by A40,Lm4;
consider s being FinSequence such that
A41: len s > 0 & s.1 = 0_(n,L) & s.len s = c &
for i being Nat st i in dom s & i+1 in dom s holds [s.i, s.(i+1)] in R
by A40,REWRITE1:12;
A42: now assume A43: len s <> 1;
A44: 0 + 1 <= len s by A41,NAT_1:38;
then 1 < len s by A43,REAL_1:def 5;
then A45: 1+1 <= len s by NAT_1:38;
A46: dom s = Seg(len s) by FINSEQ_1:def 3;
then A47: 1 in dom s by A44,FINSEQ_1:3;
1+1 in dom s by A45,A46,FINSEQ_1:3;
then A48: [s.1,s.2] in R by A41,A47;
then consider f',h' being set such that
A49: [0_(n,L),s.2] = [f',h'] &
f' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
h' in (the carrier of Polynom-Ring(n,L)) by A41,RELSET_1:6;
s.2 = [f',h']`2 by A49,MCART_1:def 2 .= h' by MCART_1:def 2;
then reconsider c' = s.2 as Polynomial of n,L by A49,POLYNOM1:def 27;
0_(n,L) reduces_to c',P,T by A41,A48,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A50: g in P & 0_(n,L) reduces_to c',g,T by POLYRED:def 7;
0_(n,L) is_reducible_wrt g,T by A50,POLYRED:def 8;
hence contradiction by POLYRED:37;
end;
A51: now assume -1.L = 0.L;
then --1.L = 0.L by RLVECT_1:25;
hence contradiction by A15,RLVECT_1:30;
end;
A52: now let u be set;
assume A53: u in {EmptyBag n};
then reconsider u' = u as Element of Bags n by TARSKI:def 1;
(q-p).u' = (q+-p).u' by POLYNOM1:def 23
.= q.u' + (-p).u' by POLYNOM1:def 21
.= q.u' + -(p.u') by POLYNOM1:def 22
.= 0.L + -(p.u') by A18,A53,TARSKI:def 1
.= 0.L + -1.L by A7,A53,TARSKI:def 1
.= -1.L by ALGSTR_1:def 5;
hence u in Support(q-p) by A51,POLYNOM1:def 9;
end;
now let u be set;
assume A54: u in Support(q-p);
then A55: (q-p).u <> 0.L by POLYNOM1:def 9;
Support(q-p) = Support (q+-p) by POLYNOM1:def 23;
then Support(q-p) c= Support(q) \/ Support(-p) by POLYNOM1:79;
then A56: Support(q-p) c= {1bag} \/ {EmptyBag n,1bag} by A14,A23,Th5;
now let u be set;
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} by TARSKI:def 3;
then A57: {1bag} \/ {EmptyBag n,1bag} = {EmptyBag n,1bag} by XBOOLE_1:12;
(q-p).1bag = (q+-p).1bag by POLYNOM1:def 23
.= q.1bag + (-p).1bag by POLYNOM1:def 21
.= q.1bag + -(p.1bag) by POLYNOM1:def 22
.= 1.L + -1.L by A4,A16,FUNCT_7:33
.= 0.L by RLVECT_1:16;
then u = EmptyBag n by A54,A55,A56,A57,TARSKI:def 2;
hence u in {EmptyBag n} by TARSKI:def 1;
end;
then A58: Support(q-p) = {EmptyBag n} by A52,TARSKI:2;
A59: now assume q-p is_reducible_wrt P,T;
then consider g being Polynomial of n,L such that
A60: q-p reduces_to g,P,T by POLYRED:def 9;
consider h being Polynomial of n,L such that
A61: h in P & q-p reduces_to g,h,T by A60,POLYRED:def 7;
consider b being bag of n such that
A62: q-p reduces_to g,h,b,T by A61,POLYRED:def 6;
q-p <> 0_(n,L) & h <> 0_(n,L) &
b in Support(q-p) &
ex s being bag of n
st s + HT(h,T) = b & g = (q-p) - ((q-p).b/HC(h,T)) * (s *' h)
by A62,POLYRED:def 5;
then reconsider h as non-zero Polynomial of n,L by POLYNOM7:def 2;
q-p is_reducible_wrt h,T by A61,POLYRED:def 8;
then consider b' being bag of n such that
A63: b' in Support(q-p) & HT(h,T) divides b' by POLYRED:36;
A64: b' = EmptyBag n by A58,A63,TARSKI:def 1;
HT(h,T) = 1bag
proof
now per cases by A61,TARSKI:def 2;
case h = p;
hence thesis by A14,A24,A25,TARSKI:def 2;
case h = q;
hence thesis by A23,A29,TARSKI:def 1;
end;
hence thesis;
end;
hence contradiction by A2,A63,A64,POLYNOM1:62;
end;
consider s being FinSequence such that
A65: len s > 0 & s.1 = q-p & s.len s = 0_(n,L) &
for i being Nat st i in dom s & i+1 in dom s holds [s.i, s.(i+1)] in R
by A40,A41,A42,REWRITE1:12;
now assume A66: len s <> 1;
A67: 0 + 1 <= len s by A65,NAT_1:38;
then 1 < len s by A66,REAL_1:def 5;
then A68: 1+1 <= len s by NAT_1:38;
A69: dom s = Seg(len s) by FINSEQ_1:def 3;
then A70: 1 in dom s by A67,FINSEQ_1:3;
1+1 in dom s by A68,A69,FINSEQ_1:3;
then A71: [q-p,s.2] in R by A65,A70;
then consider f',h' being set such that
A72: [q-p,s.2] = [f',h'] &
f' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
h' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
s.2 = [f',h']`2 by A72,MCART_1:def 2 .= h' by MCART_1:def 2;
then reconsider c' = s.2 as Polynomial of n,L by A72,POLYNOM1:def 27;
q-p reduces_to c',P,T by A71,POLYRED:def 13;
hence contradiction by A59,POLYRED:def 9;
end;
hence contradiction by A39,A65;
end;
hence thesis by Def3;
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 set;
b1.k <= b2.k & b2.k <= b3.k by A1,POLYNOM1:def 13;
hence b1.k <= b3.k by AXIOMS:22;
end;
hence thesis by POLYNOM1:def 13;
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[set,set] 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 set holds [x,y] in BO iff
x in Bags n & y in Bags n & P[x,y] from Rel_On_Set_Ex;
A2: BO is_reflexive_in Bags n
proof
let x be set;
assume x in Bags n;
hence thesis by A1;
end;
A3: BO is_antisymmetric_in Bags n
proof
let x,y be set;
assume A4: x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO;
then consider b11, b22 being Element of Bags n such that
A5: x = b11 & y = b22 & b11 divides b22 by A1;
consider b1', b2' being Element of Bags n such that
A6: y = b1' & x = b2' & b1' divides b2' by A1,A4;
reconsider b11, b22 as bag of n;
A7: dom b11 = n by PBOOLE:def 3 .= dom b22 by PBOOLE:def 3;
now let k be set;
assume k in dom b11;
A8: b11.k <= b22.k by A5,POLYNOM1:def 13;
b1'.k <= b2'.k by A6,POLYNOM1:def 13;
hence b11.k = b22.k by A5,A6,A8,AXIOMS:21;
end;
hence x = y by A5,A7,FUNCT_1:9;
end;
A9: BO is_transitive_in Bags n
proof
let x,y,z be set such that
x in Bags n & y in Bags n & z in Bags n and
A10: [x,y] in BO & [y,z] in BO;
consider b1,b2 being Element of Bags n such that
A11: x = b1 & y = b2 & b1 divides b2 by A1,A10;
consider b11, b22 being Element of Bags n such that
A12: y = b11 & z = b22 & b11 divides b22 by A1,A10;
reconsider B1 = b1, B2' = b22 as bag of n;
B1 divides B2' by A11,A12,Lm8;
hence [x,z] in BO by A1,A11,A12;
end;
A13: dom BO = Bags n & field BO = Bags n by A2,ORDERS_1:98;
then BO is total by PARTFUN1:def 4;
then reconsider BO as Order of Bags n
by A2,A3,A9,A13,RELAT_2:def 9,def 12,def 16;
take BO;
let p, q be bag of n;
A14: p in Bags n & q in Bags n by POLYNOM1:def 14;
hereby assume [p, q] in BO;
then consider b1', b2' being Element of Bags n such that
A15: p = b1' & q = b2' & b1' divides b2' by A1;
thus p divides q by A15;
end;
thus p divides q implies [p,q] in BO by A1,A14;
end;
uniqueness
proof
let B1, B2 be Order of Bags n such that
A16: for p,q being bag of n holds [p, q] in B1 iff p divides q and
A17: for p,q being bag of n holds [p, q] in B2 iff p divides q;
let a, b be set;
hereby assume
A18: [a,b] in B1;
then consider b1, b2 being set such that
A19: [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n by RELSET_1:6;
reconsider b1, b2 as bag of n by A19,POLYNOM1:def 14;
b1 divides b2 by A16,A18,A19;
hence [a,b] in B2 by A17,A19;
end;
assume A20: [a,b] in B2;
then consider b1, b2 being set such that
A21: [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n by RELSET_1:6;
reconsider b1, b2 as bag of n by A21,POLYNOM1:def 14;
b1 divides b2 by A17,A20,A21;
hence [a,b] in B1 by A16,A21;
end;
end;
definition
::: theorem 5.2, p. 189
let n be Nat;
cluster RelStr(#Bags n, DivOrder n#) -> Dickson;
coherence
proof
set P = product (n --> OrderedNAT), J = n --> OrderedNAT;
set S = product Carrier (n --> OrderedNAT), SJ = Carrier (n --> OrderedNAT);
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 A2: x in S;
let g' be Function;
assume A3: x = g';
consider g being Function such that
A4: x = g & dom g = dom SJ &
for y being set st y in dom SJ holds g.y in SJ.y by A2,CARD_3:def 5;
thus dom g' = n by A3,A4,PBOOLE:def 3;
thus for y being set st y in dom g' holds g'.y in NAT
proof
let y be set;
assume A5: y in dom g';
then A6: y in n by A3,A4,PBOOLE:def 3;
then consider R being 1-sorted such that
A7: R = J.y & SJ.y = the carrier of R by PRALG_1:def 13;
g.y in the carrier of R by A3,A4,A5,A7;
hence thesis by A3,A4,A6,A7,DICKSON:def 15,FUNCOP_1:13;
end;
end;
defpred Q[set,set] means
$1 in S & (ex b being bag of n st b = $2 & b = $1);
A8: for x,y1,y2 being set st x in S & Q[x,y1] & Q[x,y2] holds y1 = y2;
A9: for x being set st x in S ex y being set st Q[x,y]
proof
let x be set;
assume A10: x in S;
then consider g being Function such that
A11: x = g & dom g = dom SJ &
for y being set st y in dom SJ holds g.y in SJ.y
by CARD_3:def 5;
A12: x = g & dom g = n &
for y being set st y in dom g holds g.y in NAT by A1,A10,A11;
defpred QQ[set,set] means $2 = g.$1;
A13: for x,y1,y2 being set st x in n & QQ[x,y1] & QQ[x,y2]
holds y1 = y2;
A14: for x being set st x in n ex y being set st QQ[x,y];
consider b being Function such that
A15: dom b = n & for x being set st x in n holds QQ[x,b.x]
from FuncEx(A13,A14);
reconsider b as ManySortedSet of n by A15,PBOOLE:def 3;
now let u be set;
assume u in rng b;
then consider x being set such that
A16: x in dom b & u = b.x by FUNCT_1:def 5;
A17: u = g.x by A15,A16;
x in dom g by A12,A16,PBOOLE:def 3;
hence u in NAT by A1,A10,A11,A17;
end;
then rng b c= NAT by TARSKI:def 3;
then reconsider b as bag of n by SEQM_3:def 8;
take b;
thus x in S by A10;
take b;
thus b = b;
thus b = x by A12,A15,FUNCT_1:9;
end;
consider i being Function such that
A18: dom i = S & for x being set st x in S holds Q[x,i.x]
from FuncEx(A8,A9);
set R = RelStr(#Bags n, DivOrder n#);
A19: now let v be set;
assume v in rng i;
then consider u being set such that
A20: u in dom i & v = i.u by FUNCT_1:def 5;
u in S & (ex b being bag of n st b = i.u & b = u) by A18,A20;
hence v in Bags n by A20,POLYNOM1:def 14;
end;
A21: 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 by POLYNOM1:def 14;
A22: dom g = n by PBOOLE:def 3 .= dom(Carrier J) by PBOOLE:def 3;
A23: now let x be set;
assume x in dom(Carrier J);
then A24: x in n by PBOOLE:def 3;
then consider L being 1-sorted such that
A25: L = J.x & (Carrier J).x = the carrier of L by PRALG_1:def 13;
the carrier of L = NAT by A24,A25,DICKSON:def 15,FUNCOP_1:13;
hence g.x in (Carrier J).x by A25;
end;
then A26: g in product Carrier J by A22,CARD_3:def 5;
then g in the carrier of P by YELLOW_1:def 4;
then reconsider g as Element of P;
take g;
thus g in dom i by A18,A22,A23,CARD_3:def 5;
Q[g,i.g] by A18,A26;
then consider g' being Function such that
A27: g' = g & g' in S &
ex b being bag of n st b = i.g & b = g;
thus i.g = x by A27;
end;
now let N be Subset of R;
set N' = i"N;
A28: N' c= S by A18,RELAT_1:167;
then N' c= the carrier of P by YELLOW_1:def 4;
then reconsider N' as Subset of P;
consider B' being set such that
A29: B' is_Dickson-basis_of N',P & B' is finite
by DICKSON:def 10;
A30: B' c= N' &
for a being Element of P st a in N'
ex b being Element of P st b in B' & b <= a by A29,DICKSON:def 9;
set B = i.:B';
A31: B is finite by A29,FINSET_1:17;
now let u be set;
assume u in B;
then consider v being set such that
A32: v in dom i & v in B' & u = i.v by FUNCT_1:def 12;
thus u in N by A30,A32,FUNCT_1:def 13;
end;
then A33: B c= N by TARSKI:def 3;
A34: 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 A35: a = ta & b = tb & a in S;
assume a <= b;
then consider f,g being Function such that
A36: f = a & g = b &
for i be set 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 A35,YELLOW_1:def 4;
now let k be set;
assume A37: k in n;
then consider R being RelStr, ak,bk being Element of R such that
A38: R = J.k & ak = f.k & bk = g.k & ak <= bk by A36;
J.k = OrderedNAT by A37,FUNCOP_1:13;
then [ak,bk] in NATOrd by A38,DICKSON:def 15,ORDERS_1:def 9;
then consider a',b' being Nat such that
A39: [a',b'] = [ak,bk] & a' <= b' by DICKSON:def 14;
A40: a' = [ak,bk]`1 by A39,MCART_1:def 1 .= ak by MCART_1:def 1;
b' = [ak,bk]`2 by A39,MCART_1:def 2 .= bk by MCART_1:def 2;
hence ta.k <= tb.k by A35,A36,A38,A39,A40;
end;
hence thesis by POLYNOM1:50;
end;
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;
assume A41: a in N;
consider a' being Element of P such that
A42: a' in dom i & i.a' = a by A21;
A43: a' in S & (ex b being bag of n st b = i.a' & b = a') by A18,A42;
a' in N' by A41,A42,FUNCT_1:def 13;
then consider b' being Element of P such that
A44: b' in B' & b' <= a' by A29,DICKSON:def 9;
set b = i.b';
A45: B' c= S by A28,A30,XBOOLE_1:1;
then consider b1 being bag of n such that
A46: b1 = i.b' & b1 = b' by A18,A44;
b in rng i by A18,A44,A45,FUNCT_1:def 5;
then reconsider b as Element of Bags n by A19;
reconsider b as Element of R;
take b;
thus b in B by A18,A44,A45,FUNCT_1:def 12;
reconsider aa = a, bb = b as Element of Bags n;
bb divides aa by A34,A42,A43,A44,A45,A46;
then [b,a] in DivOrder(n) by Def5;
hence b <= a by ORDERS_1:def 9;
end;
then B is_Dickson-basis_of N,R by A33,DICKSON:def 9;
hence ex B being set st B is_Dickson-basis_of N,R & B is finite by A31;
end;
hence thesis by DICKSON:def 10;
end;
end;
theorem Th34:
::: theorem 5.2, p. 189
for n being 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 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#) &
B is finite by DICKSON:def 10;
now let u be set;
assume A2: u in B;
B c= N by A1,DICKSON:def 9;
hence u in N by A2;
end;
then reconsider B as finite Subset of N by A1,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 Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like 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 Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
I be add-closed left-ideal non empty Subset of Polynom-Ring(n,L);
per cases;
suppose A1: I = {0_(n,L)};
set G = {0_(n,L)}, R = PolyRedRel(G,T);
take G;
now let a,b,c be set;
assume A2: [a,b] in R & [a,c] in R;
then consider p,q being set such that
A3: p in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
q in the carrier of Polynom-Ring(n,L) & [a,b] = [p,q] by ZFMISC_1:def 2;
reconsider q as Polynomial of n,L by A3,POLYNOM1:def 27;
A4: p in the carrier of Polynom-Ring(n,L) by A3,XBOOLE_0:def 4;
not(p in {0_(n,L)}) by A3,XBOOLE_0:def 4;
then p <> 0_(n,L) by TARSKI:def 1;
then reconsider p as non-zero Polynomial of n,L
by A4,POLYNOM1:def 27,POLYNOM7:def 2;
p reduces_to q,G,T by A2,A3,POLYRED:def 13;
then consider g being Polynomial of n,L such that
A5: g in G & p reduces_to q,g,T by POLYRED:def 7;
g = 0_(n,L) by A5,TARSKI:def 1;
then p is_reducible_wrt 0_(n,L),T by A5,POLYRED:def 8;
hence b,c are_convergent_wrt R by Lm3;
end;
then A6: PolyRedRel(G,T) is locally-confluent by REWRITE1:def 24;
G-Ideal = I by A1,IDEAL_1:44;
hence thesis by A6,Def4;
suppose A7: I <> {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
A8: S is_Dickson-basis_of hti,R by Th34;
A9: S c= hti & for a being Element of R st a in hti
ex b being Element of R st b in S & b <= a
by A8,DICKSON:def 9;
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};
ex q being Element of I st q <> 0_(n,L)
proof
assume A10: not(ex q being Element of I st q <> 0_(n,L));
A11: now let u be set;
assume u in I;
then u = 0_(n,L) by A10;
hence u in {0_(n,L)} by TARSKI:def 1;
end;
now let u be set;
assume u in {0_(n,L)};
then A12: u = 0_(n,L) by TARSKI:def 1;
now assume not(u in I);
then for v being set holds not(v in I) by A10,A12;
hence thesis by XBOOLE_0:def 1;
end;
hence u in I;
end;
hence thesis by A7,A11,TARSKI:2;
end;
then consider q being Element of I such that
A13: q <> 0_(n,L);
reconsider q as Polynomial of n,L by POLYNOM1:def 27;
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 A13;
then hq in hti by Def1;
then A14: ex b being Element of R st b in S & b <= hq by A8,DICKSON:def 9;
consider s being Element of S;
s in S by A14;
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) = s' &
p <> 0_(n,L)} where s' is Element of Bags n : s' in S};
then reconsider M as non empty set;
A15: 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
A16: x = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} & s in S;
s in hti by A9,A16;
then s in {HT(p,T) where p is Polynomial of n,L :
p in I & p <> 0_(n,L)} by Def1;
then consider q being Polynomial of n,L such that
A17: s = HT(q,T) & q in I & q <> 0_(n,L);
q in x by A16,A17;
hence thesis;
end;
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 A18: x in M & y in M & x <> y;
then consider s being Element of Bags n such that
A19: x = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} & s in S;
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)} & t in S by A18;
now assume A21: x /\ y <> {};
consider u being Element of x /\ y;
A22: u in x & u in y by A21,XBOOLE_0:def 3;
then consider r being Polynomial of n,L such that
A23: u = r & r in I & HT(r,T) = s & r <> 0_(n,L) by A19;
consider v being Polynomial of n,L such that
A24: u = v & v in I & HT(v,T) = t & v <> 0_(n,L) by A20,A22;
thus contradiction by A18,A19,A20,A23,A24;
end;
hence thesis by XBOOLE_0:def 7;
end;
then consider G' being set such that
A25: for x being set st x in M
ex y being set st G' /\ x = {y} by A15,WELLORD2:27;
consider xx being Element of M;
consider y being set such that
A26: G' /\ xx = {y} by A25;
reconsider G' as non empty set by A26;
set G = { x where x is Element of G' :
ex y being set st y in M & G' /\ y = {x}};
consider xx being Element of M;
consider y being set such that
A27: G' /\ xx = {y} by A25;
now let u be set;
assume u in G;
then consider x being Element of G' such that
A28: u = x & ex y being set st y in M & G' /\ y = {x};
consider y being set such that
A29: y in M & G' /\ y = {x} by A28;
consider s being Element of Bags n such that
A30: y = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} & s in S by A29;
x in (G' /\ y) by A29,TARSKI:def 1;
then x in y by XBOOLE_0:def 3;
then consider q being Polynomial of n,L such that
A31: x = q & q in I & HT(q,T) = s & q <> 0_(n,L) by A30;
thus u in the carrier of Polynom-Ring(n,L) by A28,A31;
end;
then G c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
then reconsider G as Subset of Polynom-Ring(n,L);
A32: M is finite
proof
defpred P[set,set] means
$2 = {p where p is Polynomial of n,L : p in I & HT(p,T) = $1 &
p <> 0_(n,L)};
A33: for x,y1,y2 being set st x in S & P[x,y1] & P[x,y2] holds y1 = y2;
A34: for x being set st x in S ex y being set st P[x,y];
consider f being Function such that
A35: dom f = S & for x being set st x in S holds P[x,f.x]
from FuncEx(A33,A34);
A36: now let u be set;
assume u in M;
then consider s being Element of Bags n such that
A37: u = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} & s in S;
f.s in rng f by A35,A37,FUNCT_1:12;
hence u in rng f by A35,A37;
end;
now let u be set;
assume u in rng f;
then consider s being set such that
A38: s in dom f & u = f.s by FUNCT_1:def 5;
u = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} by A35,A38;
hence u in M by A35,A38;
end;
then rng f = M by A36,TARSKI:2;
hence thesis by A35,FINSET_1:26;
end;
defpred P[set,set] means G' /\ $1 = {$2} & $2 in G;
A39: for x,y1,y2 being set st x in M & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be set;
assume x in M & P[x,y1] & P[x,y2];
then y1 in {y2} by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
A40: for x being set st x in M ex y being set st P[x,y]
proof
let x be set;
assume A41: x in M;
then consider y being set such that
A42: G' /\ x = {y} by A25;
y in (G' /\ x) by A42,TARSKI:def 1;
then reconsider y as Element of G' by XBOOLE_0:def 3;
y in G by A41,A42;
hence thesis by A42;
end;
consider f being Function such that
A43: dom f = M & for x being set st x in M holds P[x,f.x]
from FuncEx(A39,A40);
A44: now let u be set;
assume u in G;
then consider x being Element of G' such that
A45: u = x & ex y being set st y in M & G' /\ y = {x};
consider y being set such that
A46: y in M & G' /\ y = {x} by A45;
A47: f.y in rng f by A43,A46,FUNCT_1:12;
G' /\ y = {f.y} & f.y in G by A43,A46;
then x in {f.y} by A46,TARSKI:def 1;
hence u in rng f by A45,A47,TARSKI:def 1;
end;
now let u be set;
assume u in rng f;
then consider s being set such that
A48: s in dom f & u = f.s by FUNCT_1:def 5;
thus u in G by A43,A48;
end;
then rng f = G by A44,TARSKI:2;
then reconsider G as non empty finite Subset of Polynom-Ring(n,L)
by A27,A32,A43,FINSET_1:26;
take G;
now let u be set;
assume u in G;
then consider x being Element of G' such that
A49: u = x & ex y being set st y in M & G' /\ y = {x};
consider y being set such that
A50: y in M & G' /\ y = {x} by A49;
consider s being Element of Bags n such that
A51: y = {p where p is Polynomial of n,L : p in I & HT(p,T) = s &
p <> 0_(n,L)} & s in S by A50;
x in (G' /\ y) by A50,TARSKI:def 1;
then x in y by XBOOLE_0:def 3;
then consider q being Polynomial of n,L such that
A52: x = q & q in I & HT(q,T) = s & q <> 0_(n,L) by A51;
thus u in I by A49,A52;
end;
then A53: G c= I by TARSKI:def 3;
for b being bag of n st b in HT(I,T)
ex b' being bag of n st b' in HT(G,T) & b' divides b
proof
let b be bag of n;
assume A54: b in HT(I,T);
b in Bags n by POLYNOM1:def 14;
then reconsider bb = b as Element of R;
consider bb' being Element of R such that
A55: bb' in S & bb' <= bb by A8,A54,DICKSON:def 9;
bb' is Element of Bags n;
then reconsider b' = bb' as bag of n;
take b';
A56: [bb',bb] in DivOrder(n) by A55,ORDERS_1:def 9;
set N = {p where p is Polynomial of n,L :
p in I & HT(p,T) = bb' & p <> 0_(n,L)};
A57: N in M by A55;
then consider y being set such that
A58: G' /\ N = {y} by A25;
A59: y in (G' /\ N) by