:: Term Orders
:: by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2026 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, ZFMISC_1, ALGSTR_0, VECTSP_1, RLVECT_1, PRE_POLY,
XCMPLX_0, ARYTM_3, FUNCT_1, XXREAL_0, ARYTM_1, CARD_1, XBOOLE_0,
SUBSET_1, RELAT_1, PBOOLE, TARSKI, ORDINAL1, LATTICES, POLYNOM1,
FINSEQ_1, CARD_3, PARTFUN1, NAT_1, SUPINF_2, POLYNOM7, STRUCT_0,
VECTSP_2, CAT_3, BAGORDER, RELAT_2, WELLORD1, FINSET_1, BROUWER,
VALUED_0, ORDERS_1, ALGSTR_1, TERMORD;
notations ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1, ORDERS_1,
RELAT_1, CARD_1, BAGORDER, RELSET_1, FUNCT_1, PARTFUN1, FINSET_1,
XXREAL_0, ALGSTR_1, PBOOLE, FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_0,
RLVECT_1, VFUNCT_1, XTUPLE_0, MCART_1, VECTSP_1, VECTSP_2, RELAT_2,
POLYNOM1, NAT_D, WELLORD1, POLYNOM7;
constructors VECTSP_2, ALGSTR_1, TRIANG_1, POLYNOM7, BAGORDER, WELLORD2,
RELSET_1, POLYNOM1, BINOP_2, VFUNCT_1, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, NAT_1, CARD_1,
FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, POLYNOM7,
BAGORDER, VALUED_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, POLYNOM1, NAT_1,
RLVECT_1, VECTSP_2, POLYNOM7, POLYNOM2, NAT_2, RELAT_2, CARD_1, CARD_2,
MATRLIN, XBOOLE_0, XBOOLE_1, ORDERS_1, BAGORDER, WELLORD1, XREAL_1,
PARTFUN1, VALUED_0, STRUCT_0, XREAL_0, PRE_POLY, XTUPLE_0;
schemes NAT_1;
begin :: Preliminaries
registration
cluster non trivial for addLoopStr;
existence
proof
take the Field;
thus thesis;
end;
end;
registration
cluster add-associative right_complementable right_zeroed for non trivial
addLoopStr;
existence
proof
set F = the Field;
take F;
thus thesis;
end;
end;
definition
let X be set, b be bag of X;
attr b is 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 object;
b1.k <= b2.k by A1,PRE_POLY:def 11;
then b1.k - b1.k <= b2.k - b1.k by XREAL_1:9;
hence 0 <= b2.k - b1.k;
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;
end;
case
n <> {};
then reconsider n9 = n as non empty set;
set b = the set of all [k,b2.k -' b1.k] where k is Element of n9 ;
A4: now
let x be object;
assume x in b;
then ex k being Element of n9 st x = [k,b2.k -' b1.k];
hence ex y,z being object st x = [y,z];
end;
now
let x,y1,y2 be object;
assume that
A5: [x,y1] in b and
A6: [x,y2] in b;
consider k being Element of n9 such that
A7: [x,y1] = [k,b2.k -' b1.k] by A5;
consider k9 being Element of n9 such that
A8: [x,y2] = [k9,b2.k9 -' b1.k9] by A6;
k = x by A7,XTUPLE_0:1
.= k9 by A8,XTUPLE_0:1;
hence y1 = y2 by A7,A8,XTUPLE_0:1;
end;
then reconsider b as Function by A4,FUNCT_1:def 1,RELAT_1:def 1;
A9: now
let x be object;
assume x in dom b;
then consider y being object such that
A10: [x,y] in b by XTUPLE_0:def 12;
consider k being Element of n9 such that
A11: [x,y] = [k,b2.k -' b1.k] by A10;
x = k by A11,XTUPLE_0:1;
hence x in n9;
end;
now
let x be object;
assume x in n9;
then reconsider k = x as Element of n9;
[k,b2.k -' b1.k] in b;
hence x in dom b by XTUPLE_0:def 12;
end;
then
A12: dom b = n9 by A9,TARSKI:2;
then reconsider b as ManySortedSet of n9 by PARTFUN1:def 2
,RELAT_1:def 18;
A13: now
let k be set;
assume k in n;
then consider u being object such that
A14: [k,u] in b by A12,XTUPLE_0:def 12;
consider k9 being Element of n9 such that
A15: [k,u] = [k9,b2.k9 -' b1.k9] by A14;
A16: u = b2.k9 -' b1.k9 by A15,XTUPLE_0:1;
k = k9 by A15,XTUPLE_0:1;
hence b.k = b2.k -' b1.k by A14,A16,FUNCT_1:1;
end;
now
let x be object;
A17: support b c= dom b by PRE_POLY:37;
assume
A18: x in support b;
then
A19: b.x <> 0 by PRE_POLY:def 7;
now
assume not x in support b2;
then b2.x = 0 by PRE_POLY:def 7;
then 0 = b2.x-'b1.x by NAT_2:8;
hence contradiction by A12,A13,A18,A19,A17;
end;
hence x in support b2;
end;
then
A20: support b c= support b2;
now
let x be object;
assume x in rng b;
then consider y be object such that
A21: [y,x] in b by XTUPLE_0:def 13;
consider k being Element of n9 such that
A22: [y,x] = [k,b2.k -' b1.k] by A21;
x = b2.k -' b1.k by A22,XTUPLE_0:1;
hence x in NAT;
end;
then rng b c= NAT;
then reconsider b as bag of n by A20,PRE_POLY:def 8,VALUED_0:def 6;
take b;
now
let k be object;
A23: 0 <= b2.k - b1.k by A2;
assume k in n;
hence b1.k + b.k = b1.k + (b2.k -' b1.k) by A13
.= b1.k + (b2.k + -b1.k) by A23,XREAL_0:def 2
.= b2.k;
end;
then b2 = b1 + b by PRE_POLY:33;
hence ex b being bag of n st b2 = b1 + b;
end;
end;
hence ex b being bag of n st b2 = b1 + b;
end;
hence thesis by PRE_POLY:50;
end;
theorem Th2:
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-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
well-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 L such that
A1: (Z*'p).b = Sum s and
len s = len decomp b and
A2: for k being Element of 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 10;
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:22
.= 0.L;
end;
then Sum s = 0.L by MATRLIN:11;
hence (Z*'p).b = Z.b by A1,POLYNOM1:22;
end;
hence thesis by FUNCT_2:63;
end;
registration
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-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;
end;
suppose
A1: Support(m1*'m2) <> {};
now
per cases;
case
A2: Support(m1) <> {} & Support(m2) <> {};
then consider mb2 being bag of n such that
A3: Support(m2) = {mb2} by POLYNOM7:6;
mb2 in Support m2 by A3,TARSKI:def 1;
then
A4: m2.mb2 <> 0.L by POLYNOM1:def 4;
A5: now
let b be bag of n;
assume
A6: b <> mb2;
consider b9 being bag of n such that
A7: for b being bag of n st b <> b9 holds m2.b = 0.L by POLYNOM7:def 3;
b9 = mb2 by A4,A7;
hence m2.b = 0.L by A6,A7;
end;
consider mb1 being bag of n such that
A8: Support(m1) = {mb1} by A2,POLYNOM7:6;
mb1 in Support m1 by A8,TARSKI:def 1;
then
A9: m1.mb1 <> 0.L by POLYNOM1:def 4;
A10: now
let b be bag of n;
assume
A11: b <> mb1;
consider b9 being bag of n such that
A12: for b being bag of n st b <> b9 holds m1.b = 0.L by POLYNOM7:def 3;
b9 = mb1 by A9,A12;
hence m1.b = 0.L by A11,A12;
end;
set b = the 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 L such that
A14: (m1*'m2).b = Sum s and
A15: len s = len decomp b and
A16: for k being Element of 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 10;
A17: dom s = Seg(len decomp b) by A15,FINSEQ_1:def 3
.= dom(decomp b) by FINSEQ_1:def 3;
A18: now
assume
A19: b <> mb1 + mb2;
A20: now
let k be Element of NAT;
assume
A21: k in dom s;
then consider b1,b2 being bag of n such that
A22: (decomp b)/.k = <*b1, b2*> and
A23: s/.k = m1.b1*m2.b2 by A16;
consider b19,b29 being bag of n such that
A24: (decomp b)/.k = <*b19,b29*> and
A25: b = b19+b29 by A17,A21,PRE_POLY:68;
A26: b2 = <*b19, b29*>.2 by A22,A24
.= b29;
A27: b1 = <*b19, b29*>.1 by A22,A24
.= b19;
now
per cases by A19,A25,A27,A26;
case
b1 <> mb1;
then m1.b1 = 0.L by A10;
hence m1.b1*m2.b2 = 0.L;
end;
case
b2 <> mb2;
then m2.b2 = 0.L by A5;
hence m1.b1*m2.b2 = 0.L;
end;
end;
hence s/.k = 0.L by A23;
end;
now
per cases;
case
dom s = {};
then s = <*>(the carrier of L) by RELAT_1:41;
hence (m1*'m2).b = 0.L by A15;
end;
case
A28: dom s <> {};
set k = the Element of dom s;
A29: k in dom s by A28;
for k9 being Element of NAT st k9 in dom s & k9 <> k
holds s/.k9 = 0.L by A20;
then s/.k = (m1*'m2).b by A14,A29,POLYNOM2:3;
hence (m1*'m2).b = 0.L by A20,A29;
end;
end;
hence contradiction by A13,POLYNOM1:def 4;
end;
now
let b9 be bag of n;
assume
A30: b9 <> b;
consider s being FinSequence of L such that
A31: (m1*'m2).b9 = Sum s and
A32: len s = len decomp b9 and
A33: for k being Element of NAT st k in dom s ex b1, b2 being
bag of n st (decomp b9)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 10
;
A34: dom s = Seg(len decomp b9) by A32,FINSEQ_1:def 3
.= dom(decomp b9) by FINSEQ_1:def 3;
A35: now
let k be Element of NAT;
assume
A36: k in dom s;
then consider b1, b2 being bag of n such that
A37: (decomp b9)/.k = <*b1,b2*> and
A38: s/.k = m1.b1*m2.b2 by A33;
consider b19,b29 being bag of n such that
A39: (decomp b9)/.k = <*b19,b29*> and
A40: b9 = b19+b29 by A34,A36,PRE_POLY:68;
A41: b2 = <*b19, b29*>.2 by A37,A39
.= b29;
A42: b1 = <*b19, b29*>.1 by A37,A39
.= b19;
now
per cases by A18,A30,A40,A42,A41;
case
b1 <> mb1;
then m1.b1 = 0.L by A10;
hence m1.b1*m2.b2 = 0.L;
end;
case
b2 <> mb2;
then m2.b2 = 0.L by A5;
hence m1.b1*m2.b2 = 0.L;
end;
end;
hence s/.k = 0.L by A38;
end;
now
per cases;
case
dom s = {};
then s = <*>(the carrier of L) by RELAT_1:41;
hence (m1*'m2).b9 = 0.L by A32;
end;
case
A43: dom s <> {};
set k = the Element of dom s;
A44: k in dom s by A43;
for k9 being Element of NAT st k9 in dom s & k9 <> k
holds s/.k9 = 0.L by A35;
then s/.k = (m1*'m2).b9 by A31,A44,POLYNOM2:3;
hence (m1*'m2).b9 = 0.L by A35,A44;
end;
end;
hence (m1*'m2).b9 = 0.L;
end;
hence thesis by POLYNOM7:def 3;
end;
case
A45: Support(m1) = {} or Support(m2) = {};
now
per cases by A45;
case
Support(m1) = {};
then m1 = 0_(n,L) by POLYNOM7:1;
hence thesis by Th2;
end;
case
Support(m2) = {};
then m2 = 0_(n,L) by POLYNOM7:1;
hence thesis by POLYNOM1:28;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
end;
registration
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 L such that
A2: p.b = Sum s and
A3: len s = len decomp b and
A4: for k being Element of 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 10;
A5: dom s = Seg len decomp b by A3,FINSEQ_1:def 3
.= dom decomp b by FINSEQ_1:def 3;
A6: now
let k be Element of NAT;
assume
A7: k in dom s;
then consider b1, b2 being bag of n such that
A8: (decomp b)/.k = <*b1,b2*> and
A9: s/.k = c1.b1*c2.b2 by A4;
consider b19,b29 being bag of n such that
A10: (decomp b)/.k = <*b19,b29*> and
A11: b = b19+b29 by A5,A7,PRE_POLY:68;
A12: b2 = <*b19, b29*>.2 by A8,A10
.= b29;
b1 = <*b19, b29*>.1 by A8,A10
.= b19;
then
A13: b1 <> EmptyBag n or b2 <> EmptyBag n by A1,A11,A12,PRE_POLY:53;
now
per cases by A13,POLYNOM7:def 7;
case
c1.b1 = 0.L;
hence s/.k = 0.L by A9;
end;
case
c2.b2 = 0.L;
hence s/.k = 0.L by A9;
end;
end;
hence s/.k = 0.L;
end;
now
per cases;
case
dom s = {};
then s = <*>(the carrier of L) by RELAT_1:41;
hence p.b = 0.L by A3;
end;
case
A14: dom s <> {};
set k = the Element of dom s;
A15: k in dom s by A14;
for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.
k9 = 0.L by A6;
then Sum s = s/.k by A15,POLYNOM2:3;
hence p.b = 0.L by A2,A6,A15;
end;
end;
hence p.b = 0.L;
end;
hence thesis by POLYNOM7:def 7;
end;
end;
theorem Th3:
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
b,b9 being bag of n, a,a9 being non zero Element of L holds Monom(a * a9,b + b9
) = Monom(a,b) *' Monom(a9,b9)
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, b,b9 be bag
of n, a,a9 be non zero Element of L;
set m1 = Monom(a,b), m2 = Monom(a9,b9);
set m = Monom(a * a9,b + b9);
set m3 = m1 *' m2;
consider s being FinSequence of L such that
A1: m3.(b+b9) = Sum s and
A2: len s = len decomp(b+b9) and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
st (decomp(b+b9))/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 10;
set u = b+b9;
consider k9 being Element of NAT such that
A4: k9 in dom decomp u and
A5: (decomp u)/.k9 = <*b,b9*> by PRE_POLY:69;
A6: dom s = Seg(len decomp(b+b9)) by A2,FINSEQ_1:def 3
.= dom(decomp(b+b9)) by FINSEQ_1:def 3;
then consider b1,b2 being bag of n such that
A7: (decomp u)/.k9 = <*b1, b2*> and
A8: s/.k9 = m1.b1*m2.b2 by A3,A4;
A9: b1 = <*b,b9*>.1 by A5,A7,FINSEQ_1:44
.= b;
A10: b2 = <*b,b9*>.2 by A5,A7,FINSEQ_1:44
.= b9;
A11: m2.b9 = m2.(term(m2)) by POLYNOM7:10
.= coefficient(m2) by POLYNOM7:def 6
.= a9 by POLYNOM7:9;
A12: now
A13: m2.b9 <> 0.L by A11;
let u be bag of n;
assume
A14: u <> b9;
consider v being bag of n such that
A15: for b9 being bag of n st b9 <> v holds m2.b9 = 0.L by POLYNOM7:def 3;
assume m2.u <> 0.L;
then u = v by A15;
hence contradiction by A14,A15,A13;
end;
a * a9 <> 0.L by VECTSP_2:def 1;
then
A16: a * a9 is non zero by STRUCT_0:def 12;
A17: m1.b = m1.(term(m1)) by POLYNOM7:10
.= coefficient(m1) by POLYNOM7:def 6
.= a by POLYNOM7:9;
A18: now
A19: m1.b <> 0.L by A17;
let u be bag of n;
assume
A20: u <> b;
consider v being bag of n such that
A21: for b9 being bag of n st b9 <> v holds m1.b9 = 0.L by POLYNOM7:def 3;
assume m1.u <> 0.L;
then u = v by A21;
hence contradiction by A20,A21,A19;
end;
A22: now
let k be Element of NAT;
assume that
A23: k in dom s and
A24: k <> k9;
consider b1,b2 being bag of n such that
A25: (decomp u)/.k = <*b1, b2*> and
A26: s/.k = m1.b1*m2.b2 by A3,A23;
A27: now
assume
A28: b1 = b & b2 = b9;
(decomp u).k = (decomp u)/.k by A6,A23,PARTFUN1:def 6
.= (decomp u).k9 by A4,A5,A25,A28,PARTFUN1:def 6;
hence contradiction by A6,A4,A23,A24,FUNCT_1:def 4;
end;
now
per cases by A27;
case
b1 <> b;
then m1.b1 = 0.L by A18;
hence m1.b1 * m2.b2 = 0.L;
end;
case
b2 <> b9;
then m2.b2 = 0.L by A12;
hence m1.b1*m2.b2 = 0.L;
end;
end;
hence s/.k = 0.L by A26;
end;
then Sum s = s/.k9 by A6,A4,POLYNOM2:3;
then
A29: m3.(b+b9) <> 0.L by A17,A11,A1,A8,A9,A10,VECTSP_2:def 1;
then
A30: term(m3) = b + b9 by POLYNOM7:def 5
.= term(m) by A16,POLYNOM7:10;
A31: coefficient(m3) = m3.(term m3) by POLYNOM7:def 6
.= m3.(b+b9) by A29,POLYNOM7:def 5
.= a * a9 by A17,A11,A1,A6,A4,A8,A9,A10,A22,POLYNOM2:3
.= coefficient(m) by POLYNOM7:9;
thus m = Monom(coefficient(m),term(m)) by POLYNOM7:11
.= m3 by A30,A31,POLYNOM7:11;
end;
theorem
for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
a,a9 being Element of L holds (a * a9) |(n,L) = (a |(n,L)) *' (a9 |(n,L))
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, a,a9 be
Element of L;
per cases;
suppose
A1: a is non zero & a9 is non zero;
term((a*a9) |(n,L)) = EmptyBag n & coefficient((a*a9) |(n,L)) = a*a9
by POLYNOM7:23;
then
A2: (a * a9) |(n,L) = Monom(a*a9,EmptyBag n) by POLYNOM7:11;
term(a9 |(n,L)) = EmptyBag n & coefficient(a9 |(n,L)) = a9 by POLYNOM7:23;
then
A3: a9 |(n,L) = Monom(a9,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 PRE_POLY:53;
hence thesis by A1,A2,A4,A3,Th3;
end;
suppose
A5: not(a is non zero & a9 is non zero);
now
per cases by A5,STRUCT_0:def 12;
case
A6: a = 0.L;
then a * a9 = 0.L;
then
A7: (a * a9) |(n,L) = 0_(n,L) by POLYNOM7:19;
a |(n,L) = 0_(n,L) by A6,POLYNOM7:19;
hence thesis by A7,Th2;
end;
case
A8: a9 = 0.L;
then a * a9 = 0.L;
then
A9: (a * a9) |(n,L) = 0_(n,L) by POLYNOM7:19;
a9 |(n,L) = 0_(n,L) by A8,POLYNOM7:19;
hence thesis by A9,POLYNOM1:28;
end;
end;
hence thesis;
end;
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 3;
suppose
b in dom T;
then b is Element of Bags n;
hence thesis;
end;
suppose
b in rng T;
then b is Element of Bags n;
hence thesis;
end;
end;
registration
let n be Ordinal;
cluster admissible connected for TermOrder of n;
existence
proof
set T = LexOrder n;
take T;
now
let x,y be object;
assume that
A1: x in field T & y in field T and
x <> y;
reconsider b1 = x, b2 = y as bag of n by A1,Lm1;
b1 <=' b2 or b2 <=' b1 by PRE_POLY:45;
hence [x,y] in T or [y,x] in T by PRE_POLY:def 14;
end;
then T is_connected_in field T by RELAT_2:def 6;
hence thesis by RELAT_2:def 14;
end;
end;
:: theorem 5.5 (ii), p. 190
registration
let n be Nat;
cluster -> well_founded for admissible TermOrder of n;
coherence
proof
let T be admissible TermOrder of n;
T is well-ordering by BAGORDER:34;
hence thesis by WELLORD1:def 4;
end;
end;
definition
let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
pred b <= b9,T means
[b,b9] in T;
end;
definition
let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
pred b < b9,T means
b <= b9,T & b <> b9;
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:12;
then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
b is Element of Bags n by PRE_POLY:def 12;
then [b,b] in T by A1,RELAT_2:def 1;
hence thesis;
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;
field T = Bags n by ORDERS_1:12;
then
A1: T is_antisymmetric_in Bags n by RELAT_2:def 12;
assume b1 <= b2,T & b2 <= b1,T;
then
A2: [b1,b2] in T & [b2,b1] in T;
b1 is Element of Bags n & b2 is Element of Bags n by PRE_POLY:def 12;
hence thesis by A2,A1,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:12;
then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
b is Element of Bags n by PRE_POLY:def 12;
then [b,b] in T by A1,RELAT_2:def 1;
hence thesis by RELAT_1:15;
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 Lm2;
end;
suppose
A2: b1 <> b2;
A3: not b2 < b1,T implies b1 <= b2,T
proof
assume
A4: not b2 < b1,T;
now
per cases by A4;
case
A5: not b2 <= b1,T;
A6: b1 in field T & b2 in field T by Lm4;
not [b2,b1] in T by A5;
then [b1,b2] in T by A1,A2,A6,RELAT_2:def 6;
hence thesis;
end;
case
b1 = b2;
hence thesis by A2;
end;
end;
hence thesis;
end;
b1 <= b2,T implies not b2 < b1,T
by Lm3;
hence thesis by A3;
end;
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:12;
then
A3: T is_reflexive_in Bags n by RELAT_2:def 9;
b1 is Element of Bags n by PRE_POLY:def 12;
then [b1,b2] in T by A2,A3,RELAT_2:def 1;
hence thesis;
end;
suppose
A4: b1 <> b2;
assume not b1 <= b2,T;
then
A5: not [b1,b2] in T;
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;
end;
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;
A1: b3 is Element of Bags n by PRE_POLY:def 12;
field T = Bags n by ORDERS_1:12;
then
A2: T is_transitive_in Bags n by RELAT_2:def 16;
assume b1 <= b2,T & b2 <= b3,T;
then
A3: [b1,b2] in T & [b2,b3] in T;
b1 is Element of Bags n & b2 is Element of Bags n by PRE_POLY:def 12;
then [b1,b3] in T by A3,A2,A1,RELAT_2:def 8;
hence thesis;
end;
theorem Th9:
for n being Ordinal, T being admissible TermOrder of n, b being
bag of n holds EmptyBag n <= b,T
by BAGORDER:def 5;
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;
then [EmptyBag n + b1,b2] in T by A1,BAGORDER:def 5;
then [b1,b2] in T by PRE_POLY:53;
hence thesis;
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 thesis by Def4;
end;
case
b1 = b2;
then b1 <= b2,T by Lm2;
hence contradiction by A1,Def4;
end;
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 thesis by Def5;
end;
case
b1 = b2;
then b2 <= b1,T by Lm2;
hence contradiction by A1,Def5;
end;
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
by Def4,Def5;
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;
end;
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;
end;
case
b1 <> b2;
then b2 < b1,T by A2;
then not b1 <= b2,T by Th5;
then min(b1,b2,T) = b2 by Def4;
hence thesis by A2,Lm2;
end;
end;
hence thesis;
end;
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;
end;
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;
end;
case
b1 <> b2;
then b1 < b2,T by A2;
then not b2 <= b1,T by Th5;
then max(b1,b2,T) = b2 by Def5;
hence thesis by A2,Lm2;
end;
end;
hence thesis;
end;
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);
end;
case
b1 <> b2;
then not b2 <= b1,T by A2,Lm3;
hence min(b2,b1,T) = min(b1,b2,T) by A1,Def4;
end;
end;
hence min(b1,b2,T) = min(b2,b1,T);
end;
case
b1 = b2;
hence min(b2,b1,T) = min(b1,b2,T);
end;
end;
hence min(b1,b2,T) = min(b2,b1,T);
end;
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;
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);
end;
case
b1 <> b2;
then not b1 <= b2,T by A6,Lm3;
hence max(b2,b1,T) = max(b1,b2,T) by A5,Def5;
end;
end;
hence thesis;
end;
case
b1 = b2;
hence max(b2,b1,T) = max(b1,b2,T);
end;
end;
hence thesis;
end;
case
A7: max(b1,b2,T) <> b1;
now
per cases by Lm5;
case
b1 <= b2,T;
hence max(b2,b1,T) = b2 by Def5
.= max(b1,b2,T) by A7,Th12;
end;
case
b2 <= b1,T;
hence max(b2,b1,T) = max(b1,b2,T) by A7,Def5;
end;
end;
hence max(b2,b1,T) = max(b1,b2,T);
end;
end;
hence thesis;
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: max(b1,b2,T) = b2;
now
per cases by A2,Def5;
case
not b2 <= b1,T;
then b1 <= b2,T by Lm5;
hence min(b1,b2,T) = b1 by Def4;
end;
case
b1 = b2;
hence min(b1,b2,T) = b1 by Th11;
end;
end;
hence min(b1,b2,T) = b1;
end;
now
assume
A3: min(b1,b2,T) = b1;
now
per cases by A3,Def4;
case
b1 <= b2,T;
then max(b2,b1,T) = b2 by Def5;
hence max(b1,b2,T) = b2 by Th15;
end;
case
b1 = b2;
hence max(b1,b2,T) = b2 by Th12;
end;
end;
hence max(b1,b2,T) = b2;
end;
hence thesis by A1;
end;
begin :: Headterms, Headmonomials and Headcoefficients
definition
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;
end;
suppose
A1: Support p <> {};
reconsider sp = Support p as finite set by POLYNOM1:def 5;
card sp is finite;
then consider m being Nat such that
A2: card(Support p) = card m by CARD_1:48;
reconsider sp = Support p as finite Subset of Bags n by POLYNOM1:def 5;
defpred P[Nat] means for B being finite Subset of Bags n st card B = $1
holds ex b9 being bag of n st b9 in B & for b being bag of n st b in B holds [b
,b9] in O;
A3: for k being Nat st 1 <= k holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A4: 1 <= k;
thus P[k] implies P[k+1]
proof
assume
A5: P[k];
thus P[k+1]
proof
let B be finite Subset of Bags n;
assume
A6: card B = k+1;
then reconsider B as non empty finite Subset of Bags n;
set x = the Element of B;
reconsider x as Element of Bags n;
reconsider x as bag of n;
set X = B \ {x};
now
let u be object;
assume u in {x};
then u = x by TARSKI:def 1;
hence u in B;
end;
then {x} c= B;
then
A7: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ X by XBOOLE_1:39;
x in X iff x in B & not x in {x} by XBOOLE_0:def 5;
then
A8: card(X) + 1 = k + 1 by A6,A7,CARD_2:41,TARSKI:def 1;
then reconsider X as non empty set by A4;
consider b9 being bag of n such that
A9: b9 in X and
A10: for b being bag of n st b in X holds [b,b9] in O by A5,A8;
A11: O is_connected_in field O by RELAT_2:def 14;
now
per cases;
case
A12: x = b9;
A13: now
let b be bag of n;
assume
A14: b in B;
now
per cases;
case
b in X;
hence [b,b9] in O by A10;
end;
case
not b in X;
then b in {x} by A7,A14,XBOOLE_0:def 3;
then b = x by TARSKI:def 1;
hence [b,b9] in O by A12,ORDERS_1:3;
end;
end;
hence [b,b9] in O;
end;
take b9;
X c= B by XBOOLE_1:36;
hence thesis by A9,A13;
end;
case
A15: x <> b9;
b9 is Element of Bags n by PRE_POLY:def 12;
then [b9,b9] in O by ORDERS_1:3;
then
A16: b9 in field O by RELAT_1:15;
[x,x] in O by ORDERS_1:3;
then
A17: x in field O by RELAT_1:15;
now
per cases by A11,A15,A17,A16,RELAT_2:def 6;
case
A18: [x,b9] in O;
thus ex b9 being bag of n st b9 in B & for b being bag of
n st b in B holds [b,b9] in O
proof
take b9;
for b being bag of n st b in B holds [b,b9] in O
proof
let b be bag of n;
assume
A19: b in B;
now
per cases;
case
b <> x;
then not b in {x} by TARSKI:def 1;
then b in X by A19,XBOOLE_0:def 5;
hence thesis by A10;
end;
case
b = x;
hence thesis by A18;
end;
end;
hence thesis;
end;
hence thesis by A9,XBOOLE_0:def 5;
end;
end;
case
A20: [b9,x] in O;
thus ex b9 being bag of n st b9 in B & for b being bag of
n st b in B holds [b,b9] 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
A21: b in B;
now
per cases;
case
b <> x;
then not b in {x} by TARSKI:def 1;
then b in X by A21,XBOOLE_0:def 5;
then
A22: [b,b9] in O by A10;
b is Element of Bags n & b9 is Element of
Bags n by PRE_POLY:def 12;
hence thesis by A20,A22,ORDERS_1:5;
end;
case
b = x;
hence thesis by ORDERS_1:3;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
end;
m <> 0 by A1,A2;
then
A23: 1 <= m by NAT_1:14;
A24: card(Support p) = m by A2;
A25: P[1]
proof
let B be finite Subset of Bags n;
assume card B = 1;
then card {{}} = card B by CARD_1:30;
then consider b being object such that
A26: B = {b} by CARD_1:29;
A27: b in B by A26,TARSKI:def 1;
then reconsider b as Element of Bags n;
reconsider b as bag of n;
now
let b9 be bag of n;
assume b9 in B;
then b9 = b by A26,TARSKI:def 1;
hence [b9,b] in O by ORDERS_1:3;
end;
hence thesis by A27;
end;
for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A25,A3);
then consider b9 being bag of n such that
A28: b9 in sp and
A29: for b being bag of n st b in sp holds [b,b9] in O by A24,A23;
take b9;
for b be bag of n st b in sp holds b <= b9,O by A29;
hence thesis by A28;
end;
end;
uniqueness
proof
let b1,b2 be Element of Bags n;
set O = T;
assume
A30: 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
A31: 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 A30,A31;
end;
suppose
A32: Support p <> {};
then b1 <= b2,O by A30,A31;
then
A33: [b1,b2] in O;
b2 <= b1,O by A30,A31,A32;
then [b2,b1] in O;
hence b1 = b2 by A33,ORDERS_1:4;
end;
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
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
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;
now
assume HC(p,O) = 0.L;
then not HT(p,O) in Support p by POLYNOM1:def 4;
then Support p = {} by Def6;
hence p = 0_(n,L) by POLYNOM7:1;
end;
hence thesis by POLYNOM1:22;
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: now
per cases;
case
HC(p,O) <> 0.L;
then HC(p,O) is non zero by STRUCT_0:def 12;
hence term(HM(p,O)) = HT(p,O) by POLYNOM7:10;
end;
case
A2: 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 A2,POLYNOM7:8;
end;
end;
p.(HT(p,O)) = coefficient(HM(p,O)) by POLYNOM7:9
.= (HM(p,O)).term(HM(p,O)) by POLYNOM7:def 6;
hence thesis by A1;
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 (HM(p,O)).(HT(p,O)) <> 0.L by Lm8;
hence thesis by POLYNOM1:def 4;
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 p = 0_(n,L) by Lm7;
then Support p = {} by POLYNOM7:1;
then
A2: HT(p,O) = EmptyBag n by Def6;
A3: term(HM(p,O)) = EmptyBag n by A1,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 A3,POLYNOM1:def 4;
hence contradiction by A1,A2,Lm8;
end;
hence thesis;
end;
registration
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 1;
end;
case
HC(p,O) = 0.L;
then p = 0_(n,L) by Lm7;
hence thesis by POLYNOM7:def 1;
end;
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 not(HT(p,O)) in Support p by POLYNOM1:def 4;
then Support p = {} by Def6;
then p = 0_(n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def 1;
end;
hence thesis by STRUCT_0:def 12;
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 5
.= HT(m,O) by A1,Def6;
hence HC(m,O) = coefficient(m) by POLYNOM7:def 6;
hence thesis by A2,POLYNOM7:11;
end;
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 4;
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 5;
hence HC(m,O) = coefficient(m) by POLYNOM7:def 6;
hence thesis by A6,POLYNOM7:11;
end;
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:22;
end;
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: b is Element of Bags n by PRE_POLY:def 12;
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 thesis by A2,A3,POLYNOM1:def 4;
end;
case
HC(p,O) = 0.L;
then Support(HM(p,O)) = {} by Lm10;
then HM(p,O) = 0_(n,L) by POLYNOM7:1;
hence thesis by POLYNOM1:22;
end;
end;
hence thesis;
end;
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
A2: ex b being bag of n st Support(HM(p,O)) = {b} by POLYNOM7:6;
now
per cases;
case
HC(p,O) = 0.L;
hence thesis by A1,Lm10;
end;
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;
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;
let u be object;
assume
A1: u in Support(HM(p,O));
now
per cases by A1,Lm12;
case
u in {};
hence u in Support p;
end;
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 (HM(p,O)).(HT(p,O)) = 0.L by Lm8;
hence contradiction by A1,A2,POLYNOM1:def 4;
end;
case
HC(p,O) <> 0.L;
hence u in Support p by A2,POLYNOM1:def 4;
end;
end;
hence u in Support p;
end;
end;
hence u in Support p;
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;
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 POLYNOM7:9;
end;
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 1;
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(HM(p,O)) by A1,STRUCT_0:def 12;
hence thesis by POLYNOM7:9;
end;
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;
end;
hence thesis;
end;
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) = term(Monom(a,HT(p,O))) by Lm11
.= HT(p,O) by POLYNOM7:10;
end;
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 1;
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(HM(p,O)) by A1,STRUCT_0:def 12;
hence thesis by Lm11;
end;
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;
end;
hence thesis;
end;
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(p,O)) by Th26
.= HC(p,O) by Lm8;
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
being_linear-order holds R linearly_orders S
proof
let X be set, S be Subset of X, R be Order of X;
S c= X;
then
A1: S c= field R by ORDERS_1:15;
assume R is being_linear-order;
hence thesis by A1,ORDERS_1:37,38;
end;
Lm14: for n being Ordinal, O be admissible connected TermOrder of n, L being
add-associative right_complementable left_zeroed right_zeroed well-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 well-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 L such that
A1: (p*'q).b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of 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 10;
consider S being non empty finite Subset of Bags n such that
A4: divisors b = SgmX(BagOrder n, S) and
A5: for p being bag of n holds p in S iff p divides b by PRE_POLY:def 16;
set sgm = SgmX(BagOrder n, S);
A6: BagOrder n linearly_orders S by Lm13;
HT(p,O) divides b by PRE_POLY:50;
then HT(p,O) in S by A5;
then HT(p,O) in rng(sgm) by A6,PRE_POLY:def 2;
then consider i being object such that
A7: i in dom sgm and
A8: sgm.i = HT(p,O) by FUNCT_1:def 3;
A9: i in dom decomp b by A4,A7,PRE_POLY:def 17;
(divisors b)/.i = HT(p,O) by A4,A7,A8,PARTFUN1:def 6;
then
A10: (decomp b)/.i = <*HT(p,O), b-'HT(p,O)*> by A9,PRE_POLY:def 17;
then
A11: (decomp b)/.i = <*HT(p,O), HT(q,O)*> by PRE_POLY:48;
A12: dom s = Seg(len decomp b) by A2,FINSEQ_1:def 3
.= dom(decomp b) by FINSEQ_1:def 3;
then
A13: i in dom s by A4,A7,PRE_POLY:def 17;
reconsider i as Element of NAT by A7;
consider b1,b2 being bag of n such that
A14: (decomp b)/.i = <*b1, b2*> and
A15: s/.i = p.b1*q.b2 by A3,A13;
A16: b2 = <*HT(p,O), HT(q,O)*>.2 by A11,A14,FINSEQ_1:44
.= HT(q,O);
A17: now
let k be Element of NAT;
assume that
A18: k in dom s and
A19: k <> i;
consider b1,b2 being bag of n such that
A20: (decomp b)/.k = <*b1, b2*> and
A21: s/.k = p.b1*q.b2 by A3,A18;
consider b19, b29 being bag of n such that
A22: (decomp b)/.k = <*b19, b29*> and
A23: b = b19+b29 by A12,A18,PRE_POLY:68;
A24: b2 = <*b19, b29*>.2 by A22,A20,FINSEQ_1:44
.= b29;
A25: b1 = <*b19, b29*>.1 by A22,A20,FINSEQ_1:44
.= b19;
A26: now
assume that
A27: p.b1 <> 0.L and
A28: q.b2 <> 0.L;
b1 is Element of Bags n by PRE_POLY:def 12;
then b1 in Support p by A27,POLYNOM1:def 4;
then b1 <= HT(p,O),O by Def6;
then
A29: [b1,HT(p,O)] in O;
b2 is Element of Bags n by PRE_POLY:def 12;
then b2 in Support q by A28,POLYNOM1:def 4;
then b2 <= HT(q,O),O by Def6;
then
A30: [b2,HT(q,O)] in O;
A31: now
assume b1 = HT(p,O) & b2 = HT(q,O);
then (decomp b).k = <*HT(p,O), HT(q,O)*> by A12,A18,A20,PARTFUN1:def 6
.= (decomp b)/.i by A10,PRE_POLY:48
.= (decomp b).i by A9,PARTFUN1:def 6;
hence contradiction by A9,A12,A18,A19,FUNCT_1:def 4;
end;
now
per cases by A31;
case
A32: b1 <> HT(p,O);
A33: now
assume b1+b2 = HT(p,O)+b2;
then b1 = (HT(p,O)+b2)-'b2 by PRE_POLY:48;
hence contradiction by A32,PRE_POLY:48;
end;
A34: HT(p,O)+b2 is Element of Bags n & HT(p,O)+HT(q,O) is Element of
Bags n by PRE_POLY:def 12;
[HT(p,O)+HT(q,O), HT(p,O)+b2] in O & [HT(p,O)+b2, HT(p,O)+HT(q,
O)] in O by A23,A25,A24,A29,A30,BAGORDER:def 5;
hence contradiction by A23,A25,A24,A33,A34,ORDERS_1:4;
end;
case
A35: b2 <> HT(q,O);
A36: now
assume b2+b1 = HT(q,O)+b1;
then b2 = (HT(q,O)+b1)-'b1 by PRE_POLY:48;
hence contradiction by A35,PRE_POLY:48;
end;
A37: HT(q,O)+b1 is Element of Bags n & HT(p,O)+HT(q,O) is Element of
Bags n by PRE_POLY:def 12;
[HT(p,O)+HT(q,O), HT(q,O)+b1] in O & [HT(q,O)+b1, HT(p,O)+HT(q,
O)] in O by A23,A25,A24,A29,A30,BAGORDER:def 5;
hence contradiction by A23,A25,A24,A36,A37,ORDERS_1:4;
end;
end;
hence contradiction;
end;
now
per cases by A26;
case
p.b1 = 0.L;
hence p.b1*q.b2 = 0.L;
end;
case
q.b2 = 0.L;
hence p.b1*q.b2 = 0.L;
end;
end;
hence s/.k = 0.L by A21;
end;
b1 = <*HT(p,O), HT(q,O)*>.1 by A11,A14,FINSEQ_1:44
.= HT(p,O);
hence thesis by A1,A13,A17,A15,A16,POLYNOM2:3;
end;
theorem Th29:
for n being Ordinal, T being admissible connected TermOrder of n
, L being add-associative right_complementable left_zeroed right_zeroed
well-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 well-unital
distributive domRing-like non trivial doubleLoopStr, p,q be non-zero
Polynomial of n,L;
set b = HT(p,O) + HT(q,O);
assume
A1: not HT(p,O) + HT(q,O) in Support(p*'q);
p <> 0_(n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then HT(p,O) in Support p by Def6;
then
A2: p.(HT(p,O)) <> 0.L by POLYNOM1:def 4;
q <> 0_(n,L) by POLYNOM7:def 1;
then Support q <> {} by POLYNOM7:1;
then HT(q,O) in Support q by Def6;
then
A3: q.(HT(q,O)) <> 0.L by POLYNOM1:def 4;
b is Element of Bags n by PRE_POLY:def 12;
then (p*'q).(HT(p,O) + HT(q,O)) = 0.L by A1,POLYNOM1:def 4;
then p.(HT(p,O)) * q.(HT(q,O)) = 0.L by Lm14;
hence thesis by A2,A3,VECTSP_2:def 1;
end;
theorem Th30:
for n being Ordinal, L being add-associative
right_complementable right_zeroed well-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
well-unital distributive non empty doubleLoopStr, p,q be Polynomial of n,L;
A1: now
let b be bag of n;
consider s being FinSequence of L such that
A2: (p*'q).b = Sum s and
A3: len s = len decomp b and
A4: for k being Element of 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 10;
A5: dom s = Seg(len decomp b) by A3,FINSEQ_1:def 3
.= dom(decomp b) by FINSEQ_1:def 3;
assume
A6: b in Support(p*'q);
now
per cases;
case
dom s = {};
then Seg len s = {} by FINSEQ_1:def 3;
then len s = 0;
hence contradiction by A3;
end;
case
A7: dom s <> {};
set k = the Element of dom s;
k in dom s by A7;
then reconsider k as Element of NAT;
now
assume
A8: 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);
A9: for k being Nat st k in dom s holds s/.k = 0.L
proof
let k be Nat;
assume
A10: k in dom s;
then consider b1, b2 being bag of n such that
A11: (decomp b)/.k = <*b1, b2*> and
A12: s/.k = p.b1*q.b2 by A4;
now
per cases by A5,A8,A10,A11;
case
p.b1 = 0.L;
hence thesis by A12;
end;
case
q.b2 = 0.L;
hence thesis by A12;
end;
end;
hence thesis;
end;
then for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.
k9 = 0.L;
then Sum s = s/.k by A7,POLYNOM2:3
.= 0.L by A7,A9;
hence contradiction by A6,A2,POLYNOM1:def 4;
end;
then consider
k being Element of dom(decomp b), b1,b2 being bag of n such
that
A13: (decomp b)/.k = <*b1, b2*> and
A14: p.b1 <> 0.L and
A15: q.b2 <> 0.L;
k in dom(decomp b) by A5,A7;
then reconsider k as Element of NAT;
consider b19, b29 being bag of n such that
A16: (decomp b)/.k = <*b19, b29*> and
A17: b = b19+b29 by A5,A7,PRE_POLY:68;
A18: b29 = <*b1, b2*>.2 by A13,A16,FINSEQ_1:44
.= b2;
b2 is Element of Bags n by PRE_POLY:def 12;
then
A19: b2 in Support q by A15,POLYNOM1:def 4;
b1 is Element of Bags n by PRE_POLY:def 12;
then
A20: b1 in Support p by A14,POLYNOM1:def 4;
b19 = <*b1, b2*>.1 by A13,A16,FINSEQ_1:44
.= b1;
hence
ex s,t being bag of n st s in Support p & t in Support q & b = s+
t by A20,A19,A17,A18;
end;
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 object;
assume
A21: u in Support(p*'q);
then reconsider u9 = u as Element of Bags n;
ex s,t being bag of n st s in Support p & t in Support q & u9 = s+t by A1
,A21;
hence
u in {s9 + t9 where s9,t9 is Element of Bags n : s9 in Support p & t9
in Support q};
end;
hence thesis;
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 well-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 well-unital distributive
domRing-like non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
A1: HT(p,O)+HT(q,O) is Element of Bags n by PRE_POLY:def 12;
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;
Support p*'q <> {} by Th29;
then
A3: HT(p*'q,O) in Support(p*'q) by Def6;
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 A3;
then consider s,t being Element of Bags n such that
A4: HT(p*'q,O) = s + t and
A5: s in Support p and
A6: t in Support q;
s <= HT(p,O),O by A5,Def6;
then [s,HT(p,O)] in O;
then
A7: [s + t,HT(p,O) + t] in O by BAGORDER:def 5;
t <= HT(q,O),O by A6,Def6;
then [t,HT(q,O)] in O;
then
A8: [t + HT(p,O), HT(p,O)+HT(q,O)] in O by BAGORDER:def 5;
s + t is Element of Bags n & HT(p,O) + t is Element of Bags n by
PRE_POLY:def 12;
then [s + t,HT(p,O)+HT(q,O)] in O by A1,A7,A8,ORDERS_1:5;
hence thesis by A2,A4,A1,ORDERS_1:4;
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 well-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 well-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,O) + HT(q,O)) by Th31
.= HC(p,O) * HC(q,O) by Lm14;
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 well-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 well-unital distributive
domRing-like non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
thus HM(p*'q,O) = 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
.= HM(p,O) *' HM(q,O) by Th3;
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 addLoopStr, 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 addLoopStr, 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:20;
now
per cases by A1,A2,XBOOLE_0:def 3;
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;
end;
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;
end;
hence thesis;
end;
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;
end;
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;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not HT(p+q,O) in Support(p+q);
then 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 5;
hence thesis;
end;
end;
begin :: Reductum
definition
let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed non empty addLoopStr, p be Polynomial of n,
L;
func Red(p,T) -> Polynomial of n,L equals
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 addLoopStr, 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 addLoopStr, 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 4;
then (p + -HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 7;
then p.(HT(p,O)) + (-HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:15;
then
A1: p.(HT(p,O)) + -HM(p,O).(HT(p,O)) <> 0.L by POLYNOM1:17;
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 addLoopStr, 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 addLoopStr, p
being Polynomial of n,L, b being bag of n;
assume that
A1: b in Support p and
A2: b <> HT(p,O);
(Red(p,O)).b = (p + -HM(p,O)).b by POLYNOM1:def 7
.= p.b + (-HM(p,O)).b by POLYNOM1:15
.= p.b + -HM(p,O).b by POLYNOM1:17
.= p.b + - 0.L by A2,Th19
.= p.b + 0.L by RLVECT_1:12
.= p.b by RLVECT_1:4;
then b is Element of Bags n & (Red(p,O)).b <> 0.L by A1,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
Lm17: for n being Ordinal, O being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, 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 addLoopStr, p
being Polynomial of n,L;
A1: now
let u be object;
assume
A2: u in Support(Red(p,O));
then reconsider u9 = u as Element of Bags n;
reconsider u9 as bag of n;
A3: (p - HM(p,O)).u9 <> 0.L by A2,POLYNOM1:def 4;
A4: not u9 = HT(p,O) by A2,Lm15;
(p + -HM(p,O)).u9 = p.u9 + (-HM(p,O)).u9 by POLYNOM1:15
.= p.u9 + -HM(p,O).u9 by POLYNOM1:17;
then (p + -HM(p,O)).u9 = p.u9 + - 0.L by A4,Th19
.= p.u9 + 0.L by RLVECT_1:12
.= p.u9 by RLVECT_1:4;
then p.u9 <> 0.L by A3,POLYNOM1:def 7;
then
A5: u9 in Support p by POLYNOM1:def 4;
not u9 in {HT(p,O)} by A4,TARSKI:def 1;
hence u in Support(p) \ {HT(p,O)} by A5,XBOOLE_0:def 5;
end;
now
let u be object;
assume
A6: u in Support(p) \ {HT(p,O)};
then reconsider u9 = u as Element of Bags n;
reconsider u9 as bag of n;
not u in {HT(p,O)} by A6,XBOOLE_0:def 5;
then
A7: u9 <> HT(p,O) by TARSKI:def 1;
u in Support p by A6,XBOOLE_0:def 5;
hence u in Support(Red(p,O)) by A7,Lm16;
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 addLoopStr, 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 addLoopStr, 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 addLoopStr, 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 addLoopStr, 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 addLoopStr, p be Polynomial of
n,L;
HT(p,O) in {HT(p,O)} & Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17,
TARSKI:def 1;
then not HT(p,O) in Support(Red(p,O)) by XBOOLE_0:def 5;
hence thesis by POLYNOM1:def 4;
end;
Lm19: for n being Ordinal, O being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, 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 addLoopStr, p be Polynomial of
n,L, b be bag of n;
A1: b is Element of Bags n by PRE_POLY:def 12;
assume b <> HT(p,O);
then not b in {HT(p,O)} by TARSKI:def 1;
then
A2: not b in Support(HM(p,O)) by Lm12;
thus (Red(p,O)).b = (p + -HM(p,O)).b by POLYNOM1:def 7
.= p.b + (-HM(p,O)).b by POLYNOM1:15
.= p.b + -(HM(p,O)).b by POLYNOM1:17
.= p.b + -0.L by A2,A1,POLYNOM1:def 4
.= p.b + 0.L by RLVECT_1:12
.= p.b by RLVECT_1:4;
end;
theorem
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 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 addLoopStr, p
being Polynomial of n,L;
A1: now
let u be object;
assume
A2: u in Support p;
then reconsider u9 = u as Element of Bags n;
reconsider u9 as bag of n;
A3: p.u9 <> 0.L by A2,POLYNOM1:def 4;
now
per cases;
case
A4: u9 = HT(p,O);
then
A5: p.(HT(p,O)) <> 0.L by A2,POLYNOM1:def 4;
(HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
.= HM(p,O).u9 + 0.L by A4,Lm18
.= HM(p,O).u9 by RLVECT_1:4
.= HC(p,O) by A4,Lm8;
hence u9 in Support(HM(p,O) + Red(p,O)) by A5,POLYNOM1:def 4;
end;
case
A6: u9 <> HT(p,O);
(HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
.= HM(p,O).u9 + p.u9 by A6,Lm19
.= 0.L + p.u9 by A6,Th19
.= p.u9 by RLVECT_1:4;
hence u9 in Support(HM(p,O) + Red(p,O)) by A3,POLYNOM1:def 4;
end;
end;
hence u in Support(HM(p,O) + Red(p,O));
end;
now
let u be object;
assume
A7: u in Support(HM(p,O) + Red(p,O));
then reconsider u9 = u as Element of Bags n;
reconsider u9 as bag of n;
A8: (HM(p,O) + Red(p,O)).u9 <> 0.L by A7,POLYNOM1:def 4;
now
per cases;
case
A9: u9 = HT(p,O);
(HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
.= HM(p,O).HT(p,O) + 0.L by A9,Lm18
.= HM(p,O).HT(p,O) by RLVECT_1:4
.= p.u9 by A9,Lm8;
hence u9 in Support p by A8,POLYNOM1:def 4;
end;
case
A10: u9 <> HT(p,O);
(HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
.= 0.L + Red(p,O).u9 by A10,Th19
.= Red(p,O).u9 by RLVECT_1:4
.= p.u by A10,Lm19;
hence u9 in Support p by A8,POLYNOM1:def 4;
end;
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 addLoopStr, 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 addLoopStr, p be Polynomial of
n,L;
A1: now
let x be object;
assume x in Bags n;
then reconsider x9 = 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:15
.= HM(p,O).HT(p,O) + 0.L by Lm18
.= HM(p,O).HT(p,O) by RLVECT_1:4
.= p.x by A2,Lm8;
end;
case
A3: x <> HT(p,O);
(HM(p,O) + Red(p,O)).x9 = HM(p,O).x9 + Red(p,O).x9 by POLYNOM1:15
.= HM(p,O).x9 + p.x9 by A3,Lm19
.= 0.L + p.x9 by A3,Th19
.= p.x9 by RLVECT_1:4;
hence p.x = (HM(p,O) + Red(p,O)).x;
end;
end;
hence p.x = (HM(p,O) + Red(p,O)).x;
end;
dom p = Bags n & dom(HM(p,O) + Red(p,O)) = Bags n by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem
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 (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 addLoopStr, 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;