let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
let G be Subset of (Polynom-Ring (n,L)); ( G is_Groebner_basis_wrt T implies for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) )
assume A1:
G is_Groebner_basis_wrt T
; for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
set R = PolyRedRel (G,T);
A2:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
per cases
( G = {} or G <> {} )
;
suppose
G <> {}
;
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)then reconsider G =
G as non
empty Subset of
(Polynom-Ring (n,L)) ;
A3:
PolyRedRel (
G,
T) is
locally-confluent
by A1, GROEB_1:def 3;
now for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)A4:
now 0_ (n,L) is_a_normal_form_wrt PolyRedRel (G,T)assume
not
0_ (
n,
L)
is_a_normal_form_wrt PolyRedRel (
G,
T)
;
contradictionthen consider b being
object such that A5:
[(0_ (n,L)),b] in PolyRedRel (
G,
T)
by REWRITE1:def 5;
consider f1,
f2 being
object such that A6:
f1 in NonZero (Polynom-Ring (n,L))
and
f2 in the
carrier of
(Polynom-Ring (n,L))
and A7:
[(0_ (n,L)),b] = [f1,f2]
by A5, ZFMISC_1:def 2;
A8:
f1 = 0_ (
n,
L)
by A7, XTUPLE_0:1;
not
f1 in {(0_ (n,L))}
by A2, A6, XBOOLE_0:def 5;
hence
contradiction
by A8, TARSKI:def 1;
verum end; let g1,
g2,
h be
Polynomial of
n,
L;
( g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) implies h = 0_ (n,L) )assume that A9:
(
g1 in G &
g2 in G )
and A10:
h is_a_normal_form_of S-Poly (
g1,
g2,
T),
PolyRedRel (
G,
T)
;
h = 0_ (n,L)
S-Poly (
g1,
g2,
T)
in G -Ideal
by A9, Th18;
then
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
by A3, GROEB_1:15;
then A11:
S-Poly (
g1,
g2,
T),
0_ (
n,
L)
are_convertible_wrt PolyRedRel (
G,
T)
by REWRITE1:25;
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
h
by A10, REWRITE1:def 6;
then
h,
S-Poly (
g1,
g2,
T)
are_convertible_wrt PolyRedRel (
G,
T)
by REWRITE1:25;
then A12:
h,
0_ (
n,
L)
are_convertible_wrt PolyRedRel (
G,
T)
by A11, REWRITE1:30;
h is_a_normal_form_wrt PolyRedRel (
G,
T)
by A10, REWRITE1:def 6;
hence
h = 0_ (
n,
L)
by A3, A4, A12, REWRITE1:def 19;
verum hence
for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G &
h is_a_normal_form_of S-Poly (
g1,
g2,
T),
PolyRedRel (
G,
T) holds
h = 0_ (
n,
L)
;
verum end;