Copyright (c) 2002 Association of Mizar Users
environ vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, TRIANG_1, FINSEQ_1, VECTSP_1, RLVECT_1, ORDINAL1, LATTICES, ALGSEQ_1, ANPROJ_1, CAT_3, GROUP_1, VECTSP_2, RELAT_1, RELAT_2, REALSET1, ALGSTR_1, CARD_1, ARYTM_1, MCART_1, FINSEQ_4, ARYTM_3, SQUARE_1, PBOOLE, ORDERS_1, ORDERS_2, FINSET_1, BAGORDER, WELLORD1, DICKSON, TERMORD; notation NUMBERS, XCMPLX_0, XREAL_0, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, MONOID_0, CARD_1, BAGORDER, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, NAT_1, ALGSTR_1, RLVECT_1, PBOOLE, FINSEQ_1, MCART_1, TRIANG_1, REALSET1, VECTSP_1, VECTSP_2, RELAT_2, POLYNOM1, BINARITH, ORDERS_1, ORDERS_2, FINSEQ_4, WELLORD1, POLYNOM7; constructors ALGSTR_2, POLYNOM7, MONOID_0, BINOM, BAGORDER, MCART_1, TRIANG_1, ORDERS_2, MEMBERED; clusters XREAL_0, STRUCT_0, FINSET_1, RELSET_1, FINSEQ_1, CARD_1, ALGSTR_1, POLYNOM1, POLYNOM2, POLYNOM7, BAGORDER, VECTSP_1, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, POLYNOM1, PBOOLE, NAT_1, REAL_1, FINSEQ_4, BINOM, TRIANG_1, RLVECT_1, VECTSP_2, FINSET_1, POLYNOM7, POLYNOM2, NAT_2, RELAT_2, CARD_1, CARD_2, ORDERS_1, MATRLIN, SEQM_3, XBOOLE_0, XBOOLE_1, BINARITH, ORDERS_2, MCART_1, BAGORDER, WELLORD1, VECTSP_1, XCMPLX_0, XCMPLX_1; schemes BINOM; begin :: Preliminaries definition cluster non trivial LoopStr; existence proof consider R being Field; take R; thus thesis; end; end; definition cluster add-associative right_complementable right_zeroed (non trivial LoopStr); existence proof consider F being Field; take F; thus thesis; end; end; definition let X be set, b be bag of X; attr b is non-zero means b <> EmptyBag X; end; theorem Th1: for X being set, b1,b2 being bag of X holds b1 divides b2 iff ex b being bag of X st b2 = b1 + b proof let n be set, b1,b2 be bag of n; now assume A1: b1 divides b2; A2: now let k be set; b1.k <= b2.k by A1,POLYNOM1:def 13; then b1.k - b1.k <= b2.k - b1.k by REAL_1:49; hence 0 <= b2.k - b1.k by XCMPLX_1:14; end; now per cases; case A3: n = {}; then b1 + EmptyBag n = EmptyBag n by POLYNOM7:3 .= b2 by A3,POLYNOM7:3; hence ex b being bag of n st b2 = b1 + b; case n <> {}; then reconsider n' = n as non empty set; set b = { [k,b2.k -' b1.k] where k is Element of n' : not contradiction}; A4: now let x be set; assume x in b; then consider k being Element of n' such that A5: x = [k,b2.k -' b1.k]; thus ex y,z being set st x = [y,z] by A5; end; now let x,y1,y2 be set; assume A6: [x,y1] in b & [x,y2] in b; then consider k being Element of n' such that A7: [x,y1] = [k,b2.k -' b1.k]; consider k' being Element of n' such that A8: [x,y2] = [k',b2.k' -' b1.k'] by A6; k = [x,y1]`1 by A7,MCART_1:def 1 .= x by MCART_1:def 1 .= [x,y2]`1 by MCART_1:def 1 .= k' by A8,MCART_1:def 1; hence y1 = [x,y2]`2 by A7,A8,MCART_1:def 2 .= y2 by MCART_1:def 2; end; then reconsider b as Function by A4,FUNCT_1:def 1,RELAT_1:def 1; A9: now let x be set; assume x in dom b; then consider y being set such that A10: [x,y] in b by RELAT_1:def 4; consider k being Element of n' such that A11: [x,y] = [k,b2.k -' b1.k] by A10; x = [k,b2.k -' b1.k]`1 by A11,MCART_1:def 1 .= k by MCART_1:def 1; hence x in n'; end; now let x be set; assume x in n'; then reconsider k = x as Element of n'; [k,b2.k -' b1.k] in b; hence x in dom b by RELAT_1:def 4; end; then A12: dom b = n' by A9,TARSKI:2; then reconsider b as ManySortedSet of n' by PBOOLE:def 3; now let x be set; assume x in rng b; then consider y be set such that A13: [y,x] in b by RELAT_1:def 5; consider k being Element of n' such that A14: [y,x] = [k,b2.k -' b1.k] by A13; x = [k,b2.k -' b1.k]`2 by A14,MCART_1:def 2 .= b2.k -' b1.k by MCART_1:def 2; hence x in NAT; end; then A15: rng b c= NAT by TARSKI:def 3; A16: now let k be set; assume k in n; then consider u being set such that A17: [k,u] in b by A12,RELAT_1:def 4; consider k' being Element of n' such that A18: [k,u] = [k',b2.k' -' b1.k'] by A17; A19: k = [k',b2.k' -' b1.k']`1 by A18,MCART_1:def 1 .= k' by MCART_1:def 1; u = [k',b2.k' -' b1.k']`2 by A18,MCART_1:def 2 .= b2.k' -' b1.k' by MCART_1:def 2; hence b.k = b2.k -' b1.k by A17,A19,FUNCT_1:8; end; now let x be set; assume A20: x in support b; then A21: b.x <> 0 by POLYNOM1:def 7; A22: support b c= dom b by POLYNOM1:41; now assume not(x in support b2); then A23: b2.x = 0 by POLYNOM1:def 7; 0 <= b1.x by NAT_1:18; then 0 = b2.x-'b1.x by A23,NAT_2:10; hence contradiction by A12,A16,A20,A21,A22; end; hence x in support b2; end; then support b c= support b2 by TARSKI:def 3; then support b is finite by FINSET_1:13; then reconsider b as bag of n by A15,POLYNOM1:def 8,SEQM_3:def 8; take b; now let k be set; assume A24: k in n; A25: 0 <= b2.k - b1.k by A2; thus b1.k + b.k = b1.k + (b2.k -' b1.k) by A16,A24 .= b1.k + (b2.k - b1.k) by A25,BINARITH:def 3 .= b1.k + (b2.k + -b1.k) by XCMPLX_0:def 8 .= (b1.k + - b1.k) + b2.k by XCMPLX_1:1 .= (b1.k - b1.k) + b2.k by XCMPLX_0:def 8 .= 0 + b2.k by XCMPLX_1:14 .= b2.k; end; then b2 = b1 + b by POLYNOM1:37; hence ex b being bag of n st b2 = b1 + b; end; hence ex b being bag of n st b2 = b1 + b; end; hence thesis by POLYNOM1:54; end; theorem Th2: for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p being Series of n, L holds 0_(n,L) *' p = 0_(n,L) proof let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p be Series of n, L; set Z = 0_(n,L); now let b be Element of Bags n; consider s being FinSequence of the carrier of L such that A1: (Z*'p).b = Sum s and len s = len decomp b and A2: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = Z.b1*p.b2 by POLYNOM1:def 26; now let k be Nat; assume k in dom s; then consider b1, b2 being bag of n such that (decomp b)/.k = <*b1, b2*> and A3: s/.k = Z.b1*p.b2 by A2; thus s/.k = 0.L*p.b2 by A3,POLYNOM1:81 .= 0.L by VECTSP_1:39; end; then Sum s = 0.L by MATRLIN:15; hence (Z*'p).b = Z.b by A1,POLYNOM1:81; end; hence 0_(n,L)*'p = 0_(n,L) by FUNCT_2:113; end; definition let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), m1,m2 be Monomial of n,L; cluster m1 *' m2 -> monomial-like; coherence proof per cases; suppose Support(m1*'m2) = {}; hence thesis by POLYNOM7:6; suppose A1: Support(m1*'m2) <> {}; now per cases; case A2: Support(m1) <> {} & Support(m2) <> {}; then consider mb1 being bag of n such that A3: Support(m1) = {mb1} by POLYNOM7:6; mb1 in Support m1 by A3,TARSKI:def 1; then A4: m1.mb1 <> 0.L by POLYNOM1:def 9; A5: now let b be bag of n; assume A6: b <> mb1; consider b' being bag of n such that A7: for b being bag of n st b <> b' holds m1.b = 0.L by POLYNOM7:def 4; b' = mb1 by A4,A7; hence m1.b = 0.L by A6,A7; end; consider mb2 being bag of n such that A8: Support(m2) = {mb2} by A2,POLYNOM7:6; mb2 in Support m2 by A8,TARSKI:def 1; then A9: m2.mb2 <> 0.L by POLYNOM1:def 9; A10: now let b be bag of n; assume A11: b <> mb2; consider b' being bag of n such that A12: for b being bag of n st b <> b' holds m2.b = 0.L by POLYNOM7:def 4; b' = mb2 by A9,A12; hence m2.b = 0.L by A11,A12; end; consider b being Element of Support(m1*'m2); A13: b in Support(m1*'m2) by A1; then b is Element of Bags n; then reconsider b as bag of n; consider s being FinSequence of the carrier of L such that A14: (m1*'m2).b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 26; A15: dom s = Seg(len decomp b) by A14,FINSEQ_1:def 3 .= dom(decomp b) by FINSEQ_1:def 3; A16: now assume A17: b <> mb1 + mb2; A18: now let k be Nat; assume A19: k in dom s; then consider b1,b2 being bag of n such that A20: (decomp b)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by A14; consider b1',b2' being bag of n such that A21: (decomp b)/.k = <*b1',b2'*> & b = b1'+b2' by A15,A19,POLYNOM1:72; A22: b1 = <*b1', b2'*>.1 by A20,A21,FINSEQ_1:61 .= b1' by FINSEQ_1:61; A23: b2 = <*b1', b2'*>.2 by A20,A21,FINSEQ_1:61 .= b2' by FINSEQ_1:61; now per cases by A17,A21,A22,A23; case b1 <> mb1; then m1.b1 = 0.L by A5; hence m1.b1*m2.b2 = 0.L by BINOM:1; case b2 <> mb2; then m2.b2 = 0.L by A10; hence m1.b1*m2.b2 = 0.L by BINOM:2; end; hence s/.k = 0.L by A20; end; now per cases; case dom s = {}; then s = <*>(the carrier of L) by FINSEQ_1:26; hence (m1*'m2).b = 0.L by A14,RLVECT_1:60; case A24: dom s <> {}; consider k being Element of dom s; A25: k in dom s by A24; for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A18; then s/.k = (m1*'m2).b by A14,A25,POLYNOM2:5; hence (m1*'m2).b = 0.L by A18,A25; end; hence contradiction by A13,POLYNOM1:def 9; end; now let b' be bag of n; assume A26: b' <> b; consider s being FinSequence of the carrier of L such that A27: (m1*'m2).b' = Sum s & len s = len decomp b' & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b')/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 26; A28: dom s = Seg(len decomp b') by A27,FINSEQ_1:def 3 .= dom(decomp b') by FINSEQ_1:def 3; A29: now let k be Nat; assume A30: k in dom s; then consider b1, b2 being bag of n such that A31: (decomp b')/.k = <*b1,b2*> & s/.k = m1.b1*m2.b2 by A27; consider b1',b2' being bag of n such that A32: (decomp b')/.k = <*b1',b2'*> & b' = b1'+b2' by A28,A30,POLYNOM1: 72; A33: b1 = <*b1', b2'*>.1 by A31,A32,FINSEQ_1:61 .= b1' by FINSEQ_1:61; A34: b2 = <*b1', b2'*>.2 by A31,A32,FINSEQ_1:61 .= b2' by FINSEQ_1:61; now per cases by A16,A26,A32,A33,A34; case b1 <> mb1; then m1.b1 = 0.L by A5; hence m1.b1*m2.b2 = 0.L by BINOM:1; case b2 <> mb2; then m2.b2 = 0.L by A10; hence m1.b1*m2.b2 = 0.L by BINOM:2; end; hence s/.k = 0.L by A31; end; now per cases; case dom s = {}; then s = <*>(the carrier of L) by FINSEQ_1:26; hence (m1*'m2).b' = 0.L by A27,RLVECT_1:60; case A35: dom s <> {}; consider k being Element of dom s; A36: k in dom s by A35; for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A29; then s/.k = (m1*'m2).b' by A27,A36,POLYNOM2:5; hence (m1*'m2).b' = 0.L by A29,A36; end; hence (m1*'m2).b' = 0.L; end; hence thesis by POLYNOM7:def 4; case A37: Support(m1) = {} or Support(m2) = {}; now per cases by A37; case Support(m1) = {}; then m1 = 0_(n,L) by POLYNOM7:1; hence thesis by Th2; case Support(m2) = {}; then m2 = 0_(n,L) by POLYNOM7:1; hence thesis by POLYNOM1:87; end; hence thesis; end; hence thesis; end; end; definition let n be Ordinal, L be add-associative right_complementable right_zeroed distributive (non empty doubleLoopStr), c1,c2 be ConstPoly of n,L; cluster c1 *' c2 -> Constant; coherence proof set p = c1 *' c2; now let b be bag of n; assume A1: b <> EmptyBag n; consider s being FinSequence of the carrier of L such that A2: p.b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = c1.b1*c2.b2 by POLYNOM1:def 26; A3: dom s = Seg(len decomp b) by A2,FINSEQ_1:def 3 .= dom(decomp b) by FINSEQ_1:def 3; A4: now let k be Nat; assume A5: k in dom s; then consider b1, b2 being bag of n such that A6: (decomp b)/.k = <*b1,b2*> & s/.k = c1.b1*c2.b2 by A2; consider b1',b2' being bag of n such that A7: (decomp b)/.k = <*b1',b2'*> & b = b1'+b2' by A3,A5,POLYNOM1:72; A8: b1 = <*b1', b2'*>.1 by A6,A7,FINSEQ_1:61 .= b1' by FINSEQ_1:61; b2 = <*b1', b2'*>.2 by A6,A7,FINSEQ_1:61 .= b2' by FINSEQ_1:61; then A9: b1 <> EmptyBag n or b2 <> EmptyBag n by A1,A7,A8,POLYNOM1:57; now per cases by A9,POLYNOM7:def 8; case c1.b1 = 0.L; hence s/.k = 0.L by A6,BINOM:1; case c2.b2 = 0.L; hence s/.k = 0.L by A6,BINOM:2; end; hence s/.k = 0.L; end; now per cases; case dom s = {}; then s = <*>(the carrier of L) by FINSEQ_1:26; hence p.b = 0.L by A2,RLVECT_1:60; case A10: dom s <> {}; consider k being Element of dom s; A11: k in dom s by A10; for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A4; then Sum s = s/.k by A11,POLYNOM2:5; hence p.b = 0.L by A2,A4,A11; end; hence p.b = 0.L; end; hence thesis by POLYNOM7:def 8; end; end; theorem Th3: for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), b,b' being bag of n, a,a' being non-zero Element of L holds Monom(a * a',b + b') = Monom(a,b) *' Monom(a',b') proof let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), b,b' be bag of n, a,a' be non-zero Element of L; set m1 = Monom(a,b), m2 = Monom(a',b'); set m = Monom(a * a',b + b'); set m3 = m1 *' m2; A1: a <> 0.L & a' <> 0.L by RLVECT_1:def 13; then a * a' <> 0.L by VECTSP_2:def 5; then A2: a * a' is non-zero by RLVECT_1:def 13; A3: m1.b = m1.(term(m1)) by POLYNOM7:10 .= coefficient(m1) by POLYNOM7:def 7 .= a by POLYNOM7:9; A4: m2.b' = m2.(term(m2)) by POLYNOM7:10 .= coefficient(m2) by POLYNOM7:def 7 .= a' by POLYNOM7:9; A5: now let u be bag of n; assume A6: u <> b; consider v being bag of n such that A7: for b' being bag of n st b' <> v holds m1.b' = 0.L by POLYNOM7:def 4; assume m1.u <> 0.L; then A8: u = v by A7; m1.b <> 0.L by A3,RLVECT_1:def 13; hence contradiction by A6,A7,A8; end; A9: now let u be bag of n; assume A10: u <> b'; consider v being bag of n such that A11: for b' being bag of n st b' <> v holds m2.b' = 0.L by POLYNOM7:def 4; assume m2.u <> 0.L; then A12: u = v by A11; m2.b' <> 0.L by A4,RLVECT_1:def 13; hence contradiction by A10,A11,A12; end; consider s being FinSequence of the carrier of L such that A13: m3.(b+b') = Sum s & len s = len decomp(b+b') & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp(b+b'))/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 26; A14: dom s = Seg(len decomp(b+b')) by A13,FINSEQ_1:def 3 .= dom(decomp(b+b')) by FINSEQ_1:def 3; set u = b+b'; consider k' being Nat such that A15: k' in dom decomp u & (decomp u)/.k' = <*b,b'*> by POLYNOM1:73; consider b1,b2 being bag of n such that A16: (decomp u)/.k' = <*b1, b2*> & s/.k' = m1.b1*m2.b2 by A13,A14,A15; A17: b1 = <*b,b'*>.1 by A15,A16,FINSEQ_1:61 .= b by FINSEQ_1:61; A18: b2 = <*b,b'*>.2 by A15,A16,FINSEQ_1:61 .= b' by FINSEQ_1:61; A19:now let k be Nat; assume A20: k in dom s & k <> k'; then consider b1,b2 being bag of n such that A21: (decomp u)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by A13; A22: now assume A23: b1 = b & b2 = b'; (decomp u).k = (decomp u)/.k by A14,A20,FINSEQ_4:def 4 .= (decomp u).k' by A15,A21,A23,FINSEQ_4:def 4; hence contradiction by A14,A15,A20,FUNCT_1:def 8; end; now per cases by A22; case b1 <> b; then m1.b1 = 0.L by A5; hence m1.b1 * m2.b2 = 0.L by BINOM:1; case b2 <> b'; then m2.b2 = 0.L by A9; hence m1.b1*m2.b2 = 0.L by BINOM:2; end; hence s/.k = 0.L by A21; end; then Sum s = s/.k' by A14,A15,POLYNOM2:5; then A24: m3.(b+b') <> 0.L by A1,A3,A4,A13,A16,A17,A18,VECTSP_2:def 5; then A25: term(m3) = b + b' by POLYNOM7:def 6 .= term(m) by A2,POLYNOM7:10; A26: coefficient(m3) = m3.(term(m3)) by POLYNOM7:def 7 .= m3.(b+b') by A24,POLYNOM7:def 6 .= a * a' by A3,A4,A13,A14,A15,A16,A17,A18,A19,POLYNOM2:5 .= coefficient(m) by POLYNOM7:9; thus m = Monom(coefficient(m),term(m)) by POLYNOM7:11 .= m3 by A25,A26,POLYNOM7:11; end; theorem for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), a,a' being Element of L holds (a * a') _(n,L) = (a _(n,L)) *' (a' _(n,L)) proof let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), a,a' be Element of L; per cases; suppose A1: a is non-zero & a' is non-zero; term((a*a') _(n,L)) = EmptyBag n & coefficient((a*a') _(n,L)) = a*a' by POLYNOM7:23; then A2: (a * a') _(n,L) = Monom(a*a',EmptyBag n) by POLYNOM7:11; term(a _(n,L)) = EmptyBag n & coefficient(a _(n,L)) = a by POLYNOM7:23; then A3: a _(n,L) = Monom(a,EmptyBag n) by POLYNOM7:11; term(a' _(n,L)) = EmptyBag n & coefficient(a' _(n,L)) = a' by POLYNOM7:23; then A4: a' _(n,L) = Monom(a',EmptyBag n) by POLYNOM7:11; EmptyBag n + EmptyBag n = EmptyBag n by POLYNOM1:57; hence thesis by A1,A2,A3,A4,Th3; suppose A5: not(a is non-zero & a' is non-zero); now per cases by A5,RLVECT_1:def 13; case A6: a = 0.L; then a * a' = 0.L by BINOM:1; then A7: (a * a') _(n,L) = 0_(n,L) by POLYNOM7:19; a _(n,L) = 0_(n,L) by A6,POLYNOM7:19; hence thesis by A7,Th2; case A8: a' = 0.L; then a * a' = 0.L by BINOM:2; then A9: (a * a') _(n,L) = 0_(n,L) by POLYNOM7:19; a' _(n,L) = 0_(n,L) by A8,POLYNOM7:19; hence thesis by A9,POLYNOM1:87; end; hence thesis; end; begin :: Term Orders Lm1: for n being Ordinal, T being TermOrder of n, b being set st b in field T holds b is bag of n proof let n be Ordinal, T be TermOrder of n, b be set; assume b in field T; then A1: b in dom T \/ rng T by RELAT_1:def 6; per cases by A1,XBOOLE_0:def 2; suppose b in dom T; then b is Element of Bags n; hence thesis; suppose b in rng T; then b is Element of Bags n; hence thesis; end; definition let n be Ordinal; cluster admissible connected TermOrder of n; existence proof set T = LexOrder n; take T; now let x,y be set; assume x in field T & y in field T & x <> y; then reconsider b1 = x, b2 = y as bag of n by Lm1; b1 <=' b2 or b2 <=' b1 by POLYNOM1:49; then [b1,b2] in BagOrder n or [b2,b1] in BagOrder n by POLYNOM1:def 16; hence [x,y] in T or [y,x] in T; end; then T is_connected_in field T by RELAT_2:def 6; hence thesis by RELAT_2:def 14; end; end; definition ::: theorem 5.5 (ii), p. 190 let n be Nat; cluster -> well_founded (admissible TermOrder of n); coherence proof let T be admissible TermOrder of n; T is well-ordering by BAGORDER:35; hence thesis by WELLORD1:def 4; end; end; definition let n be Ordinal, T be TermOrder of n, b,b' be bag of n; pred b <= b',T means :Def2: [b,b'] in T; end; definition let n be Ordinal, T be TermOrder of n, b,b' be bag of n; pred b < b',T means :Def3: b <= b',T & b <> b'; end; definition let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n; func min(b1,b2,T) -> bag of n equals :Def4: b1 if b1 <= b2,T otherwise b2; correctness; func max(b1,b2,T) -> bag of n equals :Def5: b1 if b2 <= b1,T otherwise b2; correctness; end; Lm2: for n being Ordinal, T being TermOrder of n, b being bag of n holds b <= b,T proof let n be Ordinal, T be TermOrder of n, b be bag of n; field T = Bags n by ORDERS_1:97; then A1: T is_reflexive_in Bags n by RELAT_2:def 9; b is Element of Bags n by POLYNOM1:def 14; then [b,b] in T by A1,RELAT_2:def 1; hence thesis by Def2; end; Lm3: for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 proof let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n; assume b1 <= b2,T & b2 <= b1,T; then A1: [b1,b2] in T & [b2,b1] in T by Def2; field T = Bags n by ORDERS_1:97; then A2: T is_antisymmetric_in Bags n by RELAT_2:def 12; b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14; hence thesis by A1,A2,RELAT_2:def 4; end; Lm4: for n being Ordinal, T being TermOrder of n, b being bag of n holds b in field T proof let n be Ordinal, T be TermOrder of n, b be bag of n; field T = Bags n by ORDERS_1:97; then A1: T is_reflexive_in Bags n by RELAT_2:def 9; b is Element of Bags n by POLYNOM1:def 14; then [b,b] in T by A1,RELAT_2:def 1; hence thesis by RELAT_1:30; end; theorem Th5: for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds b1 <= b2,T iff not(b2 < b1,T) proof let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n; A1: T is_connected_in field T by RELAT_2:def 14; per cases; suppose b1 = b2; hence thesis by Def3,Lm2; suppose A2: b1 <> b2; A3: b1 <= b2,T implies not(b2 < b1,T) proof assume A4: b1 <= b2,T; assume b2 < b1,T; then b2 <= b1,T & b1 <> b2 by Def3; hence thesis by A4,Lm3; end; not(b2 < b1,T) implies b1 <= b2,T proof assume A5: not(b2 < b1,T); now per cases by A5,Def3; case not(b2 <= b1,T); then A6: not([b2,b1] in T) by Def2; b1 in field T & b2 in field T by Lm4; then [b1,b2] in T by A1,A2,A6,RELAT_2:def 6; hence thesis by Def2; case b1 = b2; hence thesis by A2; end; hence thesis; end; hence thesis by A3; end; Lm5: for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds b1 <= b2,T or b2 <= b1,T proof let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n; A1: T is_connected_in field T by RELAT_2:def 14; per cases; suppose A2: b1 = b2; field T = Bags n by ORDERS_1:97; then A3: T is_reflexive_in Bags n by RELAT_2:def 9; b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14; then [b1,b2] in T by A2,A3,RELAT_2:def 1; hence thesis by Def2; suppose A4: b1 <> b2; assume not(b1 <= b2,T); then A5: not([b1,b2] in T) by Def2; b1 in field T & b2 in field T by Lm4; then [b2,b1] in T by A1,A4,A5,RELAT_2:def 6; hence thesis by Def2; end; theorem for n being Ordinal, T being TermOrder of n, b being bag of n holds b <= b,T by Lm2; theorem for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds b1 = b2 by Lm3; theorem Th8: for n being Ordinal, T being TermOrder of n, b1,b2,b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds b1 <= b3,T proof let n be Ordinal, T be TermOrder of n, b1,b2,b3 be bag of n; assume b1 <= b2,T & b2 <= b3,T; then A1: [b1,b2] in T & [b2,b3] in T by Def2; field T = Bags n by ORDERS_1:97; then A2: T is_transitive_in Bags n by RELAT_2:def 16; b1 is Element of Bags n & b2 is Element of Bags n & b3 is Element of Bags n by POLYNOM1:def 14; then [b1,b3] in T by A1,A2,RELAT_2:def 8; hence thesis by Def2; end; theorem Th9: for n being Ordinal, T being admissible TermOrder of n, b being bag of n holds EmptyBag n <= b,T proof let n be Ordinal, T be admissible TermOrder of n, b be bag of n; [EmptyBag n,b] in T by BAGORDER:def 7; hence thesis by Def2; end; theorem for n being Ordinal, T being admissible TermOrder of n, b1,b2 being bag of n holds b1 divides b2 implies b1 <= b2,T proof let n be Ordinal, T be admissible TermOrder of n, b1,b2 be bag of n; assume b1 divides b2; then consider b3 being bag of n such that A1: b2 = b1 + b3 by Th1; EmptyBag n <= b3,T by Th9; then [EmptyBag n,b3] in T by Def2; then [EmptyBag n + b1,b2] in T by A1,BAGORDER:def 7; then [b1,b2] in T by POLYNOM1:57; hence thesis by Def2; end; theorem Th11: for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n holds min(b1,b2,T) = b1 or min(b1,b2,T) = b2 proof let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n; assume A1: min(b1,b2,T) <> b1; now per cases by A1,Def4; case not(b1 <= b2,T); hence min(b1,b2,T) = b2 by Def4; case b1 = b2; then b1 <= b2,T by Lm2; hence contradiction by A1,Def4; end; hence thesis; end; theorem Th12: for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n holds max(b1,b2,T) = b1 or max(b1,b2,T) = b2 proof let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n; assume A1: max(b1,b2,T) <> b1; now per cases by A1,Def5; case not(b2 <= b1,T); hence max(b1,b2,T) = b2 by Def5; case b1 = b2; then b2 <= b1,T by Lm2; hence contradiction by A1,Def5; end; hence thesis; end; Lm6: for n being Ordinal, T being TermOrder of n, b being bag of n holds min(b,b,T) = b & max(b,b,T) = b proof let n being Ordinal, T being TermOrder of n, b being bag of n; A1: b <= b,T by Lm2; hence min(b,b,T) = b by Def4; thus max(b,b,T) = b by A1,Def5; end; theorem for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds min(b1,b2,T) <= b1,T & min(b1,b2,T) <= b2,T proof let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n; per cases by Lm5; suppose A1: b1 <= b2,T; then min(b1,b2,T) = b1 by Def4; hence thesis by A1,Lm2; suppose A2: b2 <= b1,T; now per cases; case A3: b1 = b2; then min(b1,b2,T) = b1 by Lm6; hence thesis by A3,Lm2; case b1 <> b2; then b2 < b1,T by A2,Def3; then not(b1 <= b2,T) by Th5; then min(b1,b2,T) = b2 by Def4; hence thesis by A2,Lm2; end; hence thesis; end; theorem Th14: for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds b1 <= max(b1,b2,T),T & b2 <= max(b1,b2,T),T proof let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n; per cases by Lm5; suppose A1: b2 <= b1,T; then max(b1,b2,T) = b1 by Def5; hence thesis by A1,Lm2; suppose A2: b1 <= b2,T; now per cases; case A3: b1 = b2; then max(b1,b2,T) = b1 by Lm6; hence thesis by A3,Lm2; case b1 <> b2; then b1 < b2,T by A2,Def3; then not(b2 <= b1,T) by Th5; then max(b1,b2,T) = b2 by Def5; hence thesis by A2,Lm2; end; hence thesis; end; theorem Th15: for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds min(b1,b2,T) = min(b2,b1,T) & max(b1,b2,T) = max(b2,b1,T) proof let n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n; now per cases; case A1: min(b1,b2,T) = b1; now per cases by A1,Def4; case A2: b1 <= b2,T; now per cases; case b1 = b2; hence min(b2,b1,T) = min(b1,b2,T); case b1 <> b2; then not(b2 <= b1,T) by A2,Lm3; hence min(b2,b1,T) = min(b1,b2,T) by A1,Def4; end; hence min(b1,b2,T) = min(b2,b1,T); case b1 = b2; hence min(b2,b1,T) = min(b1,b2,T); end; hence min(b1,b2,T) = min(b2,b1,T); case A3: min(b1,b2,T) <> b1; A4: now assume not(b2 <= b1,T); then b1 <= b2,T by Lm5; hence contradiction by A3,Def4; end; thus min(b1,b2,T) = b2 by A3,Th11 .= min(b2,b1,T) by A4,Def4; end; hence min(b1,b2,T) = min(b2,b1,T); now per cases; case A5: max(b1,b2,T) = b1; now per cases by A5,Def5; case A6: b2 <= b1,T; now per cases; case b1 = b2; hence max(b2,b1,T) = max(b1,b2,T); case b1 <> b2; then not(b1 <= b2,T) by A6,Lm3; hence max(b2,b1,T) = max(b1,b2,T) by A5,Def5; end; hence max(b1,b2,T) = max(b2,b1,T); case b1 = b2; hence max(b2,b1,T) = max(b1,b2,T); end; hence max(b1,b2,T) = max(b2,b1,T); case A7: max(b1,b2,T) <> b1; now now per cases by Lm5; case b1 <= b2,T; hence max(b2,b1,T) = b2 by Def5 .= max(b1,b2,T) by A7,Th12; case b2 <= b1,T; hence max(b2,b1,T) = max(b1,b2,T) by A7,Def5; end; hence max(b2,b1,T) = max(b1,b2,T); end; hence max(b2,b1,T) = max(b1,b2,T); end; hence max(b1,b2,T) = max(b2,b1,T); end; theorem for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n holds min(b1,b2,T) = b1 iff max(b1,b2,T) = b2 proof let n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n; A1: now assume A2: min(b1,b2,T) = b1; now per cases by A2,Def4; case b1 <= b2,T; then max(b2,b1,T) = b2 by Def5; hence max(b1,b2,T) = b2 by Th15; case b1 = b2; hence max(b1,b2,T) = b2 by Th12; end; hence max(b1,b2,T) = b2; end; now assume A3: max(b1,b2,T) = b2; now per cases by A3,Def5; case not(b2 <= b1,T); then b1 <= b2,T by Lm5; hence min(b1,b2,T) = b1 by Def4; case b1 = b2; hence min(b1,b2,T) = b1 by Th11; end; hence min(b1,b2,T) = b1; end; hence thesis by A1; end; begin :: Headterms, Headmonomials and Headcoefficients definition ::: definition 5.15, p. 194 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; func HT(p,T) -> Element of Bags n means :Def6: (Support p = {} & it = EmptyBag n) or (it in Support p & for b being bag of n st b in Support p holds b <= it,T); existence proof set O = T; per cases; suppose Support p = {}; hence thesis; suppose A1: Support p <> {}; defpred P[Nat] means for B being finite Subset of Bags n st card B = $1 holds ex b' being bag of n st b' in B & for b being bag of n st b in B holds [b,b'] in O; A2: P[1] proof let B be finite Subset of Bags n; assume A3: card B = 1; consider x being set; card {x} = card B by A3,CARD_1:79; then consider b being set such that A4: B = {b} by CARD_1:49; A5: b in B by A4,TARSKI:def 1; then reconsider b as Element of Bags n; reconsider b as bag of n; now let b' be bag of n; assume b' in B; then b' = b by A4,TARSKI:def 1; hence [b',b] in O by ORDERS_1:12; end; hence ex b' being bag of n st b' in B & for b being bag of n st b in B holds [b,b'] in O by A5; end; A6: for k being Nat st 1 <= k holds P[k] implies P[k+1] proof let k be Nat; assume A7: 1 <= k; thus P[k] implies P[k+1] proof assume A8: P[k]; thus P[k+1] proof let B be finite Subset of Bags n; assume A9: card B = k+1; then reconsider B as non empty finite Subset of Bags n by CARD_1:47; consider x being Element of B; x in B & B c= Bags n; then reconsider x as Element of Bags n; reconsider x as bag of n; set X = B \ {x}; A10: x in X iff x in B & not x in {x} by XBOOLE_0:def 4; now let u be set; assume u in {x}; then u = x by TARSKI:def 1; hence u in B; end; then {x} c= B by TARSKI:def 3; then A11: B = {x} \/ B by XBOOLE_1:12 .= {x} \/ X by XBOOLE_1:39; then card(X) + 1 = k + 1 by A9,A10,CARD_2:54,TARSKI:def 1; then A12: card(X) = k by XCMPLX_1:2; now assume X = {}; hence contradiction by A7,A12,CARD_1:47,51; end; then reconsider X as non empty set; reconsider X as non empty finite set; now let u be set; assume u in X; then u in B by XBOOLE_0:def 4; hence u in Bags n; end; then reconsider X as non empty finite Subset of Bags n by TARSKI:def 3; consider b' being bag of n such that A13: b' in X & for b being bag of n st b in X holds [b,b'] in O by A8,A12; A14: O is_connected_in field O by RELAT_2:def 14; now per cases; case A15: x = b'; take b'; A16: X c= B by XBOOLE_1:36; now let b be bag of n; assume A17: b in B; now per cases; case b in X; hence [b,b'] in O by A13; case not(b in X); then b in {x} by A11,A17,XBOOLE_0:def 2; then b = x by TARSKI:def 1; hence [b,b'] in O by A15,ORDERS_1:12; end; hence [b,b'] in O; end; hence thesis by A13,A16; case A18: x <> b'; A19: [x,x] in O by ORDERS_1:12; b' is Element of Bags n by POLYNOM1:def 14; then [b',b'] in O by ORDERS_1:12; then A20: x in field O & b' in field O by A19,RELAT_1:30; now per cases by A14,A18,A20,RELAT_2:def 6; case A21: [x,b'] in O; thus ex b' being bag of n st b' in B & for b being bag of n st b in B holds [b,b'] in O proof take b'; for b being bag of n st b in B holds [b,b'] in O proof let b be bag of n; assume A22: b in B; now per cases; case b <> x; then not(b in {x}) by TARSKI:def 1; then b in X by A22,XBOOLE_0:def 4; hence thesis by A13; case b = x; hence thesis by A21; end; hence thesis; end; hence thesis by A13,XBOOLE_0:def 4; end; case A23: [b',x] in O; thus ex b' being bag of n st b' in B & for b being bag of n st b in B holds [b,b'] in O proof take x; for b being bag of n st b in B holds [b,x] in O proof let b be bag of n; assume A24: b in B; now per cases; case b <> x; then not(b in {x}) by TARSKI:def 1; then b in X by A24,XBOOLE_0:def 4; then A25: [b,b'] in O by A13; b is Element of Bags n & b' is Element of Bags n by POLYNOM1:def 14; hence thesis by A23,A25,ORDERS_1:14; case b = x; hence thesis by ORDERS_1:12; end; hence thesis; end; hence thesis; end; end; hence thesis; end; hence thesis; end; thus thesis; end; end; A26: for k being Nat st 1 <= k holds P[k] from Ind2(A2,A6); reconsider sp = Support p as finite set by POLYNOM1:def 10; Card sp is finite; then consider m being Nat such that A27: Card(Support p) = Card m by CARD_1:86; A28: Card(Support p) = m by A27,CARD_1:66; now assume m = 0; then card sp = 0 by A27,CARD_1:66; hence contradiction by A1,CARD_2:59; end; then A29: 1 <= m by RLVECT_1:99; reconsider sp = Support p as finite Subset of Bags n by POLYNOM1:def 10; consider b' being bag of n such that A30: b' in sp & for b being bag of n st b in sp holds [b,b'] in O by A26,A28,A29; take b'; now let b be bag of n; assume b in sp; then [b,b'] in O by A30; hence b <= b',O by Def2; end; hence thesis by A30; end; uniqueness proof set O = T; let b1,b2 be Element of Bags n; assume A31: (Support p = {} & b1 = EmptyBag n) or (b1 in Support p & for b being bag of n st b in Support p holds b <= b1,O); assume A32: (Support p = {} & b2 = EmptyBag n) or (b2 in Support p & for b being bag of n st b in Support p holds b <= b2,O); per cases; suppose Support p = {}; hence b1 = b2 by A31,A32; suppose Support p <> {}; then b2 <= b1,O & b1 <= b2,O by A31,A32; then [b1,b2] in O & [b2,b1] in O by Def2; hence b1 = b2 by ORDERS_1:13; end; end; definition ::: definition 5.15, p. 194 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; func HC(p,T) -> Element of L equals :Def7: p.(HT(p,T)); correctness; end; definition ::: definition 5.15, p. 194 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; func HM(p,T) -> Monomial of n,L equals :Def8: Monom(HC(p,T),HT(p,T)); correctness; end; Lm7: for n being Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L holds HC(p,O) = 0.L iff p = 0_(n,L) proof let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n,L; A1: now assume HC(p,O) = 0.L; then p.(HT(p,O)) = 0.L by Def7; then not(HT(p,O) in Support p) by POLYNOM1:def 9; then Support p = {} by Def6; hence p = 0_(n,L) by POLYNOM7:1; end; now assume p = 0_(n,L); then p.(HT(p,O)) = 0.L by POLYNOM1:81; hence HC(p,O) = 0.L by Def7; end; hence thesis by A1; end; Lm8: for n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L holds (HM(p,O)).(HT(p,O)) = p.(HT(p,O)) proof let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; A1: HM(p,O) = Monom(HC(p,O),HT(p,O)) by Def8; A2: p.(HT(p,O)) = HC(p,O) by Def7 .= coefficient(HM(p,O)) by A1,POLYNOM7:9 .= (HM(p,O)).term(HM(p,O)) by POLYNOM7:def 7; now per cases; case HC(p,O) <> 0.L; then HC(p,O) is non-zero by RLVECT_1:def 13; hence term(HM(p,O)) = HT(p,O) by A1,POLYNOM7:10; case A3: HC(p,O) = 0.L; then p = 0_(n,L) by Lm7; then Support p = {} by POLYNOM7:1; then HT(p,O) = EmptyBag n by Def6; hence term(HM(p,O)) = HT(p,O) by A1,A3,POLYNOM7:8; end; hence thesis by A2; end; Lm9: for n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L st HC(p,O) <> 0.L holds HT(p,O) in Support(HM(p,O)) proof let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; assume HC(p,O) <> 0.L; then p.(HT(p,O)) <> 0.L by Def7; then (HM(p,O)).(HT(p,O)) <> 0.L by Lm8; hence thesis by POLYNOM1:def 9; end; Lm10: for n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L st HC(p,O) = 0.L holds Support(HM(p,O)) = {} proof let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; assume A1: HC(p,O) = 0.L; then A2: p = 0_(n,L) by Lm7; then Support p = {} by POLYNOM7:1; then A3: HT(p,O) = EmptyBag n by Def6; then HM(p,O) = Monom(0.L,EmptyBag n) by A1,Def8; then A4: term(HM(p,O)) = EmptyBag n by POLYNOM7:8; now assume Support(HM(p,O)) <> {}; then Support(HM(p,O)) = {term(HM(p,O))} by POLYNOM7:7; then term(HM(p,O)) in Support(HM(p,O)) by TARSKI:def 1; then (HM(p,O)).EmptyBag n <> 0.L by A4,POLYNOM1:def 9; then p.(HT(p,O)) <> 0.L by A3,Lm8; hence contradiction by A2,POLYNOM1:81; end; hence thesis; end; definition let n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n,L; cluster HM(p,T) -> non-zero; coherence proof set O = T; now per cases; case HC(p,O) <> 0.L; then HT(p,O) in Support(HM(p,O)) by Lm9; then HM(p,O) <> 0_(n,L) by POLYNOM7:1; hence thesis by POLYNOM7:def 2; case HC(p,O) = 0.L; then p = 0_(n,L) by Lm7; hence thesis by POLYNOM7:def 2; end; hence thesis; end; cluster HC(p,T) -> non-zero; coherence proof set O = T, a = HC(p,O); now assume a = 0.L; then p.(HT(p,O)) = 0.L by Def7; then not(HT(p,O)) in Support p by POLYNOM1:def 9; then Support p = {} by Def6; then p = 0_(n,L) by POLYNOM7:1; hence contradiction by POLYNOM7:def 2; end; hence thesis by RLVECT_1:def 13; end; end; Lm11: for n being Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, m being Monomial of n,L holds HT(m,O) = term(m) & HC(m,O) = coefficient(m) & HM(m,O) = m proof let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, m be Monomial of n,L; per cases by POLYNOM7:6; suppose A1: Support m = {}; hence A2: term(m) = EmptyBag n by POLYNOM7:def 6 .= HT(m,O) by A1,Def6; hence HC(m,O) = m.(term(m)) by Def7 .= coefficient(m) by POLYNOM7:def 7; hence HM(m,O) = Monom(coefficient(m),term(m)) by A2,Def8 .= m by POLYNOM7:11; suppose A3: ex b being bag of n st Support m = {b}; then consider b being bag of n such that A4: Support m = {b}; b in Support m by A4,TARSKI:def 1; then A5: m.b <> 0.L by POLYNOM1:def 9; HT(m,O) in Support m by A3,Def6; hence A6: HT(m,O) = b by A4,TARSKI:def 1 .= term(m) by A5,POLYNOM7:def 6; hence HC(m,O) = m.(term(m)) by Def7 .= coefficient(m) by POLYNOM7:def 7; hence HM(m,O) = Monom(coefficient(m),term(m)) by A6,Def8 .= m by POLYNOM7:11; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds HC(p,T) = 0.L iff p = 0_(n,L) by Lm7; theorem for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds (HM(p,T)).(HT(p,T)) = p.(HT(p,T)) by Lm8; theorem Th19: for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L, b being bag of n st b <> HT(p,T) holds HM(p,T).b = 0.L proof let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L, b being bag of n; assume A1: b <> HT(p,O); per cases by POLYNOM7:6; suppose Support HM(p,O) = {}; then HM(p,O) = 0_(n,L) by POLYNOM7:1; hence thesis by POLYNOM1:81; suppose ex b being bag of n st Support HM(p,O) = {b}; then consider b1 being bag of n such that A2: Support HM(p,O) = {b1}; A3: b1 is Element of Bags n & b is Element of Bags n by POLYNOM1:def 14; now per cases; case HC(p,O) <> 0.L; then HT(p,O) in {b1} by A2,Lm9; then b1 <> b by A1,TARSKI:def 1; then not(b in {b1}) by TARSKI:def 1; hence HM(p,O).b = 0.L by A2,A3,POLYNOM1:def 9; case HC(p,O) = 0.L; then Support(HM(p,O)) = {} by Lm10; then HM(p,O) = 0_(n,L) by POLYNOM7:1; hence HM(p,O).b = 0.L by POLYNOM1:81; end; hence thesis; end; Lm12: for n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L holds Support(HM(p,O)) = {} or Support(HM(p,O)) = {HT(p,O)} proof let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; assume A1: not(Support(HM(p,O)) = {}); then consider b being bag of n such that A2: Support(HM(p,O)) = {b} by POLYNOM7:6; now per cases; case HC(p,O) = 0.L; hence thesis by A1,Lm10; case HC(p,O) <> 0.L; then HT(p,O) in Support HM(p,O) by Lm9; hence thesis by A2,TARSKI:def 1; end; hence thesis; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds Support(HM(p,T)) c= Support(p) proof let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; now let u be set; assume A1: u in Support(HM(p,O)); now per cases by A1,Lm12; case u in {}; hence u in Support p; case u in {HT(p,O)}; then A2: u = HT(p,O) by TARSKI:def 1; now per cases; case HC(p,O) = 0.L; then p = 0_(n,L) by Lm7; then p.(HT(p,O)) = 0.L by POLYNOM1:81; then (HM(p,O)).(HT(p,O)) = 0.L by Lm8; hence contradiction by A1,A2,POLYNOM1:def 9; case HC(p,O) <> 0.L; then p.(HT(p,O)) <> 0.L by Def7; hence u in Support p by A2,POLYNOM1:def 9; end; hence u in Support p; end; hence u in Support p; end; hence thesis by TARSKI:def 3; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds Support(HM(p,T)) = {} or Support(HM(p,T)) = {HT(p,T)} by Lm12; theorem for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds term(HM(p,T)) = HT(p,T) & coefficient(HM(p,T)) = HC(p,T) proof let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; A1: HM(p,O) = Monom(HC(p,O),HT(p,O)) by Def8; per cases; suppose HC(p,O) is non-zero; then reconsider a = HC(p,O) as non-zero Element of L; term(Monom(a,HT(p,O))) = HT(p,O) by POLYNOM7:10; hence thesis by A1,POLYNOM7:9; suppose A2: not(HC(p,O) is non-zero); now per cases; case not(p is non-zero); then p = 0_(n,L) by POLYNOM7:def 2; then Support p = {} by POLYNOM7:1; then HT(p,O) = EmptyBag n by Def6 .= term(Monom(0.L,HT(p,O))) by POLYNOM7:8 .= term(Monom(HC(p,O),HT(p,O))) by A2,RLVECT_1:def 13 .= term(HM(p,O)) by Def8; hence thesis by A1,POLYNOM7:9; case p is non-zero; then reconsider p as non-zero Polynomial of n,L; HC(p,O) is non-zero; hence thesis by A2; end; hence thesis; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, m being Monomial of n,L holds HT(m,T) = term(m) & HC(m,T) = coefficient(m) & HM(m,T) = m by Lm11; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, c being ConstPoly of n,L holds HT(c,T) = EmptyBag n & HC(c,T) = c.(EmptyBag n) proof let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, c be ConstPoly of n,L; thus HT(c,O) = term(c) by Lm11 .= EmptyBag n by POLYNOM7:16; thus HC(c,O) = coefficient(c) by Lm11 .= c.(EmptyBag n) by POLYNOM7:16; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, a being Element of L holds HT(a _(n,L),T) = EmptyBag n & HC(a _(n,L),T) = a proof let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, a be Element of L; set p = a _(n,L); thus HT(p,O) = term(p) by Lm11 .= EmptyBag n by POLYNOM7:23; thus HC(p,O) = coefficient(p) by Lm11 .= a by POLYNOM7:23; end; theorem Th26: for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds HT(HM(p,T),T) = HT(p,T) proof let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n,L; per cases; suppose HC(p,O) is non-zero; then reconsider a = HC(p,O) as non-zero Element of L; thus HT(HM(p,O),O) = HT(Monom(HC(p,O),HT(p,O)),O) by Def8 .= term(Monom(a,HT(p,O))) by Lm11 .= HT(p,O) by POLYNOM7:10; suppose A1: not(HC(p,O) is non-zero); now per cases; case not(p is non-zero); then p = 0_(n,L) by POLYNOM7:def 2; then Support p = {} by POLYNOM7:1; then HT(p,O) = EmptyBag n by Def6 .= term(Monom(0.L,HT(p,O))) by POLYNOM7:8 .= term(Monom(HC(p,O),HT(p,O))) by A1,RLVECT_1:def 13 .= term(HM(p,O)) by Def8; hence thesis by Lm11; case p is non-zero; then reconsider p as non-zero Polynomial of n,L; HC(p,O) is non-zero; hence thesis by A1; end; hence thesis; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being Polynomial of n,L holds HC(HM(p,T),T) = HC(p,T) proof let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p being Polynomial of n,L; thus HC(HM(p,O),O) = (HM(p,O)).(HT(HM(p,O),O)) by Def7 .= (HM(p,O)).(HT(p,O)) by Th26 .= p.(HT(p,O)) by Lm8 .= HC(p,O) by Def7; end; theorem for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds HM(HM(p,T),T) = HM(p,T) by Lm11; Lm13: for X being set, S being Subset of X, R being Order of X st R is_linear-order holds R linearly_orders S proof let X be set, S be Subset of X, R be Order of X; assume R is_linear-order; then A1: R linearly_orders field R by ORDERS_2:35; S c= X; then S c= field R by ORDERS_2:2; hence thesis by A1,ORDERS_2:36; end; Lm14: for n being Ordinal, O be admissible connected TermOrder of n, L being add-associative right_complementable left_zeroed right_zeroed unital distributive (non trivial doubleLoopStr), p,q being non-zero Polynomial of n,L holds (p*'q).(HT(p,O) + HT(q,O)) = p.(HT(p,O)) * q.(HT(q,O)) proof let n be Ordinal, O be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed left_zeroed unital distributive (non trivial doubleLoopStr), p,q be non-zero Polynomial of n,L; set b = HT(p,O) + HT(q,O); consider s being FinSequence of the carrier of L such that A1: (p*'q).b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by POLYNOM1:def 26; consider S being non empty finite Subset of Bags n such that A2: divisors b = SgmX(BagOrder n, S) & for p being bag of n holds p in S iff p divides b by POLYNOM1:def 18; HT(p,O) divides b by POLYNOM1:54; then A3: HT(p,O) in S by A2; set sgm = SgmX(BagOrder n, S); BagOrder n linearly_orders S by Lm13; then HT(p,O) in rng(sgm) by A3,TRIANG_1:def 2; then consider i being set such that A4: i in dom sgm & sgm.i = HT(p,O) by FUNCT_1:def 5; A5: i in dom decomp b by A2,A4,POLYNOM1:def 19; (divisors b)/.i = HT(p,O) by A2,A4,FINSEQ_4:def 4; then A6: (decomp b)/.i = <*HT(p,O), b-'HT(p,O)*> by A5,POLYNOM1:def 19; then A7: (decomp b)/.i = <*HT(p,O), HT(q,O)*> by POLYNOM1:52; A8: dom s = Seg(len decomp b) by A1,FINSEQ_1:def 3 .= dom(decomp b) by FINSEQ_1:def 3; then A9: i in dom s by A2,A4,POLYNOM1:def 19; reconsider i as Nat by A4; A10:now let k be Nat; assume A11: k in dom s & k <> i; then consider b1', b2' being bag of n such that A12: (decomp b)/.k = <*b1', b2'*> & b = b1'+b2' by A8,POLYNOM1:72; consider b1,b2 being bag of n such that A13: (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by A1,A11; A14: b1 = <*b1', b2'*>.1 by A12,A13,FINSEQ_1:61 .= b1' by FINSEQ_1:61; A15: b2 = <*b1', b2'*>.2 by A12,A13,FINSEQ_1:61 .= b2' by FINSEQ_1:61; A16: now assume A17: p.b1 <> 0.L & q.b2 <> 0.L; b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14; then b1 in Support p & b2 in Support q by A17,POLYNOM1:def 9; then b1 <= HT(p,O),O & b2 <= HT(q,O),O by Def6; then A18: [b1,HT(p,O)] in O & [b2,HT(q,O)] in O by Def2; A19: now assume b1 = HT(p,O) & b2 = HT(q,O); then (decomp b).k = <*HT(p,O), HT(q,O)*> by A8,A11,A13,FINSEQ_4:def 4 .= (decomp b)/.i by A6,POLYNOM1:52 .= (decomp b).i by A5,FINSEQ_4:def 4; hence contradiction by A5,A8,A11,FUNCT_1:def 8; end; now per cases by A19; case A20: b1 <> HT(p,O); A21: now assume b1+b2 = HT(p,O)+b2; then b1 = (HT(p,O)+b2)-'b2 by POLYNOM1:52; hence contradiction by A20,POLYNOM1:52; end; A22: [HT(p,O)+HT(q,O), HT(p,O)+b2] in O by A12,A14,A15,A18,BAGORDER:def 7; A23: [HT(p,O)+b2, HT(p,O)+HT(q,O)] in O by A18,BAGORDER:def 7; HT(p,O)+b2 is Element of Bags n & HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14; hence contradiction by A12,A14,A15,A21,A22,A23,ORDERS_1:13; case A24: b2 <> HT(q,O); A25: now assume b2+b1 = HT(q,O)+b1; then b2 = (HT(q,O)+b1)-'b1 by POLYNOM1:52; hence contradiction by A24,POLYNOM1:52; end; A26: [HT(p,O)+HT(q,O), HT(q,O)+b1] in O by A12,A14,A15,A18,BAGORDER:def 7; A27: [HT(q,O)+b1, HT(p,O)+HT(q,O)] in O by A18,BAGORDER:def 7; HT(q,O)+b1 is Element of Bags n & HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14; hence contradiction by A12,A14,A15,A25,A26,A27,ORDERS_1:13; end; hence contradiction; end; now per cases by A16; case p.b1 = 0.L; hence p.b1*q.b2 = 0.L by BINOM:1; case q.b2 = 0.L; hence p.b1*q.b2 = 0.L by BINOM:2; end; hence s/.k = 0.L by A13; end; consider b1,b2 being bag of n such that A28: (decomp b)/.i = <*b1, b2*> & s/.i = p.b1*q.b2 by A1,A9; A29: b1 = <*HT(p,O), HT(q,O)*>.1 by A7,A28,FINSEQ_1:61 .= HT(p,O) by FINSEQ_1:61; b2 = <*HT(p,O), HT(q,O)*>.2 by A7,A28,FINSEQ_1:61 .= HT(q,O) by FINSEQ_1:61; hence thesis by A1,A9,A10,A28,A29,POLYNOM2:5; end; theorem Th29: for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable left_zeroed right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q being non-zero Polynomial of n,L holds HT(p,T) + HT(q,T) in Support(p*'q) proof let n be Ordinal, O be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed left_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q be non-zero Polynomial of n,L; p <> 0_(n,L) & q <> 0_(n,L) by POLYNOM7:def 2; then Support p <> {} & Support q <> {} by POLYNOM7:1; then HT(p,O) in Support p & HT(q,O) in Support q by Def6; then A1: p.(HT(p,O)) <> 0.L & q.(HT(q,O)) <> 0.L by POLYNOM1:def 9; set b = HT(p,O) + HT(q,O); A2: b is Element of Bags n by POLYNOM1:def 14; assume not(HT(p,O) + HT(q,O) in Support(p*'q)); then (p*'q).(HT(p,O) + HT(q,O)) = 0.L by A2,POLYNOM1:def 9; then p.(HT(p,O)) * q.(HT(q,O)) = 0.L by Lm14; hence thesis by A1,VECTSP_2:def 5; end; theorem Th30: for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p,q being Polynomial of n,L holds Support(p*'q) c= {s + t where s,t is Element of Bags n : s in Support p & t in Support q} proof let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p,q be Polynomial of n,L; A1: now let b be bag of n; assume A2: b in Support(p*'q); then A3: (p*'q).b <> 0.L by POLYNOM1:def 9; consider s being FinSequence of the carrier of L such that A4: (p*'q).b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by POLYNOM1:def 26; A5: dom s = Seg(len decomp b) by A4,FINSEQ_1:def 3 .= dom(decomp b) by FINSEQ_1:def 3; now per cases; case dom s = {}; then len s = 0 by FINSEQ_1:4,def 3; then s = <*>(the carrier of L) by FINSEQ_1:32; hence contradiction by A3,A4,RLVECT_1:60; case A6: dom s <> {}; consider k being Element of dom s; k in dom s by A6; then reconsider k as Nat; now assume A7: not( ex k being Element of dom(decomp b), b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*> & p.b1 <> 0.L & q.b2 <> 0.L); A8: for k being Nat st k in dom s holds s/.k = 0.L proof let k be Nat; assume A9: k in dom s; then consider b1, b2 being bag of n such that A10: (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by A4; now per cases by A5,A7,A9,A10; case p.b1 = 0.L; hence 0.L = s/.k by A10,BINOM:1; case q.b2 = 0.L; hence 0.L = s/.k by A10,BINOM:2; end; hence thesis; end; then for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L; then Sum s = s/.k by A6,POLYNOM2:5 .= 0.L by A6,A8; hence contradiction by A2,A4,POLYNOM1:def 9; end; then consider k being Element of dom(decomp b), b1,b2 being bag of n such that A11: (decomp b)/.k = <*b1, b2*> & p.b1 <> 0.L & q.b2 <> 0.L; k in dom(decomp b) by A5,A6; then reconsider k as Nat; b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14; then A12: b1 in Support p & b2 in Support q by A11,POLYNOM1:def 9; consider b1', b2' being bag of n such that A13: (decomp b)/.k = <*b1', b2'*> & b = b1'+b2' by A5,A6,POLYNOM1:72; A14: b1' = <*b1, b2*>.1 by A11,A13,FINSEQ_1:61 .= b1 by FINSEQ_1:61; b2' = <*b1, b2*>.2 by A11,A13,FINSEQ_1:61 .= b2 by FINSEQ_1:61; hence ex s,t being bag of n st s in Support p & t in Support q & b = s+t by A12,A13,A14; end; hence ex s,t being bag of n st s in Support p & t in Support q & b = s+t; end; now let u be set; assume A15: u in Support(p*'q); then reconsider u' = u as Element of Bags n; consider s,t being bag of n such that A16: s in Support p & t in Support q & u' = s+t by A1,A15; thus u in {s' + t' where s',t' is Element of Bags n : s' in Support p & t' in Support q} by A16; end; hence thesis by TARSKI:def 3; end; theorem Th31: ::: lemma 5.17 (i), p. 195 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q being non-zero Polynomial of n,L holds HT(p*'q,T) = HT(p,T) + HT(q,T) proof let n be Ordinal, O be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q be non-zero Polynomial of n,L; Support p*'q <> {} by Th29; then A1: HT(p*'q,O) in Support(p*'q) by Def6; HT(p,O) + HT(q,O) in Support(p*'q) by Th29; then HT(p,O) + HT(q,O) <= HT(p*'q,O),O by Def6; then A2: [HT(p,O) + HT(q,O),HT(p*'q,O)] in O by Def2; Support(p*'q) c= {s + t where s,t is Element of Bags n : s in Support p & t in Support q} by Th30; then HT(p*'q,O) in {s + t where s,t is Element of Bags n : s in Support p & t in Support q} by A1; then consider s,t being Element of Bags n such that A3: HT(p*'q,O) = s + t & s in Support p & t in Support q; s <= HT(p,O),O & t <= HT(q,O),O by A3,Def6; then A4: [s,HT(p,O)] in O & [t,HT(q,O)] in O by Def2; A5: s + t is Element of Bags n & HT(p,O) + t is Element of Bags n & HT(p*'q,O) is Element of Bags n & HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14; A6: [s + t,HT(p,O) + t] in O by A4,BAGORDER:def 7; [t + HT(p,O), HT(p,O)+HT(q,O)] in O by A4,BAGORDER:def 7; then [s + t,HT(p,O)+HT(q,O)] in O by A5,A6,ORDERS_1:14; hence thesis by A2,A3,A5,ORDERS_1:13; end; theorem Th32: ::: lemma 5.17 (iii), p. 195 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q being non-zero Polynomial of n,L holds HC(p*'q,T) = HC(p,T) * HC(q,T) proof let n be Ordinal, O being admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q be non-zero Polynomial of n,L; thus HC(p*'q,O) = (p*'q).(HT(p*'q,O)) by Def7 .= (p*'q).(HT(p,O) + HT(q,O)) by Th31 .= p.(HT(p,O)) * q.(HT(q,O)) by Lm14 .= HC(p,O) * q.(HT(q,O)) by Def7 .= HC(p,O) * HC(q,O) by Def7; end; theorem ::: lemma 5.17 (ii), p. 195 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q being non-zero Polynomial of n,L holds HM(p*'q,T) = HM(p,T) *' HM(q,T) proof let n be Ordinal, O being admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q be non-zero Polynomial of n,L; thus HM(p*'q,O) = Monom(HC(p*'q,O),HT(p*'q,O)) by Def8 .= Monom(HC(p,O) * HC(q,O),HT(p*'q,O)) by Th32 .= Monom(HC(p,O) * HC(q,O),HT(p,O) + HT(q,O)) by Th31 .= Monom(HC(p,O),HT(p,O)) *' Monom(HC(q,O),HT(q,O)) by Th3 .= HM(p,O) *' Monom(HC(q,O),HT(q,O)) by Def8 .= HM(p,O) *' HM(q,O) by Def8; end; theorem ::: lemma 5.17 (iv), p. 195 for n being Ordinal, T being admissible connected TermOrder of n, L being right_zeroed (non empty LoopStr), p,q being Polynomial of n,L holds HT(p+q,T) <= max(HT(p,T),HT(q,T),T), T proof let n be Ordinal, O being admissible connected TermOrder of n, L be right_zeroed (non empty LoopStr), p,q be Polynomial of n,L; per cases; suppose A1: HT(p+q,O) in Support(p+q); A2: Support(p+q) c= Support p \/ Support q by POLYNOM1:79; now per cases by A1,A2,XBOOLE_0:def 2; case A3: HT(p+q,O) in Support(p); then A4: HT(p+q,O) <= HT(p,O),O by Def6; now per cases by Th12; case max(HT(p,O),HT(q,O),O) = HT(p,O); hence thesis by A3,Def6; case A5: max(HT(p,O),HT(q,O),O) = HT(q,O); then HT(p,O) <= HT(q,O),O by Th14; hence thesis by A4,A5,Th8; end; hence thesis; case A6: HT(p+q,O) in Support(q); then A7: HT(p+q,O) <= HT(q,O),O by Def6; now per cases by Th12; case max(HT(p,O),HT(q,O),O) = HT(q,O); hence thesis by A6,Def6; case A8: max(HT(p,O),HT(q,O),O) = HT(p,O); then HT(q,O) <= HT(p,O),O by Th14; hence thesis by A7,A8,Th8; end; hence thesis; end; hence thesis; suppose not(HT(p+q,O) in Support(p+q)); then Support(p+q) = {} & HT(p+q,O) = EmptyBag n by Def6; then [HT(p+q,O),max(HT(p,O),HT(q,O),O)] in O by BAGORDER:def 7; hence thesis by Def2; end; begin :: Reductum definition ::: definition 5.15, p. 194 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed (non empty LoopStr), p be Polynomial of n,L; func Red(p,T) -> Polynomial of n,L equals :Def9: p - HM(p,T); coherence; end; Lm15: for n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds not(HT(p,O) in Support(Red(p,O))) proof let n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L; assume HT(p,O) in Support(Red(p,O)); then (Red(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 9; then (p - HM(p,O)).(HT(p,O)) <> 0.L by Def9; then (p + -HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 23; then p.(HT(p,O)) + (-HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 21; then A1: p.(HT(p,O)) + -HM(p,O).(HT(p,O)) <> 0.L by POLYNOM1:def 22; HM(p,O).(HT(p,O)) = p.(HT(p,O)) by Lm8; hence thesis by A1,RLVECT_1:def 10; end; Lm16: for n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L, b being bag of n st b in Support p & b <> HT(p,O) holds b in Support(Red(p,O)) proof let n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L, b being bag of n; assume A1: b in Support p & b <> HT(p,O); A2: b is Element of Bags n by POLYNOM1:def 14; (Red(p,O)).b = (p - HM(p,O)).b by Def9 .= (p + -HM(p,O)).b by POLYNOM1:def 23 .= p.b + (-HM(p,O)).b by POLYNOM1:def 21 .= p.b + -HM(p,O).b by POLYNOM1:def 22 .= p.b + - 0.L by A1,Th19 .= p.b + 0.L by RLVECT_1:25 .= p.b by RLVECT_1:10; then (Red(p,O)).b <> 0.L by A1,POLYNOM1:def 9; hence thesis by A2,POLYNOM1:def 9; end; Lm17: for n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds Support(Red(p,O)) = Support(p) \ {HT(p,O)} proof let n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L; A1: now let u be set; assume u in Support(p) \ {HT(p,O)}; then A2: u in Support p & not(u in {HT(p,O)}) by XBOOLE_0:def 4; then reconsider u' = u as Element of Bags n; reconsider u' as bag of n; u' <> HT(p,O) by A2,TARSKI:def 1; hence u in Support(Red(p,O)) by A2,Lm16; end; now let u be set; assume A3: u in Support(Red(p,O)); then A4: u in Support(p - HM(p,O)) by Def9; reconsider u' = u as Element of Bags n by A3; reconsider u' as bag of n; A5: (p - HM(p,O)).u' <> 0.L by A4,POLYNOM1:def 9; A6: (p + -HM(p,O)).u' = p.u' + (-HM(p,O)).u' by POLYNOM1:def 21 .= p.u' + -HM(p,O).u' by POLYNOM1:def 22; A7: not(u' = HT(p,O)) by A3,Lm15; then (p + -HM(p,O)).u' = p.u' + - 0.L by A6,Th19 .= p.u' + 0.L by RLVECT_1:25 .= p.u' by RLVECT_1:10; then p.u' <> 0.L by A5,POLYNOM1:def 23; then A8: u' in Support p by POLYNOM1:def 9; not(u' in {HT(p,O)}) by A7,TARSKI:def 1; hence u in Support(p) \ {HT(p,O)} by A8,XBOOLE_0:def 4; end; hence thesis by A1,TARSKI:2; end; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds Support(Red(p,T)) c= Support(p) proof let n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L; Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17; hence thesis by XBOOLE_1:36; end; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds Support(Red(p,T)) = Support(p) \ {HT(p,T)} by Lm17; Lm18: for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds (Red(p,T)).(HT(p,T)) = 0.L proof let n be Ordinal, O being connected TermOrder of n, L be add-associative right_complementable right_zeroed (non trivial LoopStr), p be Polynomial of n,L; A1: HT(p,O) in {HT(p,O)} by TARSKI:def 1; Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17; then not(HT(p,O) in Support(Red(p,O))) by A1,XBOOLE_0:def 4; hence thesis by POLYNOM1:def 9; end; Lm19: for n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L, b being bag of n st b <> HT(p,O) holds (Red(p,O)).b = p.b proof let n be Ordinal, O being connected TermOrder of n, L be add-associative right_complementable right_zeroed (non trivial LoopStr), p be Polynomial of n,L, b be bag of n; assume b <> HT(p,O); then not(b in {HT(p,O)}) by TARSKI:def 1; then A1: not(b in Support(HM(p,O))) by Lm12; A2: b is Element of Bags n by POLYNOM1:def 14; thus (Red(p,O)).b = (p - HM(p,O)).b by Def9 .= (p + -HM(p,O)).b by POLYNOM1:def 23 .= p.b + (-HM(p,O)).b by POLYNOM1:def 21 .= p.b + -(HM(p,O)).b by POLYNOM1:def 22 .= p.b + -0.L by A1,A2,POLYNOM1:def 9 .= p.b + 0.L by RLVECT_1:25 .= p.b by RLVECT_1:10; end; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds Support(HM(p,T) + Red(p,T)) = Support p proof let n being Ordinal, O being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L; A1: now let u be set; assume A2: u in Support p; then reconsider u' = u as Element of Bags n; reconsider u' as bag of n; A3: p.u' <> 0.L by A2,POLYNOM1:def 9; now per cases; case A4: u' = HT(p,O); then p.(HT(p,O)) <> 0.L by A2,POLYNOM1:def 9; then A5: HC(p,O) <> 0.L by Def7; (HM(p,O) + Red(p,O)).u' = HM(p,O).u' + Red(p,O).u' by POLYNOM1:def 21 .= HM(p,O).u' + 0.L by A4,Lm18 .= HM(p,O).u' by RLVECT_1:10 .= p.(HT(p,O)) by A4,Lm8 .= HC(p,O) by Def7; hence u' in Support(HM(p,O) + Red(p,O)) by A5,POLYNOM1:def 9; case A6: u' <> HT(p,O); (HM(p,O) + Red(p,O)).u' = HM(p,O).u' + Red(p,O).u' by POLYNOM1:def 21 .= HM(p,O).u' + p.u' by A6,Lm19 .= 0.L + p.u' by A6,Th19 .= p.u' by RLVECT_1:10; hence u' in Support(HM(p,O) + Red(p,O)) by A3,POLYNOM1:def 9; end; hence u in Support(HM(p,O) + Red(p,O)); end; now let u be set; assume A7: u in Support(HM(p,O) + Red(p,O)); then reconsider u' = u as Element of Bags n; reconsider u' as bag of n; A8: (HM(p,O) + Red(p,O)).u' <> 0.L by A7,POLYNOM1:def 9; now per cases; case A9: u' = HT(p,O); (HM(p,O) + Red(p,O)).u' = HM(p,O).u' + Red(p,O).u' by POLYNOM1:def 21 .= HM(p,O).HT(p,O) + 0.L by A9,Lm18 .= HM(p,O).HT(p,O) by RLVECT_1:10 .= p.u' by A9,Lm8; hence u' in Support p by A8,POLYNOM1:def 9; case A10: u' <> HT(p,O); (HM(p,O) + Red(p,O)).u' = HM(p,O).u' + Red(p,O).u' by POLYNOM1:def 21 .= 0.L + Red(p,O).u' by A10,Th19 .= Red(p,O).u' by RLVECT_1:10 .= p.u by A10,Lm19; hence u' in Support p by A8,POLYNOM1:def 9; end; hence u in Support p; end; hence thesis by A1,TARSKI:2; end; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds HM(p,T) + Red(p,T) = p proof let n be Ordinal, O being connected TermOrder of n, L be add-associative right_complementable right_zeroed (non trivial LoopStr), p be Polynomial of n,L; A1: dom p = Bags n & dom(HM(p,O) + Red(p,O)) = Bags n by FUNCT_2:def 1; now let x be set; assume x in Bags n; then reconsider x' = x as Element of Bags n; now per cases; case A2: x = HT(p,O); hence (HM(p,O) + Red(p,O)).x = HM(p,O).HT(p,O) + Red(p,O).HT(p,O) by POLYNOM1:def 21 .= HM(p,O).HT(p,O) + 0.L by Lm18 .= HM(p,O).HT(p,O) by RLVECT_1:10 .= p.x by A2,Lm8; case A3: x <> HT(p,O); now thus (HM(p,O) + Red(p,O)).x' = HM(p,O).x' + Red(p,O).x' by POLYNOM1:def 21 .= HM(p,O).x' + p.x' by A3,Lm19 .= 0.L + p.x' by A3,Th19 .= p.x' by RLVECT_1:10; end; hence p.x = (HM(p,O) + Red(p,O)).x; end; hence p.x = (HM(p,O) + Red(p,O)).x; end; hence thesis by A1,FUNCT_1:9; end; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds (Red(p,T)).(HT(p,T)) = 0.L by Lm18; theorem for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L, b being bag of n st b in Support p & b <> HT(p,T) holds (Red(p,T)).b = p.b by Lm19;