let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 11;
now for a, b, c being object st [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) holds
b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)let a,
b,
c be
object ;
( [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))},T)consider p,
q being
object such that A3:
p in NonZero (Polynom-Ring (n,L))
and A4:
q in the
carrier of
(Polynom-Ring (n,L))
and A5:
[a,b] = [p,q]
by A2, ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A4, POLYNOM1:def 11;
not
p in {(0_ (n,L))}
by A1, A3, XBOOLE_0:def 5;
then
p <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider p =
p as
non-zero Polynomial of
n,
L by A3, POLYNOM1:def 11, POLYNOM7:def 1;
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 11;
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; verum