let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n

for L being non degenerated non trivial 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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let T be connected admissible TermOrder of n; :: thesis: for L being non degenerated non trivial 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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let L be non degenerated non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) implies 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) )

assume A1: not 0_ (n,L) in G ; :: thesis: ( ex g1, g2 being Polynomial of n,L st

( g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & not PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or 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) )

assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: 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)

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)

hence 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) by GROEB_2:23; :: thesis: verum

for L being non degenerated non trivial 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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let T be connected admissible TermOrder of n; :: thesis: for L being non degenerated non trivial 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 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let L be non degenerated non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

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)

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) implies 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) )

assume A1: not 0_ (n,L) in G ; :: thesis: ( ex g1, g2 being Polynomial of n,L st

( g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & not PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or 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) )

assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: 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)

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

then
G is_Groebner_basis_wrt T
by A1, GROEB_2:25;
let g1, g2 be Polynomial of n,L; :: thesis: ( 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 ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

end;assume that

A3: g1 in G and

A4: g2 in G ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

now :: thesis: ( ( 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) ) )end;

hence
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
; :: thesis: verumper cases
( HT (g1,T), HT (g2,T) are_disjoint or not HT (g1,T), HT (g2,T) are_disjoint )
;

end;

case A5:
HT (g1,T), HT (g2,T) are_disjoint
; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

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; :: thesis: verum

end;

now :: thesis: for u being object st u in {g1,g2} holds

u in G

then A7:
{g1,g2} c= G
;u in G

let u be object ; :: thesis: ( u in {g1,g2} implies u in G )

assume A6: u in {g1,g2} ; :: thesis: u in G

end;assume A6: u in {g1,g2} ; :: thesis: u in G

now :: thesis: ( ( u = g1 & u in G ) or ( u = g2 & u in G ) )end;

hence
u in G
; :: thesis: verumPolyRedRel ({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; :: thesis: verum

case
not HT (g1,T), HT (g2,T) are_disjoint
; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

end;

end;

hence 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) by GROEB_2:23; :: thesis: verum