let n be Element of NAT ; :: thesis: 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; :: thesis: 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 ; :: thesis: {(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;
X:
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
now let a,
b,
c be
set ;
:: thesis: ( [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 A1:
(
[a,b] in PolyRedRel {(0_ n,L)},
T &
[a,c] in PolyRedRel {(0_ n,L)},
T )
;
:: thesis: b,c are_convergent_wrt PolyRedRel {(0_ n,L)},Tthen consider p,
q being
set such that A2:
(
p in NonZero (Polynom-Ring n,L) &
q in the
carrier of
(Polynom-Ring n,L) &
[a,b] = [p,q] )
by ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A2, POLYNOM1:def 27;
not
p in {(0_ n,L)}
by A2, X, 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 A2, POLYNOM1:def 27, POLYNOM7:def 2;
p reduces_to q,
{(0_ n,L)},
T
by A1, A2, POLYRED:def 13;
then consider g being
Polynomial of
n,
L such that A3:
(
g in {(0_ n,L)} &
p reduces_to q,
g,
T )
by POLYRED:def 7;
g = 0_ n,
L
by A3, TARSKI:def 1;
then
p is_reducible_wrt 0_ n,
L,
T
by A3, POLYRED:def 8;
hence
b,
c are_convergent_wrt PolyRedRel {(0_ n,L)},
T
by Lm3;
:: thesis: verum end;
then A4:
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)} is Ideal of (Polynom-Ring n,L)
;
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 A4, Def4; :: thesis: verum