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