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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) )
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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) )
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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) )
let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) )
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( P is_Groebner_basis_wrt T implies ( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) ) )
assume P is_Groebner_basis_wrt T ; :: thesis: ( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) )
then PolyRedRel (P,T) is locally-confluent by Def3;
hence ( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) ) by Th15, POLYRED:60; :: thesis: verum