:: Polynomial Reduction :: by Christoph Schwarzweller :: :: Received December 20, 2002 :: Copyright (c) 2002-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ORDINAL1, ZFMISC_1, STRUCT_0, VALUED_0, POLYNOM7, SUBSET_1, RELAT_1, SUPINF_2, POLYNOM1, VECTSP_1, ORDERS_1, TARSKI, PRE_POLY, ARYTM_3, FUNCT_1, ALGSEQ_1, NAT_1, FINSET_1, CARD_1, XXREAL_0, XBOOLE_0, RLVECT_1, ALGSTR_0, FINSEQ_1, CARD_3, PARTFUN1, ORDINAL4, ARYTM_1, ALGSTR_1, LATTICES, VECTSP_2, BINOP_1, CAT_3, RELAT_2, BAGORDER, TERMORD, XCMPLX_0, BROUWER, ORDERS_2, WELLORD1, FINSUB_1, WAYBEL_4, MESFUNC1, REWRITE1, INT_1, IDEAL_1, POLYRED; notations CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XXREAL_0, STRUCT_0, ALGSTR_0, ALGSTR_1, WAYBEL_0, FINSUB_1, WAYBEL_4, REWRITE1, RLVECT_1, FINSEQ_1, XTUPLE_0, MCART_1, ORDERS_1, VFUNCT_1, GROUP_1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1, IDEAL_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD, PRE_POLY; constructors REWRITE1, VECTSP_2, TRIANG_1, WAYBEL_4, WELLFND1, IDEAL_1, BAGORDER, TERMORD, DOMAIN_1, RELSET_1, BINOP_2, FVSUM_1, VFUNCT_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, FINSUB_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, BAGORDER, TERMORD, VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1, RELSET_1; requirements NUMERALS, REAL, SUBSET, BOOLE; begin :: Preliminaries registration let n be Ordinal, R be non trivial ZeroStr; cluster non-zero for Monomial of n,R; end; registration cluster non trivial for Field; end; registration let n be Ordinal, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p,q be non-zero finite-Support Series of n,L; cluster p *' q -> non-zero; end; begin :: More on Polynomials and Monomials theorem :: POLYRED:1 for X being set, L being Abelian add-associative right_zeroed right_complementable non empty addLoopStr, p,q being Series of X, L holds -(p + q) = (-p) + (-q); theorem :: POLYRED:2 for X being set, L being left_zeroed non empty addLoopStr, p being Series of X, L holds 0_(X,L) + p = p; theorem :: POLYRED:3 for X being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p being Series of X, L holds -p + p = 0_(X,L) & p + -p = 0_(X,L); theorem :: POLYRED:4 for n being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds p - 0_(n ,L) = p; theorem :: POLYRED:5 for n being Ordinal, L being add-associative right_complementable right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p being Series of n,L holds 0_(n,L) *' p = 0_(n,L); theorem :: POLYRED:6 for n being Ordinal, L being Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p,q being Polynomial of n,L holds -(p *' q) = (-p) *' q & -(p *' q) = p *' (-q); theorem :: POLYRED:7 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p being Polynomial of n,L, m being Monomial of n,L, b being bag of n holds (m*'p).(term(m)+b) = m.term(m) * p.b; theorem :: POLYRED:8 for X being set, L being right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p being Series of X,L holds 0.L * p = 0_(X,L); theorem :: POLYRED:9 for X being set, L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p being Series of X,L, a being Element of L holds -(a * p) = (-a) * p & -(a * p) = a * (-p); theorem :: POLYRED:10 for X being set, L being left-distributive non empty doubleLoopStr, p being Series of X,L, a,a9 being Element of L holds a * p + a9 * p = (a + a9) * p; theorem :: POLYRED:11 for X being set, L being associative non empty multLoopStr_0, p being Series of X,L, a,a9 being Element of L holds (a * a9) * p = a * (a9 * p ); theorem :: POLYRED:12 for n being Ordinal, L being add-associative right_zeroed right_complementable well-unital associative commutative distributive non empty doubleLoopStr, p,p9 being Series of n,L, a being Element of L holds a * (p *' p9) = p *' (a * p9); begin :: Multiplication of polynomials with bags definition let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L; func b *' p -> Series of n,L means :: POLYRED:def 1 for b9 being bag of n st b divides b9 holds it.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds it.b9 = 0.L; end; registration let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be finite-Support Series of n,L; cluster b *' p -> finite-Support; end; theorem :: POLYRED:13 for n being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p being Series of n,L holds (b*'p).(b9+b) = p.b9; theorem :: POLYRED:14 for n being Ordinal, L being non empty ZeroStr, p being Polynomial of n,L, b being bag of n holds Support(b*'p) c= {b + b9 where b9 is Element of Bags n : b9 in Support p}; theorem :: POLYRED:15 for n being Ordinal, T being connected admissible TermOrder of n , L being non trivial ZeroStr, p being non-zero Polynomial of n,L, b being bag of n holds HT(b*'p,T) = b + HT(p,T); theorem :: POLYRED:16 for n being Ordinal, T being connected admissible TermOrder of n , L being non empty ZeroStr, p being Polynomial of n,L, b,b9 being bag of n holds b9 in Support(b*'p) implies b9 <= b+HT(p,T),T; theorem :: POLYRED:17 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L holds (EmptyBag n) *' p = p; theorem :: POLYRED:18 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L, b1,b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p); theorem :: POLYRED:19 for n being Ordinal, L being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L holds Support(a*p) c= Support(p); theorem :: POLYRED:20 for n being Ordinal, L being domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, a being non zero Element of L holds Support(p) c= Support(a*p); theorem :: POLYRED:21 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, a being non zero Element of L holds HT(a*p,T) = HT(p,T); theorem :: POLYRED:22 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive non trivial doubleLoopStr, p being Series of n,L, b being bag of n, a being Element of L holds a * (b *' p) = Monom(a,b) *' p; theorem :: POLYRED:23 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p being non-zero Polynomial of n,L, q being Polynomial of n,L, m being non-zero Monomial of n,L holds HT(p,T) in Support q implies HT(m*'p,T) in Support(m*'q); begin :: Orders on Polynomials registration let n be Ordinal, T be connected TermOrder of n; cluster RelStr(#Bags n, T#) -> connected; end; registration let n be Nat, T be admissible TermOrder of n; cluster RelStr (#Bags n, T#) -> well_founded; end; definition :: according to p. 193 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p <= q,T means :: POLYRED:def 2 [Support p, Support q] in FinOrd RelStr(# Bags n, T#); end; definition let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p < q,T means :: POLYRED:def 3 p <= q,T & Support p <> Support q; end; definition let n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L; func Support(p,T) -> Element of Fin the carrier of RelStr(#Bags n,T#) equals :: POLYRED:def 4 Support(p); end; theorem :: POLYRED:24 :: according to definition 5.15, p. 194 for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being non-zero Polynomial of n,L holds PosetMax(Support( p,T)) = HT(p,T); theorem :: POLYRED:25 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p being Polynomial of n,L holds p <= p,T; theorem :: POLYRED:26 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T & q <= p,T iff Support p = Support q; theorem :: POLYRED:27 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q,r being Polynomial of n,L holds p <= q,T & q <= r,T implies p <= r,T; theorem :: POLYRED:28 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T or q <= p,T; theorem :: POLYRED:29 for n being Ordinal, T being connected TermOrder of n, L being non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T iff not q < p, T; theorem :: POLYRED:30 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T; theorem :: POLYRED:31 :: according to p. 193 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L) holds ex p being Polynomial of n,L st p in P & for q being Polynomial of n,L st q in P holds p <= q,T; theorem :: POLYRED:32 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr , p,q being Polynomial of n,L holds p < q,T iff (p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T); theorem :: POLYRED:33 :: exercise 5.16, p. 194 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < HM(p,T),T; theorem :: POLYRED:34 :: exercise 5.16, p. 194 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being Polynomial of n,L holds HM(p,T) <= p,T; theorem :: POLYRED:35 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed non trivial addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < p,T; begin :: Polynomial Reduction definition :: definition 5.18 (i), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L, b be bag of n; pred f reduces_to g,p,b,T means :: POLYRED:def 5 f <> 0_(n,L) & p <> 0_(n,L) & b in Support f & ex s being bag of n st s + HT(p,T) = b & g = f - (f.b/HC(p,T)) * (s *' p); end; definition :: definition 5.18 (ii), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L; pred f reduces_to g,p,T means :: POLYRED:def 6 ex b being bag of n st f reduces_to g,p ,b,T; end; definition :: definition 5.18 (iii), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f reduces_to g,P,T means :: POLYRED:def 7 ex p being Polynomial of n,L st p in P & f reduces_to g,p,T; end; definition :: definition 5.18 (iv), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; pred f is_reducible_wrt p,T means :: POLYRED:def 8 ex g being Polynomial of n,L st f reduces_to g,p,T; end; notation :: definition 5.18 (iv), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T; antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T; end; definition :: definition 5.18 (v), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_reducible_wrt P,T means :: POLYRED:def 9 ex g being Polynomial of n,L st f reduces_to g,P,T; end; notation :: definition 5.18 (v), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T; antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n,L; pred f top_reduces_to g,p,T means :: POLYRED:def 10 f reduces_to g,p,HT(f,T),T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n,L; pred f is_top_reducible_wrt p,T means :: POLYRED:def 11 ex g being Polynomial of n,L st f top_reduces_to g,p,T; end; definition :: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_top_reducible_wrt P,T means :: POLYRED:def 12 ex p being Polynomial of n,L st p in P & f is_top_reducible_wrt p,T; end; theorem :: POLYRED:36 :: lemma 5.20 (i), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f being Polynomial of n,L, p being non-zero Polynomial of n,L holds f is_reducible_wrt p,T iff ex b being bag of n st b in Support f & HT(p,T) divides b; theorem :: POLYRED:37 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p being Polynomial of n,L holds 0_(n,L) is_irreducible_wrt p,T; theorem :: POLYRED:38 :: lemma 5.20 (ii), p. 197 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to f-m*'p,p,T implies HT(m*'p,T) in Support f; theorem :: POLYRED:39 :: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L, b being bag of n holds f reduces_to g,p,b,T implies not(b in Support g); theorem :: POLYRED:40 :: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T holds f reduces_to g,p,b,T implies (b9 in Support g iff b9 in Support f); theorem :: POLYRED:41 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T holds f reduces_to g,p,b,T implies f.b9 = g.b9; theorem :: POLYRED:42 for n being Ordinal, T being connected admissible TermOrder of n , L being add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p, T implies for b being bag of n st b in Support g holds b <= HT(f,T),T; theorem :: POLYRED:43 :: lemma 5.20 (iv), p. 197 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p, T implies g < f,T; begin :: Polynomial Reduction Relation definition let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L); func PolyRedRel(P,T) -> Relation of NonZero Polynom-Ring(n,L), the carrier of Polynom-Ring(n,L) means :: POLYRED:def 13 for p,q being Polynomial of n,L holds [p,q] in it iff p reduces_to q,P,T; end; theorem :: POLYRED:44 :: lemma 5.20 (v), p. 197 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,g being Polynomial of n,L, P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies g <= f,T & (g = 0_( n,L) or HT(g,T) <= HT(f,T),T); registration :: theorem 5.21, p. 198 let n be Nat, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of Polynom-Ring(n,L); cluster PolyRedRel(P,T) -> strongly-normalizing; end; theorem :: POLYRED:45 :: lemma 5.24 (i), p. 200 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable left_zeroed right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,h being Polynomial of n,L holds f in P implies PolyRedRel(P,T) reduces h*'f,0_(n,L); theorem :: POLYRED:46 :: lemma 5.24 (ii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to g,P,T implies m*'f reduces_to m*'g,P,T; theorem :: POLYRED:47 :: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n , L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,g implies PolyRedRel(P,T) reduces m*'f,m*'g; theorem :: POLYRED:48 :: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,0_(n ,L) implies PolyRedRel(P,T) reduces m*'f,0_(n,L); theorem :: POLYRED:49 :: lemma 5.25 (i), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies ex f1,g1 being Polynomial of n,L st f1 - g1 = h1 & PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P ,T) reduces g,g1; theorem :: POLYRED:50 :: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convergent_wrt PolyRedRel(P,T); theorem :: POLYRED:51 :: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convertible_wrt PolyRedRel(P,T); definition let R be non empty addLoopStr, I be Subset of R, a,b be Element of R; pred a,b are_congruent_mod I means :: POLYRED:def 14 a - b in I; end; theorem :: POLYRED:52 for R being add-associative left_zeroed right_zeroed right_complementable right-distributive non empty doubleLoopStr, I being right-ideal non empty Subset of R, a being Element of R holds a,a are_congruent_mod I; theorem :: POLYRED:53 for R being add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, I being right-ideal non empty Subset of R, a,b being Element of R holds a,b are_congruent_mod I implies b,a are_congruent_mod I; theorem :: POLYRED:54 for R being add-associative right_zeroed right_complementable non empty addLoopStr, I being add-closed non empty Subset of R, a,b,c being Element of R holds a,b are_congruent_mod I & b,c are_congruent_mod I implies a, c are_congruent_mod I; theorem :: POLYRED:55 for R being Abelian add-associative right_zeroed right_complementable well-unital distributive associative non trivial doubleLoopStr, I being add-closed non empty Subset of R, a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a+c,b+d are_congruent_mod I; theorem :: POLYRED:56 for R being add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr, I being add-closed right-ideal non empty Subset of R, a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a*c,b*d are_congruent_mod I; theorem :: POLYRED:57 :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_convertible_wrt PolyRedRel(P,T) implies f,g are_congruent_mod P-Ideal; theorem :: POLYRED:58 :: lemma 5.26, p. 202 for n being Nat, T being admissible connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_congruent_mod P-Ideal implies f,g are_convertible_wrt PolyRedRel(P,T); theorem :: POLYRED:59 :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n, L holds PolyRedRel(P,T) reduces f,g implies f-g in P-Ideal; theorem :: POLYRED:60 :: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L holds PolyRedRel(P ,T) reduces f,0_(n,L) implies f in P-Ideal;