let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( g1 in G & g2 in G implies PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L )
assume A3: ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L

now

per cases ( HT g1,T, HT g2,T are_disjoint or not HT g1,T, HT g2,T are_disjoint ) ;

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

then A4: PolyRedRel {g1,g2},T reduces S-Poly g1,g2,T, 0_ n,L by Th56;

now

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

now

per cases ( u = g1 or u = g2 ) by A5, TARSKI:def 2;

case u = g1 ; :: thesis: u in G

hence u in G by A3; :: thesis: verum

end;

case u = g2 ; :: thesis: u in G

hence u in G by A3; :: thesis: verum

end;

end;

end;

hence u in G ; :: thesis: verum

end;

then {g1,g2} c= G by TARSKI:def 3;
hence PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L by A4, GROEB_1:4, REWRITE1:23; :: thesis: verum

end;

case A6: not HT g1,T, HT g2,T are_disjoint ; :: thesis: 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

per cases ( not S-Poly g1,g2,T in field (PolyRedRel G,T) or S-Poly g1,g2,T in field (PolyRedRel G,T) ) ;

case not S-Poly g1,g2,T in field (PolyRedRel G,T) ; :: thesis: S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T

hence S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T by REWRITE1:47; :: thesis: verum

end;

case S-Poly g1,g2,T in field (PolyRedRel G,T) ; :: thesis: S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T

hence S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T by REWRITE1:def 14; :: thesis: verum

end;

end;

end;

hence S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T ; :: thesis: verum

end;

then consider h being set such that
A7: 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 A7, REWRITE1:def 6;
then reconsider h = h as Polynomial of n,L by Lm1;
h = 0_ n,L by A2, A3, A6, A7;
hence PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L by A7, REWRITE1:def 6; :: thesis: verum

end;

end;

end;

hence PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ; :: thesis: verum

end;

hence G is_Groebner_basis_wrt T by A1, GROEB_2:30; :: thesis: verum