let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds {(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T
let T be connected admissible TermOrder of n; for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds {(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; {(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T
set I = {(0_ n,L)};
set G = {(0_ n,L)};
set R = PolyRedRel {(0_ n,L)},T;
A1:
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
now let a,
b,
c be
set ;
( [a,b] in PolyRedRel {(0_ n,L)},T & [a,c] in PolyRedRel {(0_ n,L)},T implies b,c are_convergent_wrt PolyRedRel {(0_ n,L)},T )assume that A2:
[a,b] in PolyRedRel {(0_ n,L)},
T
and
[a,c] in PolyRedRel {(0_ n,L)},
T
;
b,c are_convergent_wrt PolyRedRel {(0_ n,L)},Tconsider p,
q being
set such that A3:
p in NonZero (Polynom-Ring n,L)
and A4:
q in the
carrier of
(Polynom-Ring n,L)
and A5:
[a,b] = [p,q]
by A2, ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A4, POLYNOM1:def 27;
not
p in {(0_ n,L)}
by A1, A3, XBOOLE_0:def 5;
then
p <> 0_ n,
L
by TARSKI:def 1;
then reconsider p =
p as
non-zero Polynomial of
n,
L by A3, POLYNOM1:def 27, POLYNOM7:def 2;
p reduces_to q,
{(0_ n,L)},
T
by A2, A5, POLYRED:def 13;
then consider g being
Polynomial of
n,
L such that A6:
g in {(0_ n,L)}
and A7:
p reduces_to q,
g,
T
by POLYRED:def 7;
g = 0_ n,
L
by A6, TARSKI:def 1;
then
p is_reducible_wrt 0_ n,
L,
T
by A7, POLYRED:def 8;
hence
b,
c are_convergent_wrt PolyRedRel {(0_ n,L)},
T
by Lm3;
verum end;
then A8:
PolyRedRel {(0_ n,L)},T is locally-confluent
by REWRITE1:def 24;
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
then
{(0_ n,L)} -Ideal = {(0_ n,L)}
by IDEAL_1:44;
hence
{(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T
by A8, Def4; verum