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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,T )

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( P is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T )

f has_a_Standard_Representation_of P,T ) by A1; :: thesis: verum

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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,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 non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,T )

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( P is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T )

A1: now :: thesis: ( ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T ) implies P is_Groebner_basis_wrt T )

A2:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;f has_a_Standard_Representation_of P,T ) implies P is_Groebner_basis_wrt T )

assume
for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T ; :: thesis: P is_Groebner_basis_wrt T

then for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T by Th39;

then for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) by GROEB_1:18;

then HT ((P -Ideal),T) c= multiples (HT (P,T)) by GROEB_1:19;

then PolyRedRel (P,T) is locally-confluent by GROEB_1:20;

hence P is_Groebner_basis_wrt T by GROEB_1:def 3; :: thesis: verum

end;f has_a_Standard_Representation_of P,T ; :: thesis: P is_Groebner_basis_wrt T

then for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T by Th39;

then for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) by GROEB_1:18;

then HT ((P -Ideal),T) c= multiples (HT (P,T)) by GROEB_1:19;

then PolyRedRel (P,T) is locally-confluent by GROEB_1:20;

hence P is_Groebner_basis_wrt T by GROEB_1:def 3; :: thesis: verum

now :: thesis: ( P is_Groebner_basis_wrt T implies for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T )

hence
( P is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in P -Ideal holds f has_a_Standard_Representation_of P,T )

assume
P is_Groebner_basis_wrt T
; :: thesis: for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T

then PolyRedRel (P,T) is locally-confluent by GROEB_1:def 3;

hence for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T by A2, Th38, GROEB_1:15; :: thesis: verum

end;f has_a_Standard_Representation_of P,T

then PolyRedRel (P,T) is locally-confluent by GROEB_1:def 3;

hence for f being non-zero Polynomial of n,L st f in P -Ideal holds

f has_a_Standard_Representation_of P,T by A2, Th38, GROEB_1:15; :: thesis: verum

f has_a_Standard_Representation_of P,T ) by A1; :: thesis: verum