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 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; :: thesis: 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 ; :: 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 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) ) )
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 ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)
now :: thesis: for u being object st u in {g1,g2} holds
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
now :: thesis: ( ( u = g1 & u in G ) or ( u = g2 & u in G ) )
per cases ( u = g1 or u = g2 ) by A6, 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 A4; :: thesis: verum
end;
end;
end;
hence u in G ; :: thesis: verum
end;
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; :: thesis: verum
end;
case A8: 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
hence S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) ; :: thesis: 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; :: 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:25; :: thesis: verum