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 not 0_ (n,L) in G & ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
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 not 0_ (n,L) in G & ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
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 not 0_ (n,L) in G & ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
let G be Subset of (Polynom-Ring (n,L)); ( not 0_ (n,L) in G & ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ) implies G is_Groebner_basis_wrt T )
assume A1:
not 0_ (n,L) in G
; ( ex g1, g2, h being Polynomial of n,L st
( g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) & not h = 0_ (n,L) ) or G is_Groebner_basis_wrt T )
assume A2:
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
; G is_Groebner_basis_wrt T
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
proof
let g1,
g2 be
Polynomial of
n,
L;
( g1 in G & g2 in G implies PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )
assume that A3:
g1 in G
and A4:
g2 in G
;
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
now ( ( HT (g1,T), HT (g2,T) are_disjoint & PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or ( not HT (g1,T), HT (g2,T) are_disjoint & PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) )per cases
( HT (g1,T), HT (g2,T) are_disjoint or not HT (g1,T), HT (g2,T) are_disjoint )
;
case A5:
HT (
g1,
T),
HT (
g2,
T)
are_disjoint
;
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)then A7:
{g1,g2} c= G
;
PolyRedRel (
{g1,g2},
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
by A5, Th56;
hence
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
by A7, GROEB_1:4, REWRITE1:22;
verum end; case A8:
not
HT (
g1,
T),
HT (
g2,
T)
are_disjoint
;
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
S-Poly (
g1,
g2,
T)
has_a_normal_form_wrt PolyRedRel (
G,
T)
proof
now ( ( not S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) & S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) ) or ( S-Poly (g1,g2,T) in field (PolyRedRel (G,T)) & S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) ) )end;
hence
S-Poly (
g1,
g2,
T)
has_a_normal_form_wrt PolyRedRel (
G,
T)
;
verum
end; then consider h being
object such that A9:
h is_a_normal_form_of S-Poly (
g1,
g2,
T),
PolyRedRel (
G,
T)
by REWRITE1:def 11;
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
h
by A9, REWRITE1:def 6;
then reconsider h =
h as
Polynomial of
n,
L by Lm1;
h = 0_ (
n,
L)
by A2, A3, A4, A8, A9;
hence
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
by A9, REWRITE1:def 6;
verum end; end; end;
hence
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
;
verum
end;
hence
G is_Groebner_basis_wrt T
by A1, GROEB_2:25; verum