:: More About Polynomials: Monomials and Constant Polynomials
:: by Christoph Schwarzweller
::
:: Received November 28, 2001
:: Copyright (c) 2001-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 RLVECT_1, ALGSTR_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES,
VECTSP_2, ZFMISC_1, XBOOLE_0, STRUCT_0, POLYNOM1, VALUED_0, SUBSET_1,
SUPINF_2, FUNCT_4, PRE_POLY, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL1,
CARD_1, PARTFUN1, POLYNOM2, FINSEQ_1, CARD_3, NUMBERS, XXREAL_0,
FINSET_1, ORDERS_1, ARYTM_3, NAT_1, MESFUNC1, QUOFIELD, GROUP_1, TARSKI,
MSSUBFAM, ALGSEQ_1, CAT_3, XCMPLX_0, ORDINAL4, POLYNOM7, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_7, POLYNOM1, NUMBERS,
XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_4, NAT_1, ALGSTR_1,
RLVECT_1, ORDERS_1, FINSEQ_1, FUNCOP_1, GROUP_1, QUOFIELD, GRCAT_1,
VECTSP_2, POLYNOM2, VECTSP_1, GROUP_6, PRE_POLY;
constructors REALSET2, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM2,
ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, FUNCT_4, RINGCAT1, MOD_4;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, ALGSTR_0, CARD_1,
SUBSET_1, PRE_POLY, FUNCT_1, RINGCAT1, MOD_4;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FUNCOP_1, STRUCT_0, ORDINAL1;
expansions FUNCT_2, STRUCT_0;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, VECTSP_1,
POLYNOM1, QUOFIELD, FUNCT_7, FUNCT_4, FUNCOP_1, BINOM, FINSEQ_3,
RLVECT_1, VECTSP_2, GROUP_1, NAT_1, FINSEQ_2, FINSEQ_5, MATRLIN,
POLYNOM2, XBOOLE_0, XREAL_1, GROUP_6, XXREAL_0, ORDINAL1, PARTFUN1,
PRE_POLY, XTUPLE_0, PBOOLE;
schemes FUNCT_2;
begin
registration
cluster Abelian left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative distributive
domRing-like for non trivial doubleLoopStr;
existence
proof
set R = the domRing;
take R;
thus thesis;
end;
end;
definition
let X be set, R be non empty ZeroStr, p be Series of X,R;
attr p is non-zero means
p <> 0_(X,R);
end;
registration
let X be set, R be non trivial ZeroStr;
cluster non-zero for Series of X,R;
existence
proof
set a = the Element of NonZero R;
A1: not a in {0.R} by XBOOLE_0:def 5;
reconsider a as Element of R;
set p = 0_(X,R)+*(EmptyBag X,a);
reconsider p as Function of Bags X, the carrier of R;
reconsider p as Function of Bags X, R;
reconsider p as Series of X,R;
take p;
0_(X,R) = (Bags X --> 0.R) by POLYNOM1:def 8;
then dom 0_(X,R) = Bags X;
then
A2: p.(EmptyBag X) = a by FUNCT_7:31;
a <> 0.R by A1,TARSKI:def 1;
then p <> 0_(X,R) by A2,POLYNOM1:22;
hence thesis;
end;
end;
registration
let n be Ordinal, R be non trivial ZeroStr;
cluster non-zero for Polynomial of n,R;
existence
proof
set a = the Element of NonZero R;
A1: not a in {0.R} by XBOOLE_0:def 5;
reconsider a as Element of R;
set p = 0_(n,R)+*(EmptyBag n,a);
reconsider p as Function of Bags n, the carrier of R;
reconsider p as Function of Bags n, R;
reconsider p as Series of n,R;
A2: now
let u be object;
assume
A3: u in Support p;
then
u is Element of Bags n;
then A4: u is bag of n;
now
assume u <> EmptyBag n;
then p.u = (0_(n,R)).u by FUNCT_7:32
.= 0.R by A4,POLYNOM1:22;
hence contradiction by A3,POLYNOM1:def 4;
end;
hence u in {EmptyBag n} by TARSKI:def 1;
end;
0_(n,R) = (Bags n --> 0.R) by POLYNOM1:def 8;
then dom 0_(n,R) = Bags n;
then
A5: p.(EmptyBag n) = a by FUNCT_7:31;
now
let u be object;
assume u in {EmptyBag n};
then
A6: u = EmptyBag n by TARSKI:def 1;
a <> 0.R by A1,TARSKI:def 1;
hence u in Support p by A5,A6,POLYNOM1:def 4;
end;
then Support p = {EmptyBag n} by A2,TARSKI:2;
then reconsider p as Polynomial of n,R by POLYNOM1:def 5;
take p;
a <> 0.R by A1,TARSKI:def 1;
then p <> 0_(n,R) by A5,POLYNOM1:22;
hence thesis;
end;
end;
theorem Th1:
for X being set, R being non empty ZeroStr, s being Series of X,R
holds s = 0_(X,R) iff Support s = {}
proof
let X be set, R be non empty ZeroStr, s be Series of X,R;
A1: now
assume
A2: Support s = {};
now
let x be object;
assume x in Bags X;
then reconsider x9 = x as Element of Bags X;
s.x9 = 0.R by A2,POLYNOM1:def 4;
hence s.x = (0_(X,R)).x by POLYNOM1:22;
end;
hence s = 0_(X,R);
end;
now
assume
A3: s = 0_(X,R);
now
set x = the Element of Support s;
assume Support s <> {};
then
A4: x in Support s;
then reconsider x as bag of X;
s.x <> 0.R by A4,POLYNOM1:def 4;
hence contradiction by A3,POLYNOM1:22;
end;
hence Support s = {};
end;
hence thesis by A1;
end;
theorem
for X being set, R being non empty ZeroStr holds R is non trivial iff
ex s being Series of X,R st Support(s) <> {}
proof
let X be set, R be non empty ZeroStr;
A1: now
set x = EmptyBag X;
assume R is non trivial;
then consider a being Element of R such that
A2: a <> 0.R;
take s = (Bags X) --> a;
s.x = a;
then EmptyBag X in Support s by A2,POLYNOM1:def 4;
hence ex s being Series of X,R st Support(s) <> {};
end;
now
assume ex s being Series of X,R st Support(s) <> {};
then consider s being Series of X,R such that
A3: Support(s) <> {};
set b = the Element of Support s;
b in Support s by A3;
then reconsider b as Element of Bags X;
now
given x being object such that
A4: the carrier of R = {x};
0.R = x by A4,TARSKI:def 1
.= s.b by A4,TARSKI:def 1;
hence contradiction by A3,POLYNOM1:def 4;
end;
hence R is non trivial by ZFMISC_1:131;
end;
hence thesis by A1;
end;
definition
let X be set, b be bag of X;
attr b is univariate means
ex u being Element of X st support b = {u};
end;
registration
let X be non empty set;
cluster univariate for bag of X;
existence
proof
set x = the Element of X;
set b = EmptyBag X +* (x,1);
take b;
A1: dom (EmptyBag X) = X by PARTFUN1:def 2;
then
A2: b.x = ((EmptyBag X)+*(x.-->1)).x by FUNCT_7:def 3;
A4: for u being object holds u in support b implies u in {x}
proof
let u be object;
assume
A5: u in support b;
now
assume u <> x;
then
A6: not u in dom (x.-->1) by TARSKI:def 1;
b.u = ((EmptyBag X)+*(x.-->1)).u by A1,FUNCT_7:def 3;
then b.u = (EmptyBag X).u by A6,FUNCT_4:11
.= 0 by PBOOLE:5;
hence contradiction by A5,PRE_POLY:def 7;
end;
hence thesis by TARSKI:def 1;
end;
x in dom (x.-->1) by TARSKI:def 1;
then
A7: b.x = (x.-->1).x by A2,FUNCT_4:13
.= 1 by FUNCOP_1:72;
for u being object holds u in {x} implies u in support b
proof
let u be object;
assume u in {x};
then u = x by TARSKI:def 1;
hence thesis by A7,PRE_POLY:def 7;
end;
then support b = {x} by A4,TARSKI:2;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster univariate -> non empty-yielding for bag of X;
coherence
proof
let b be bag of X;
assume b is univariate;
then consider x being Element of X such that
A1: support b = {x};
x in support b by A1,TARSKI:def 1;
then b.x <> 0 by PRE_POLY:def 7;
then b.x <> (EmptyBag X).x by PBOOLE:5;
hence thesis by PRE_POLY:def 18;
end;
end;
begin :: Polynomials without Variables
theorem
for b being bag of {} holds b = EmptyBag {}
proof
set n = {};
let b be bag of {};
A1: for b being bag of n holds b = {}
proof
let b be bag of n;
b in Bags n by PRE_POLY:def 12;
hence thesis by PRE_POLY:51,TARSKI:def 1;
end;
then EmptyBag n = {};
hence thesis by A1;
end;
Lm1: for L being non empty doubleLoopStr, p being Polynomial of {},L holds
ex a being Element of L st p = {EmptyBag {}} --> a
proof
set n = {};
let L be non empty doubleLoopStr, p be Polynomial of {},L;
A1: for b being bag of {} holds b = {}
proof
let b be bag of {};
b in Bags {} by PRE_POLY:def 12;
hence thesis by PRE_POLY:51,TARSKI:def 1;
end;
reconsider p as Function of Bags {},L;
reconsider p as Function of {{}},the carrier of L by PRE_POLY:51;
set a = p/.{};
A2: dom p = {{}} by FUNCT_2:def 1
.= {EmptyBag n} by A1;
A3: for u being object holds u in p implies u in [:{EmptyBag n},{a}:]
proof
let u be object;
assume
A4: u in p;
then consider p1,p2 being object such that
A5: u = [p1,p2] by RELAT_1:def 1;
A6: p1 in dom p by A4,A5,XTUPLE_0:def 12;
then reconsider p1 as bag of n by A2;
A7: p2 is set by TARSKI:1;
A8: p1 = {} by A1;
then p2 = p.{} by A4,A5,A6,FUNCT_1:def 2,A7
.= p/.{} by A6,A8,PARTFUN1:def 6;
then p2 in {a} by TARSKI:def 1;
hence thesis by A2,A5,A6,ZFMISC_1:def 2;
end;
take a;
A9: EmptyBag n = {} by A1;
for u being object holds u in [:{EmptyBag n},{a}:] implies u in p
proof
let u be object;
assume u in [:{EmptyBag n},{a}:];
then consider u1,u2 being object such that
A10: u1 in {EmptyBag n} and
A11: u2 in {a} and
A12: u = [u1,u2] by ZFMISC_1:def 2;
A13: u1 = {} by A9,A10,TARSKI:def 1;
u2 = a by A11,TARSKI:def 1
.= p.{} by A2,A10,A13,PARTFUN1:def 6;
hence thesis by A2,A10,A12,A13,FUNCT_1:1;
end;
hence thesis by A3,TARSKI:2;
end;
theorem
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p being Polynomial of {},
L, x being Function of {},L holds eval(p,x) = p.(EmptyBag{})
proof
set n = {};
let L be right_zeroed add-associative right_complementable well-unital
distributive non trivial doubleLoopStr, p be Polynomial of {},L, x be
Function of {},L;
A1: for b being bag of n holds b = {}
proof
let b be bag of n;
b in Bags n by PRE_POLY:def 12;
hence thesis by PRE_POLY:51,TARSKI:def 1;
end;
then
A2: EmptyBag n = {};
consider a being Element of L such that
A3: p = {EmptyBag n} --> a by Lm1;
A4: p.(EmptyBag n) = a by A3;
A5: dom p = {EmptyBag n} by A3;
now
per cases;
case
A6: a = 0.L;
Support p = {}
proof
set u = the Element of Support p;
assume
A7: Support p <> {};
then u in Support p;
then reconsider u as Element of Bags n;
p.u <> 0.L by A7,POLYNOM1:def 4;
hence thesis by A1,A2,A4,A6;
end;
then reconsider Sp = Support p as empty Subset of Bags n;
consider y being FinSequence of the carrier of L such that
A8: len y = len SgmX(BagOrder n, Support p) and
A9: eval(p,x) = Sum y and
for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (p *
SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x)
by POLYNOM2:def 4;
SgmX(BagOrder n, Sp) = {} by POLYNOM2:18,PRE_POLY:76;
then y = <*>(the carrier of L) by A8;
hence eval(p,x) = a by A6,A9,RLVECT_1:43;
end;
case
A10: a <> 0.L;
reconsider sp = Support p as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sp);
A11: BagOrder n linearly_orders sp by POLYNOM2:18;
A12: for u being object holds u in Support p implies u in {{}}
proof
let u be object;
assume u in Support p;
then reconsider u as Element of Bags n;
u = {} by A1;
hence thesis by TARSKI:def 1;
end;
for u being object holds u in {{}} implies u in Support p
proof
let u be object;
assume u in {{}};
then u = EmptyBag n by A2,TARSKI:def 1;
hence thesis by A4,A10,POLYNOM1:def 4;
end;
then Support p = {{}} by A12,TARSKI:2;
then
A13: rng sg = {{}} by A11,PRE_POLY:def 2;
then
A14: {} in rng sg by TARSKI:def 1;
then
A15: 1 in dom sg by FINSEQ_3:31;
then sg.1 in dom p by A2,A5,A13,FUNCT_1:3;
then 1 in dom (p * sg) by A15,FUNCT_1:11;
then
A16: (p * sg)/.1 = (p * sg).1 by PARTFUN1:def 6
.= p.(sg.1) by A15,FUNCT_1:13
.= a by A2,A3,A13,A15,FUNCOP_1:7,FUNCT_1:3;
A17: for u being object holds u in dom sg implies u in {1}
proof
let u be object;
assume
A18: u in dom sg;
assume
A19: not u in {1};
reconsider u as Element of NAT by A18;
sg/.u = sg.u by A18,PARTFUN1:def 6;
then
A20: sg/.u in rng sg by A18,FUNCT_1:3;
A21: u <> 1 by A19,TARSKI:def 1;
A22: 1 < u
proof
consider k being Nat such that
A23: dom sg = Seg k by FINSEQ_1:def 2;
Seg k = {m where m is Nat : 1 <= m & m <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23;
hence thesis by A21,XXREAL_0:1;
end;
sg/.1 = sg.1 by A14,A18,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A15,FUNCT_1:3;
then sg/.1 = {} by A13,TARSKI:def 1
.= sg/.u by A13,A20,TARSKI:def 1;
hence thesis by A11,A15,A18,A22,PRE_POLY:def 2;
end;
for u being object holds u in {1} implies u in dom sg
by A15,TARSKI:def 1;
then dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2;
then
A24: len sg = 1 by FINSEQ_1:def 3;
consider y being FinSequence of the carrier of L such that
A25: len y = len sg and
A26: Sum y = eval(p,x) and
A27: for i being Element of NAT st 1 <= i & i <= len y holds y/.i =
(p * sg)/.i * eval((sg/.i),x) by POLYNOM2:def 4;
dom y = Seg(len y) by FINSEQ_1:def 3
.= dom sg by A25,FINSEQ_1:def 3;
then y.1 = y/.1 by A14,FINSEQ_3:31,PARTFUN1:def 6
.= (p * sg)/.1 * eval((sg/.1),x) by A24,A25,A27
.= (p * sg)/.1 * eval(EmptyBag n,x) by A1,A2
.= (p * sg)/.1 * 1.L by POLYNOM2:14
.= a by A16;
then y = <* a *> by A24,A25,FINSEQ_1:40;
hence eval(p,x) = a by A26,RLVECT_1:44;
end;
end;
hence thesis by A3;
end;
theorem
for L being right_zeroed add-associative right_complementable Abelian
well-unital distributive associative non trivial non trivial doubleLoopStr
holds Polynom-Ring({},L) is_ringisomorph_to L
proof
set n = {};
let L be right_zeroed add-associative right_complementable Abelian
well-unital distributive associative non trivial non trivial doubleLoopStr;
set PL = Polynom-Ring(n,L);
defpred P[set,set] means ex p being Polynomial of n,L st p = $1 & p.{} = $2;
A1: dom 0_(n,L) = Bags n by FUNCT_2:def 1;
A2: EmptyBag n in dom(EmptyBag n .--> 1_L) by TARSKI:def 1;
A3: for b being bag of {} holds b = {}
proof
let b be bag of {};
b in Bags {} by PRE_POLY:def 12;
hence thesis by PRE_POLY:51,TARSKI:def 1;
end;
then
A4: EmptyBag n = {};
then reconsider i = {} as bag of n;
A5: for x being Element of PL ex y being Element of L st P[x,y]
proof
let x be Element of PL;
reconsider p = x as Polynomial of n,L by POLYNOM1:def 11;
take p.{};
dom p = Bags n by FUNCT_2:def 1;
then
A6: p.{} in rng p by A4,FUNCT_1:3;
rng p c= the carrier of L by RELAT_1:def 19;
hence thesis by A6;
end;
consider f being Function of the carrier of PL,the carrier of L such that
A7: for x being Element of PL holds P[x,f.x] from FUNCT_2:sch 3(A5);
A8: dom f = the carrier of PL by FUNCT_2:def 1;
reconsider f as Function of PL,L;
consider p being Polynomial of n,L such that
A9: p = 1_PL and
A10: p.{} = f.(1.PL) by A7;
A11: p = 1_(n,L) by A9,POLYNOM1:31
.= 0_(n,L)+*(EmptyBag n,1_L) by POLYNOM1:def 9;
for x,y being Element of PL holds f.(x*y) = f.x * f.y
proof
let x,y be Element of PL;
consider p being Polynomial of n,L such that
A12: p = x & p.{} = f.x by A7;
consider q being Polynomial of n,L such that
A13: q = y & q.{} = f.y by A7;
A14: (p*'q).{} = p.i * q.i
proof
A15: decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73;
then
A16: len decomp EmptyBag n = 1 by FINSEQ_1:39;
set z = p.i * q.i;
consider s being FinSequence of the carrier of L such that
A17: (p*'q).(EmptyBag n) = Sum s and
A18: len s = len decomp EmptyBag n and
A19: for k being Element of NAT st k in dom s ex b1, b2 being bag of
n st (decomp EmptyBag n)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by POLYNOM1:def 10;
len s = 1 by A15,A18,FINSEQ_1:39;
then Seg 1 = dom s by FINSEQ_1:def 3;
then
A20: 1 in dom s by FINSEQ_1:2,TARSKI:def 1;
then consider b1,b2 being bag of n such that
(decomp EmptyBag n)/.1 = <*b1, b2*> and
A21: s/.1 = p.b1*q.b2 by A19;
s.1 = p.b1 * q.b2 by A20,A21,PARTFUN1:def 6
.= p.i * q.b2 by A3
.= p.i * q.i by A3;
then s = <* z *> by A16,A18,FINSEQ_1:40;
then Sum s = z by RLVECT_1:44;
hence thesis by A3,A17;
end;
ex pq being Polynomial of n,L st pq = x * y & pq.{} = f.( x*y) by A7;
hence thesis by A12,A13,A14,POLYNOM1:def 11;
end;
then
A22: f is multiplicative by GROUP_6:def 6;
for x,y being Element of PL holds f.(x+y) = f.x + f.y
proof
let x,y be Element of PL;
consider p being Polynomial of n,L such that
A23: p = x and
A24: p.{} = f.x by A7;
consider q being Polynomial of n,L such that
A25: q = y and
A26: q.{} = f.y by A7;
consider a being Element of L such that
A27: p = {EmptyBag n} --> a by Lm1;
A28: ex pq being Polynomial of n,L st pq = x + y & pq.{} = f.( x+y) by A7;
consider b being Element of L such that
A29: q = {EmptyBag n} --> b by Lm1;
A30: p.{} = a by A4,A27;
A31: (p+q).{} = p.i + q.i by POLYNOM1:15
.= a + b by A4,A30,A29;
q.{} = b by A4,A29;
then f.x + f.y = a + b by A4,A24,A26,A27;
hence thesis by A23,A25,A28,A31,POLYNOM1:def 11;
end;
then
A32: f is additive by VECTSP_1:def 20;
p.i = p.(EmptyBag n) by A3
.= (0_(n,L)+*(EmptyBag n .--> 1_L)).(EmptyBag n) by A11,A1,FUNCT_7:def 3
.= (EmptyBag n .--> 1_L).(EmptyBag n) by A2,FUNCT_4:13
.= 1_L by FUNCOP_1:72;
then f is unity-preserving by A9,A10,GROUP_1:def 13;
then
A33: f is RingHomomorphism by A32,A22;
A34: for u being object holds u in the carrier of L implies u in rng f
proof
let u be object;
assume u in the carrier of L;
then reconsider u as Element of L;
set p = EmptyBag n .--> u;
reconsider p as Function;
rng p = {u} & dom p = Bags n by FUNCOP_1:8,PRE_POLY:51,TARSKI:def 1;
then reconsider p as Function of Bags n, the carrier of L by FUNCT_2:2;
reconsider p as Function of Bags n, L;
reconsider p as Series of n, L;
now
per cases;
case
A35: u = 0.L;
Support p = {}
proof
set v = the Element of Support p;
assume Support p <> {};
then
A36: v in Support p;
then v is bag of n;
then p.v = p.(EmptyBag n) by A3,A4
.= u by FUNCOP_1:72;
hence thesis by A35,A36,POLYNOM1:def 4;
end;
hence Support p is finite;
end;
case
A37: u <> 0.L;
A38: for v being object holds v in {EmptyBag n} implies v in Support p
proof
let v be object;
assume
A39: v in {EmptyBag n};
then reconsider v as Element of Bags n;
p.v = p.(EmptyBag n) by A39,TARSKI:def 1
.= u by FUNCOP_1:72;
hence thesis by A37,POLYNOM1:def 4;
end;
for v being object holds v in Support p implies v in {EmptyBag n}
proof
let v be object;
assume v in Support p;
then reconsider v as bag of n;
v = EmptyBag n by A3,A4;
hence thesis by TARSKI:def 1;
end;
hence Support p is finite by A38,TARSKI:2;
end;
end;
then reconsider p as Polynomial of n,L by POLYNOM1:def 5;
reconsider p9 = p as Element of PL by POLYNOM1:def 11;
consider q being Polynomial of n,L such that
A40: q = p9 and
A41: q.{} = f.p9 by A7;
q.{} = p.(EmptyBag n) by A3,A40
.= u by FUNCOP_1:72;
hence thesis by A8,A41,FUNCT_1:3;
end;
rng f c= the carrier of L by RELAT_1:def 19;
then for u being object holds u in rng f implies u in the carrier of L;
then rng f = the carrier of L by A34,TARSKI:2;
then f is onto;
then
A42: f is RingEpimorphism by A33;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A43: x1 in dom f & x2 in dom f and
A44: f.x1 = f.x2;
reconsider x1,x2 as Element of PL by A43;
consider p being Polynomial of n,L such that
A45: p = x1 & p.{} = f.x1 by A7;
consider q being Polynomial of n,L such that
A46: q = x2 & q.{} = f.x2 by A7;
consider a2 being Element of L such that
A47: q = {EmptyBag n} --> a2 by Lm1;
A48: q.(EmptyBag n) = a2 by A47;
A49: p.{} = p.(EmptyBag n) by A3;
consider a1 being Element of L such that
A50: p = {EmptyBag n} --> a1 by Lm1;
thus thesis by A3,A44,A45,A46,A50,A47,A48,A49;
end;
then f is one-to-one by FUNCT_1:def 4;
then f is RingMonomorphism by A33;
then f is RingIsomorphism by A42;
hence thesis by QUOFIELD:def 23;
end;
begin :: Monomials
definition
let X be set, L be non empty ZeroStr, p be Series of X,L;
attr p is monomial-like means
:Def3:
ex b being bag of X st for b9 being bag of X st b9 <> b holds p.b9 = 0.L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster monomial-like for Series of X,L;
existence
proof
set p = 0_(X,L);
take p;
for b9 being bag of X st b9 <> EmptyBag X holds p.b9 = 0.L by POLYNOM1:22;
hence thesis;
end;
end;
definition
let X be set, L be non empty ZeroStr;
mode Monomial of X,L is monomial-like Series of X,L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster monomial-like -> finite-Support for Series of X,L;
coherence
proof
let s be Series of X,L;
assume s is monomial-like;
then consider b being bag of X such that
A1: for b9 being bag of X st b9 <> b holds s.b9 = 0.L;
per cases;
suppose
A2: s.b = 0.L;
now
assume Support s <> {};
then reconsider sp = Support s as non empty Subset of Bags X;
set c = the Element of sp;
s.c <> 0.L by POLYNOM1:def 4;
hence contradiction by A1,A2;
end;
hence thesis by POLYNOM1:def 5;
end;
suppose
A3: s.b <> 0.L;
A4: now
let u be object;
assume
A5: u in Support s;
then reconsider u9 = u as Element of Bags X;
s.u9 <> 0.L by A5,POLYNOM1:def 4;
then u9 = b by A1;
hence u in {b} by TARSKI:def 1;
end;
now
let u be object;
assume u in {b};
then
A6: u = b by TARSKI:def 1;
then reconsider u9 = u as Element of Bags X by PRE_POLY:def 12;
u9 in Support s by A3,A6,POLYNOM1:def 4;
hence u in Support s;
end;
then Support s = {b} by A4,TARSKI:2;
hence thesis by POLYNOM1:def 5;
end;
end;
end;
theorem Th6:
for X being set, L being non empty ZeroStr, p being Series of X,L
holds p is Monomial of X,L iff (Support p = {} or ex b being bag of X st
Support p = {b})
proof
let n be set, L be non empty ZeroStr, p be Series of n,L;
A1: now
assume ex b being bag of n st Support p = {b};
then consider b being bag of n such that
A2: Support p = {b};
for b9 being bag of n st b9 <> b holds p.b9 = 0.L
proof
let b9 be bag of n;
assume
A3: b9 <> b;
assume
A4: p.b9 <> 0.L;
reconsider b9 as Element of Bags n by PRE_POLY:def 12;
b9 in Support p by A4,POLYNOM1:def 4;
hence thesis by A2,A3,TARSKI:def 1;
end;
hence p is Monomial of n,L by Def3;
end;
A5: now
assume p is Monomial of n,L;
then consider b being bag of n such that
A6: for b9 being bag of n st b9 <> b holds p.b9 = 0.L by Def3;
now
per cases;
case
A7: p.b <> 0.L;
A8: for u being object holds u in {b} implies u in Support p
proof
let u be object;
assume
A9: u in {b};
then u = b by TARSKI:def 1;
then reconsider u9 = u as Element of Bags n by PRE_POLY:def 12;
p.u9 <> 0.L by A7,A9,TARSKI:def 1;
hence thesis by POLYNOM1:def 4;
end;
for u being object holds u in Support p implies u in {b}
proof
let u be object;
assume
A10: u in Support p;
then reconsider u9 = u as bag of n;
p.u <> 0.L by A10,POLYNOM1:def 4;
then u9 = b by A6;
hence thesis by TARSKI:def 1;
end;
then Support p = {b} by A8,TARSKI:2;
hence ex b being bag of n st Support p = {b};
end;
case
A11: p.b = 0.L;
thus Support p = {}
proof
assume Support p <> {};
then reconsider sp = Support p as non empty Subset of Bags n;
set c = the Element of sp;
p.c <> 0.L by POLYNOM1:def 4;
hence thesis by A6,A11;
end;
end;
end;
hence Support p = {} or ex b being bag of n st Support p = {b};
end;
now
set b = the bag of n;
assume
A12: Support p = {};
for b9 being bag of n st b9 <> b holds p.b9 = 0.L
proof
let b9 be bag of n;
assume b9 <> b;
reconsider c = b9 as Element of Bags n by PRE_POLY:def 12;
assume p.b9 <> 0.L;
then c in Support p by POLYNOM1:def 4;
hence thesis by A12;
end;
hence p is Monomial of n,L by Def3;
end;
hence thesis by A1,A5;
end;
definition
let X be set, L be non empty ZeroStr, a be Element of L, b be bag of X;
func Monom(a,b) -> Monomial of X,L equals
0_(X,L)+*(b,a);
coherence
proof
A1: b in dom(b .--> a) by TARSKI:def 1;
set m = 0_(X,L)+*(b,a);
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L;
reconsider m as Series of X, L;
A2: b in Bags X by PRE_POLY:def 12;
A3: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A4: m = 0_(X,L)+*(b .--> a) by A2,FUNCT_7:def 3;
A5: m.b = (0_(X,L)+*(b .--> a)).b by A3,A2,FUNCT_7:def 3
.= (b .--> a).b by A1,FUNCT_4:13
.= a by FUNCOP_1:72;
now
per cases;
case
A6: a <> 0.L;
A7: for u being object holds u in Support m implies u in {b}
proof
let u be object;
assume
A8: u in Support m;
assume not u in {b};
then
A9: not u in dom(b .--> a);
reconsider u as bag of X by A8;
m.u = (0_(X,L)).u by A4,A9,FUNCT_4:11
.= 0.L by POLYNOM1:22;
hence thesis by A8,POLYNOM1:def 4;
end;
b in Support m by A2,A5,A6,POLYNOM1:def 4;
then for u being object holds u in {b} implies u in Support m by
TARSKI:def 1;
then Support m = {b} by A7,TARSKI:2;
hence thesis by Th6;
end;
case
A10: a = 0.L;
now
assume Support m <> {};
then reconsider sm = Support m as non empty Subset of Bags X;
set c = the Element of sm;
m.c <> 0.L by POLYNOM1:def 4;
then not c in {b} by A5,A10,TARSKI:def 1;
then
A11: not c in dom(b .--> a);
reconsider c as bag of X;
m.c = (0_(X,L)).c by A4,A11,FUNCT_4:11
.= 0.L by POLYNOM1:22;
hence contradiction by POLYNOM1:def 4;
end;
hence thesis by Th6;
end;
end;
hence thesis;
end;
end;
definition
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
func term(m) -> bag of X means
:Def5:
m.it <> 0.L or Support m = {} & it = EmptyBag X;
existence
proof
consider b being bag of X such that
A1: for b9 being bag of X st b9 <> b holds m.b9 = 0.L by Def3;
now
per cases;
case
m.b <> 0.L;
hence thesis;
end;
case
A2: m.b = 0.L;
Support m = {}
proof
assume Support m <> {};
then reconsider sm = Support m as non empty Subset of Bags X;
set c = the Element of sm;
m.c <> 0.L by POLYNOM1:def 4;
hence thesis by A1,A2;
end;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let b1,b2 be bag of X;
assume
A3: m.b1 <> 0.L or Support m = {} & b1 = EmptyBag X;
consider b being bag of X such that
A4: for b9 being bag of X st b9 <> b holds m.b9 = 0.L by Def3;
assume
A5: m.b2 <> 0.L or Support m = {} & b2 = EmptyBag X;
now
per cases;
case
A6: m.b1 <> 0.L;
reconsider b19 = b1 as Element of Bags X by PRE_POLY:def 12;
A7: b19 in Support m by A6,POLYNOM1:def 4;
thus b1 = b by A4,A6
.= b2 by A5,A4,A7;
end;
case
A8: m.b1 = 0.L;
now
per cases by A5;
case
A9: m.b2 <> 0.L;
reconsider b29 = b2 as Element of Bags X by PRE_POLY:def 12;
b29 in Support m by A9,POLYNOM1:def 4;
hence thesis by A3,A8;
end;
case
Support m = {} & b2 = EmptyBag X;
hence thesis by A3,A8;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
definition
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
func coefficient(m) -> Element of L equals
m.(term(m));
coherence;
end;
theorem Th7:
for X being set, L being non empty ZeroStr, m being Monomial of X
,L holds Support(m) = {} or Support(m) = {term(m)}
proof
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
A1: term(m) is Element of Bags X by PRE_POLY:def 12;
assume
A2: Support(m) <> {};
then m.term(m) <> 0.L by Def5;
then
A3: term(m) in Support(m) by A1,POLYNOM1:def 4;
ex b being bag of X st Support(m) = {b} by A2,Th6;
hence thesis by A3,TARSKI:def 1;
end;
theorem Th8:
for X being set, L being non empty ZeroStr, b being bag of X
holds coefficient(Monom(0.L,b)) = 0.L & term(Monom(0.L,b)) = EmptyBag X
proof
let n be set, L be non empty ZeroStr, b be bag of n;
set m = 0_(n,L)+*(b,0.L);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L;
reconsider m as Series of n, L;
A1: b in Bags n by PRE_POLY:def 12;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8
.= Bags n;
then
A3: m = 0_(n,L)+*(b .--> 0.L) by A1,FUNCT_7:def 3;
A4: b in dom(b .--> 0.L) by TARSKI:def 1;
A5: m.b = (0_(n,L)+*(b .--> 0.L)).b by A2,A1,FUNCT_7:def 3
.= (b .--> 0.L).b by A4,FUNCT_4:13
.= 0.L by FUNCOP_1:72;
A6: now
let b9 be bag of n;
now
per cases;
case
b9 = b;
hence m.b9 = 0.L by A5;
end;
case
b9 <> b;
then not b9 in dom(b .--> 0.L) by TARSKI:def 1;
hence m.b9 = (0_(n,L)).b9 by A3,FUNCT_4:11
.= 0.L by POLYNOM1:22;
end;
end;
hence m.b9 = 0.L;
end;
hence coefficient(Monom(0.L,b)) = 0.L;
(Monom(0.L,b)).(term(Monom(0.L,b))) = 0.L by A6;
hence thesis by Def5;
end;
theorem Th9:
for X being set, L being non empty ZeroStr, a being Element of L,
b being bag of X holds coefficient(Monom(a,b)) = a
proof
let n be set, L be non empty ZeroStr, a be Element of L, b be bag of n;
set m = 0_(n,L)+*(b,a);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L;
reconsider m as Series of n, L;
A1: b in Bags n by PRE_POLY:def 12;
A2: b in dom(b .--> a) by TARSKI:def 1;
dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8
.= Bags n;
then
A3: m.b = (0_(n,L)+*(b .--> a)).b by A1,FUNCT_7:def 3
.= (b .--> a).b by A2,FUNCT_4:13
.= a by FUNCOP_1:72;
per cases;
suppose
m.b <> 0.L;
hence thesis by A3,Def5;
end;
suppose
m.b = 0.L;
hence thesis by A3,Th8;
end;
end;
theorem Th10:
for X being set, L being non trivial ZeroStr, a being non zero
Element of L, b being bag of X holds term(Monom(a,b)) = b
proof
let n be set, L be non trivial ZeroStr, a be non zero Element of L, b be
bag of n;
set m = 0_(n,L)+*(b,a);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L;
reconsider m as Series of n, L;
A1: b in Bags n by PRE_POLY:def 12;
A2: b in dom(b .--> a) by TARSKI:def 1;
dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8
.= Bags n;
then m.b = (0_(n,L)+*(b .--> a)).b by A1,FUNCT_7:def 3
.= (b .--> a).b by A2,FUNCT_4:13
.= a by FUNCOP_1:72;
then m.b <> 0.L;
hence thesis by Def5;
end;
theorem
for X being set, L being non empty ZeroStr, m being Monomial of X,L
holds Monom(coefficient(m),term(m)) = m
proof
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
per cases by Th6;
suppose
A1: Support m = {};
A2: now
A3: term(m) is Element of Bags X by PRE_POLY:def 12;
assume coefficient(m) <> 0.L;
hence contradiction by A1,A3,POLYNOM1:def 4;
end;
A4: m = 0_(X,L) by A1,Th1;
set m9 = Monom(coefficient(m),term(m));
A5: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
A6: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
A7: term(m) = EmptyBag X by A1,Def5;
then
A8: m9.EmptyBag X = (0_(X,L)+*(EmptyBag X .--> 0.L)).EmptyBag X by A2,A5,
FUNCT_7:def 3
.= (EmptyBag X .--> 0.L).EmptyBag X by A6,FUNCT_4:13
.= 0.L by FUNCOP_1:72;
now
let x be object;
assume x in Bags X;
then reconsider x9= x as Element of Bags X;
now
per cases;
case
x9 = EmptyBag X;
hence m9.x9 = 0.L by A8;
end;
case
x <> EmptyBag X;
then
A9: not x9 in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
m9.x9 = (0_(X,L)+*(EmptyBag X .--> 0.L)).x9 by A7,A2,A5,FUNCT_7:def 3
.= 0_(X,L).x9 by A9,FUNCT_4:11;
hence m9.x9 = 0.L by POLYNOM1:22;
end;
end;
hence m.x = m9.x by A4,POLYNOM1:22;
end;
hence thesis;
end;
suppose
ex b being bag of X st Support m = {b};
then consider b being bag of X such that
A10: Support m = {b};
set a = m.b;
A11: b in dom(b .--> a) by TARSKI:def 1;
set m9 = Monom(coefficient(m),term(m));
A12: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
A13: b in Support m by A10,TARSKI:def 1;
then a <> 0.L by POLYNOM1:def 4;
then
A14: term(m) = b by Def5;
A15: now
let u be object;
assume
A16: u in Support(Monom(coefficient(m),term(m)));
then reconsider u9 = u as Element of Bags X;
now
assume u <> b;
then
A17: not u9 in dom(b .--> a) by TARSKI:def 1;
b in dom 0_(X,L) by A12,PRE_POLY:def 12;
then m9.u9 = (0_(X,L)+*(b .--> a)).u9 by A14,FUNCT_7:def 3
.= 0_(X,L).u9 by A17,FUNCT_4:11;
hence m9.u9 = 0.L by POLYNOM1:22;
end;
hence u in {b} by A16,POLYNOM1:def 4,TARSKI:def 1;
end;
b in Bags X by PRE_POLY:def 12;
then
A18: m9.b = (0_(X,L)+*(b .--> a)).b by A14,A12,FUNCT_7:def 3
.= (b .--> a).b by A11,FUNCT_4:13
.= a by FUNCOP_1:72;
now
let u be object;
assume u in {b};
then
A19: u = b by TARSKI:def 1;
m9.b <> 0.L by A13,A18,POLYNOM1:def 4;
hence u in Support(Monom(coefficient(m),term(m))) by A13,A19,
POLYNOM1:def 4;
end;
then
A20: Support(Monom(coefficient(m),term(m))) = {b} by A15,TARSKI:2;
now
let x be object;
assume x in Bags X;
then reconsider x9 = x as Element of Bags X;
now
per cases;
case
x = b;
hence Monom(coefficient(m),term(m)).x9 = m.x9 by A18;
end;
case
A21: x <> b;
then
A22: not x in Support(Monom(coefficient(m),term(m))) by A20,TARSKI:def 1;
not x in Support m by A10,A21,TARSKI:def 1;
hence m.x9 = 0.L by POLYNOM1:def 4
.= Monom(coefficient(m),term(m)).x9 by A22,POLYNOM1:def 4;
end;
end;
hence m.x = Monom(coefficient(m),term(m)).x;
end;
hence thesis;
end;
end;
theorem Th12:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, m
being Monomial of n,L, x being Function of n,L holds eval(m,x) = coefficient(m)
* eval(term(m),x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, m be Monomial of n,L, x
be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support m) and
A2: eval(m,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (m *
SgmX(BagOrder n, Support m))/.i * eval(((SgmX(BagOrder n, Support m))/.i),x)
by POLYNOM2:def 4;
consider b being bag of n such that
A4: for b9 being bag of n st b9 <> b holds m.b9 = 0.L by Def3;
now
per cases;
case
A5: m.b <> 0.L;
A6: for u being object holds u in Support m implies u in {b}
proof
let u be object;
assume
A7: u in Support m;
assume
A8: not u in {b};
reconsider u as Element of Bags n by A7;
u <> b by A8,TARSKI:def 1;
then m.u = 0.L by A4;
hence thesis by A7,POLYNOM1:def 4;
end;
A9: b in Bags n & dom m = Bags n by FUNCT_2:def 1,PRE_POLY:def 12;
reconsider sm = Support m as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sm);
A10: BagOrder n linearly_orders sm by POLYNOM2:18;
for u being object holds u in {b} implies u in Support m
proof
let u be object;
assume
A11: u in {b};
then u = b by TARSKI:def 1;
then reconsider u as Element of Bags n by PRE_POLY:def 12;
m.u <> 0.L by A5,A11,TARSKI:def 1;
hence thesis by POLYNOM1:def 4;
end;
then Support m = {b} by A6,TARSKI:2;
then
A12: rng sg = {b} by A10,PRE_POLY:def 2;
then
A13: b in rng sg by TARSKI:def 1;
then
A14: 1 in dom sg by FINSEQ_3:31;
then
A15: sg.1 in rng sg by FUNCT_1:3;
then sg.1 = b by A12,TARSKI:def 1;
then 1 in dom (m * sg) by A14,A9,FUNCT_1:11;
then
A16: (m * sg)/.1 = (m * sg).1 by PARTFUN1:def 6
.= m.(sg.1) by A14,FUNCT_1:13
.= m.b by A12,A15,TARSKI:def 1
.= coefficient(m) by A5,Def5;
A17: for u being object holds u in dom sg implies u in {1}
proof
let u be object;
assume
A18: u in dom sg;
assume
A19: not u in {1};
reconsider u as Element of NAT by A18;
sg/.u = sg.u by A18,PARTFUN1:def 6;
then
A20: sg/.u in rng sg by A18,FUNCT_1:3;
A21: u <> 1 by A19,TARSKI:def 1;
A22: 1 < u
proof
consider k being Nat such that
A23: dom sg = Seg k by FINSEQ_1:def 2;
Seg k = {l where l is Nat : 1 <= l & l <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23;
hence thesis by A21,XXREAL_0:1;
end;
sg/.1 = sg.1 by A13,A18,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A14,FUNCT_1:3;
then sg/.1 = b by A12,TARSKI:def 1
.= sg/.u by A12,A20,TARSKI:def 1;
hence thesis by A10,A14,A18,A22,PRE_POLY:def 2;
end;
for u being object holds u in {1} implies u in dom sg
by A14,TARSKI:def 1;
then
A24: dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2;
then
A25: 1 in dom sg by FINSEQ_1:2,TARSKI:def 1;
sg/.1 = sg.1 by A14,PARTFUN1:def 6;
then sg/.1 in rng sg by A25,FUNCT_1:3;
then
A26: sg/.1 = b by A12,TARSKI:def 1;
A27: len sg = 1 by A24,FINSEQ_1:def 3;
dom y = Seg(len y) by FINSEQ_1:def 3
.= dom sg by A1,FINSEQ_1:def 3;
then y.1 = y/.1 by A25,PARTFUN1:def 6
.= (m * sg)/.1 * eval(b,x) by A26,A1,A3,A27;
then y = <* coefficient(m) * eval(b,x) *> by A1,A27,A16,FINSEQ_1:40;
hence eval(m,x) = coefficient(m) * eval(b,x) by A2,RLVECT_1:44
.= coefficient(m) * eval(term(m),x) by A5,Def5;
end;
case
A28: m.b = 0.L;
A29: Support m = {}
proof
assume Support m <> {};
then reconsider sm = Support m as non empty Subset of Bags n;
set c = the Element of sm;
m.c <> 0.L by POLYNOM1:def 4;
hence thesis by A4,A28;
end;
then term(m) = EmptyBag n & m.(EmptyBag n) = 0.L by Def5,POLYNOM1:def 4;
then
A30: coefficient(m) * eval(term(m),x) = 0.L;
consider y being FinSequence of the carrier of L such that
A31: len y = len SgmX(BagOrder n, Support m) and
A32: eval(m,x) = Sum y and
for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (m *
SgmX(BagOrder n, Support m))/.i * eval(((SgmX(BagOrder n, Support m))/.i),x)
by POLYNOM2:def 4;
BagOrder n linearly_orders Support m by POLYNOM2:18;
then rng SgmX(BagOrder n, Support m) = {} by A29,PRE_POLY:def 2;
then SgmX(BagOrder n, Support m) = {} by RELAT_1:41;
then y = <*>(the carrier of L) by A31;
hence thesis by A30,A32,RLVECT_1:43;
end;
end;
hence thesis;
end;
theorem
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, a
being Element of L, b being bag of n, x being Function of n,L holds eval(Monom(
a,b),x) = a * eval(b,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, a be Element of L, b be
bag of n, x be Function of n,L;
set m = Monom(a,b);
now
per cases;
case
a <> 0.L;
then
A1: a is non zero;
thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12
.= a * eval(term(m),x) by Th9
.= a * eval(b,x) by A1,Th10;
end;
case
A2: a = 0.L;
for b9 being bag of n holds m.b9 = 0.L
proof
let b9 be bag of n;
now
per cases;
case
A3: b9 = b;
A4: b in Bags n by PRE_POLY:def 12;
A5: b in dom(b .--> a) by TARSKI:def 1;
dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8
.= Bags n;
then m = 0_(n,L)+*(b .--> a) by A4,FUNCT_7:def 3;
hence m.b9 = (b .--> a).b by A3,A5,FUNCT_4:13
.= 0.L by A2,FUNCOP_1:72;
end;
case
b9 <> b;
hence m.b9 = 0_(n,L).b9 by FUNCT_7:32
.= 0.L by POLYNOM1:22;
end;
end;
hence thesis;
end;
then
A6: m.(term(m)) = 0.L;
thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12
.= 0.L by A6
.= a * eval(b,x) by A2;
end;
end;
hence thesis;
end;
begin :: Constant Polynomials
definition
let X be set, L be non empty ZeroStr, p be Series of X,L;
attr p is Constant means
:Def7:
for b being bag of X st b <> EmptyBag X holds p.b = 0.L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster Constant for Series of X,L;
existence
proof
set c = 0_(X,L);
take c;
for b being bag of X st b <> EmptyBag X holds c.b = 0.L by POLYNOM1:22;
hence thesis;
end;
end;
definition
let X be set, L be non empty ZeroStr;
mode ConstPoly of X,L is Constant Series of X,L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster Constant -> monomial-like for Series of X,L;
coherence;
end;
theorem Th14:
for X being set, L being non empty ZeroStr, p being Series of X,
L holds p is ConstPoly of X,L iff (p = 0_(X,L) or Support p = {EmptyBag X})
proof
let n be set, L be non empty ZeroStr, p be Series of n,L;
A1: now
assume
A2: p is ConstPoly of n,L;
A3: for u being object holds u in Support p implies u in {EmptyBag n}
proof
let u be object;
assume
A4: u in Support p;
then reconsider u as Element of Bags n;
reconsider u9 = u as bag of n;
p.u9 <> 0.L by A4,POLYNOM1:def 4;
then u9 = EmptyBag n by A2,Def7;
hence thesis by TARSKI:def 1;
end;
thus Support p = {EmptyBag n} or p = 0_(n,L)
proof
assume
A5: not Support p = {EmptyBag n};
A6: not EmptyBag n in Support p
proof
assume EmptyBag n in Support p;
then
for u being object holds u in {EmptyBag n} implies u in Support p by
TARSKI:def 1;
hence thesis by A3,A5,TARSKI:2;
end;
A7: Support p = {}
proof
set v = the Element of Support p;
assume Support p <> {};
then v in Support p & v in {EmptyBag n} by A3;
hence thesis by A6,TARSKI:def 1;
end;
A8: for b being bag of n holds p.b = 0.L
proof
let b be bag of n;
A9: b is Element of Bags n by PRE_POLY:def 12;
assume p.b <> 0.L;
hence thesis by A7,A9,POLYNOM1:def 4;
end;
A10: for u being object holds u in rng p implies u in {0.L}
proof
let u be object;
assume u in rng p;
then consider x being object such that
A11: x in dom p and
A12: p.x = u by FUNCT_1:def 3;
x is bag of n by A11;
then u = 0.L by A8,A12;
hence thesis by TARSKI:def 1;
end;
A13: dom p = Bags n by FUNCT_2:def 1;
for u being object holds u in {0.L} implies u in rng p
proof
set b = the bag of n;
let u be object;
assume u in {0.L};
then u = 0.L by TARSKI:def 1;
then
A14: p.b = u by A8;
b in dom p by A13,PRE_POLY:def 12;
hence thesis by A14,FUNCT_1:def 3;
end;
then rng p = {0.L} by A10,TARSKI:2;
then p = (Bags n) --> 0.L by A13,FUNCOP_1:9;
hence thesis by POLYNOM1:def 8;
end;
end;
now
assume
A15: p = 0_(n,L) or Support p = {EmptyBag n};
per cases by A15;
suppose
p = 0_(n,L);
then for b being bag of n st b <> EmptyBag n holds p.b = 0.L by
POLYNOM1:22;
hence p is ConstPoly of n,L by Def7;
end;
suppose
A16: Support p = {EmptyBag n};
for b being bag of n st b <> EmptyBag n holds p.b = 0.L
proof
let b be bag of n;
assume
A17: b <> EmptyBag n;
reconsider b as Element of Bags n by PRE_POLY:def 12;
not b in Support p by A16,A17,TARSKI:def 1;
hence thesis by POLYNOM1:def 4;
end;
hence p is ConstPoly of n,L by Def7;
end;
end;
hence thesis by A1;
end;
registration
let X be set, L be non empty ZeroStr;
cluster 0_(X,L) -> Constant;
coherence
by POLYNOM1:22;
end;
registration
let X be set, L be well-unital non empty doubleLoopStr;
cluster 1_(X,L) -> Constant;
coherence
by POLYNOM1:25;
end;
Lm2: for X being set, L being non empty ZeroStr, c being ConstPoly of X,L
holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X)
proof
let n be set, L be non empty ZeroStr, c be ConstPoly of n,L;
set eb = EmptyBag n;
A1: now
per cases;
case
c.eb <> 0.L;
hence term(c) = EmptyBag n by Def5;
end;
case
A2: c.eb = 0.L;
Support c = {}
proof
set u = the Element of Support c;
assume
A3: Support c <> {};
then u in Support c;
then reconsider u as Element of Bags n;
c.u <> 0.L by A3,POLYNOM1:def 4;
hence thesis by A2,Def7;
end;
hence term(c) = EmptyBag n by Def5;
end;
end;
hence term(c) = EmptyBag n;
thus thesis by A1;
end;
theorem Th15:
for X being set, L being non empty ZeroStr, c being ConstPoly of
X,L holds Support(c) = {} or Support(c) = {EmptyBag X}
proof
let X be set, L be non empty ZeroStr, c be ConstPoly of X,L;
assume Support(c) <> {};
hence Support(c) = {term(c)} by Th7
.= {EmptyBag X} by Lm2;
end;
theorem
for X being set, L being non empty ZeroStr, c being ConstPoly of X,L
holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X) by Lm2;
definition
let X be set, L be non empty ZeroStr, a be Element of L;
func a |(X,L) -> Series of X,L equals
0_(X,L)+*(EmptyBag X,a);
coherence;
end;
registration
let X be set, L be non empty ZeroStr, a be Element of L;
cluster a |(X,L) -> Constant;
coherence
proof
set Z = 0_(X,L);
set O = Z+*(EmptyBag X,a);
reconsider O as Function of Bags X,the carrier of L;
reconsider O9 = O as Function of Bags X,L;
reconsider O9 as Series of X,L;
now
let b be bag of X;
dom(Z) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A1: O9 = 0_(X,L)+*(EmptyBag X .--> a) by FUNCT_7:def 3;
assume b <> EmptyBag X;
then not b in dom(EmptyBag X .--> a) by TARSKI:def 1;
hence (O9).b = (0_(X,L)).b by A1,FUNCT_4:11
.= 0.L by POLYNOM1:22;
end;
hence thesis;
end;
end;
Lm3: for X being set, L being non empty ZeroStr holds 0.L |(X,L) = 0_(X,L)
proof
let X be set, L be non empty ZeroStr;
set o1 = 0.L |(X,L), o2 = 0_(X,L);
now
set m = 0_(X,L)+*(EmptyBag X,0.L);
let x be object;
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L;
reconsider m as Series of X, L;
assume x in Bags X;
then reconsider x9 = x as bag of X;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A2: m = 0_(X,L)+*(EmptyBag X .--> 0.L) by FUNCT_7:def 3;
A3: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
A4: m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> 0.L)).(EmptyBag X) by A1,
FUNCT_7:def 3
.= (EmptyBag X .--> 0.L).(EmptyBag X) by A3,FUNCT_4:13
.= 0.L by FUNCOP_1:72;
per cases;
suppose
x9 = EmptyBag X;
hence o1.x = o2.x by A4,POLYNOM1:22;
end;
suppose
x9 <> EmptyBag X;
then not x9 in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
hence o1.x = o2.x by A2,FUNCT_4:11;
end;
end;
hence thesis;
end;
theorem
for X being set, L being non empty ZeroStr, p being Series of X,L
holds p is ConstPoly of X,L iff ex a being Element of L st p = a |(X,L)
proof
let X be set, L be non empty ZeroStr, p be Series of X,L;
now
assume
A1: p is ConstPoly of X,L;
now
per cases by A1,Th14;
case
p = 0_(X,L);
then p = 0.L |(X,L) by Lm3;
hence ex a being Element of L st p = a |(X,L);
end;
case
A2: Support p = {EmptyBag X};
set q = 0_(X,L)+*(EmptyBag X,p.(EmptyBag X));
A3: now
let x be object;
assume x in Bags X;
then reconsider x9 = x as bag of X;
A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A5: q = 0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X)) by FUNCT_7:def 3;
A6: EmptyBag X in dom(EmptyBag X .--> p.(EmptyBag X)) by TARSKI:def 1;
A7: q.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X))).(
EmptyBag X) by A4,FUNCT_7:def 3
.= (EmptyBag X .--> p.(EmptyBag X)).(EmptyBag X) by A6,FUNCT_4:13
.= p.(EmptyBag X) by FUNCOP_1:72;
now
per cases;
case
x9 = EmptyBag X;
hence p.x = q.x by A7;
end;
case
A8: x9 <> EmptyBag X;
A9: x9 is Element of Bags X by PRE_POLY:def 12;
not x9 in Support p by A2,A8,TARSKI:def 1;
then
A10: p.x9 = 0.L by A9,POLYNOM1:def 4;
not x9 in dom(EmptyBag X .--> p.(EmptyBag X)) by A8,TARSKI:def 1;
then q.x9 = (0_(X,L)).x9 by A5,FUNCT_4:11;
hence p.x = q.x by A10,POLYNOM1:22;
end;
end;
hence p.x = q.x;
end;
A11: Bags X = dom q by FUNCT_2:def 1;
q = p.(EmptyBag X) |(X,L) & Bags X = dom p by FUNCT_2:def 1;
hence ex a being Element of L st p = a |(X,L) by A11,A3,FUNCT_1:2;
end;
end;
hence ex a being Element of L st p = a |(X,L);
end;
hence thesis;
end;
theorem Th18:
for X being set, L being non empty multLoopStr_0, a being
Element of L holds (a |(X,L)).EmptyBag X = a & for b being bag of X st b <>
EmptyBag X holds (a |(X,L)).b = 0.L
proof
let n be set, L be non empty multLoopStr_0, a be Element of L;
set Z = 0_(n,L);
A1: Z = (Bags n --> 0.L) by POLYNOM1:def 8;
then dom Z = Bags n;
hence (a |(n,L)).EmptyBag n = a by FUNCT_7:31;
let b be bag of n;
A2: b in Bags n by PRE_POLY:def 12;
assume b <> EmptyBag n;
hence (a |(n,L)).b = Z.b by FUNCT_7:32
.= 0.L by A1,A2,FUNCOP_1:7;
end;
theorem
for X being set, L being non empty ZeroStr holds 0.L |(X,L) = 0_(X,L) by Lm3;
theorem
for X being set, L being well-unital non empty multLoopStr_0 holds (
1.L) |(X,L) = 1_(X,L)
proof
let X be set, L be well-unital non empty multLoopStr_0;
set o1 = (1.L) |(X,L), o2 = 1_(X,L);
now
set m = 0_(X,L)+*(EmptyBag X,1.L);
let x be object;
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L;
reconsider m as Series of X, L;
assume x in Bags X;
then reconsider x9 = x as bag of X;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A2: m = 0_(X,L)+*(EmptyBag X .--> 1.L) by FUNCT_7:def 3;
A3: EmptyBag X in dom(EmptyBag X .--> 1.L) by TARSKI:def 1;
A4: m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> 1.L)).(EmptyBag X) by A1,
FUNCT_7:def 3
.= (EmptyBag X .--> 1.L).(EmptyBag X) by A3,FUNCT_4:13
.= 1.L by FUNCOP_1:72;
per cases;
suppose
x9 = EmptyBag X;
hence o1.x = o2.x by A4,POLYNOM1:25;
end;
suppose
A5: x9 <> EmptyBag X;
then not x9 in dom(EmptyBag X .--> 1.L) by TARSKI:def 1;
then m.x9 = (0_(X,L)).x9 by A2,FUNCT_4:11
.= 0.L by POLYNOM1:22
.= o2.x9 by A5,POLYNOM1:25;
hence o1.x = o2.x;
end;
end;
hence thesis;
end;
theorem
for X being set, L being non empty ZeroStr, a,b being Element of L
holds a |(X,L) = b |(X,L) iff a = b
proof
let X be set, L be non empty ZeroStr, a,b be Element of L;
set m = 0_(X,L)+*(EmptyBag X,a);
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L;
reconsider m as Series of X, L;
set k = 0_(X,L)+*(EmptyBag X,b);
reconsider k as Function of Bags X, the carrier of L;
reconsider k as Function of Bags X, L;
reconsider k as Series of X, L;
A1: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
A2: EmptyBag X in dom(EmptyBag X .--> b) by TARSKI:def 1;
dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then
A3: k.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> b)).(EmptyBag X) by
FUNCT_7:def 3
.= (EmptyBag X .--> b).(EmptyBag X) by A2,FUNCT_4:13
.= b by FUNCOP_1:72;
dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by
FUNCT_7:def 3
.= (EmptyBag X .--> a).(EmptyBag X) by A1,FUNCT_4:13
.= a by FUNCOP_1:72;
hence thesis by A3;
end;
theorem
for X being set, L being non empty ZeroStr, a being Element of L holds
Support(a |(X,L)) = {} or Support(a |(X,L)) = {EmptyBag X} by Th15;
theorem Th23:
for X being set, L being non empty ZeroStr, a being Element of L
holds term(a |(X,L)) = EmptyBag X & coefficient(a |(X,L)) = a
proof
let X be set, L be non empty ZeroStr, a be Element of L;
set m = 0_(X,L)+*(EmptyBag X,a);
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L;
reconsider m as Series of X, L;
A1: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
then m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by
FUNCT_7:def 3
.= (EmptyBag X .--> a).(EmptyBag X) by A1,FUNCT_4:13
.= a by FUNCOP_1:72;
hence thesis by Lm2;
end;
theorem Th24:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, c
being ConstPoly of n,L, x being Function of n,L holds eval(c,x) = coefficient(c
)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, c be ConstPoly of n,L, x
be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support c) and
A2: eval(c,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (c *
SgmX(BagOrder n, Support c))/.i * eval(((SgmX(BagOrder n, Support c))/.i),x)
by POLYNOM2:def 4;
now
per cases;
case
A4: coefficient(c) = 0.L;
Support c = {}
proof
set u = the Element of Support c;
assume
A5: Support c <> {};
then u in Support c;
then reconsider u as Element of Bags n;
c.u <> 0.L by A5,POLYNOM1:def 4;
then u <> EmptyBag n by A4,Lm2;
then c.u = 0.L by Def7;
hence thesis by A5,POLYNOM1:def 4;
end;
then reconsider Sc = Support c as empty Subset of Bags n;
SgmX(BagOrder n, Sc) = {} by POLYNOM2:18,PRE_POLY:76;
then y = <*>(the carrier of L) by A1;
hence thesis by A2,A4,RLVECT_1:43;
end;
case
A6: coefficient(c) <> 0.L;
reconsider sc = Support c as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sc);
A7: BagOrder n linearly_orders sc by POLYNOM2:18;
A8: for u being object holds u in Support c implies u in {EmptyBag n}
proof
let u be object;
assume
A9: u in Support c;
assume
A10: not u in {EmptyBag n};
reconsider u as Element of Bags n by A9;
u <> EmptyBag n by A10,TARSKI:def 1;
then c.u = 0.L by Def7;
hence thesis by A9,POLYNOM1:def 4;
end;
for u being object holds u in {EmptyBag n} implies u in Support c
proof
let u be object;
assume
A11: u in {EmptyBag n};
then
A12: u = EmptyBag n by TARSKI:def 1;
reconsider u as Element of Bags n by A11;
c.u <> 0.L by A6,A12,Lm2;
hence thesis by POLYNOM1:def 4;
end;
then Support c = {EmptyBag n} by A8,TARSKI:2;
then
A13: rng sg = {EmptyBag n} by A7,PRE_POLY:def 2;
then
A14: EmptyBag n in rng sg by TARSKI:def 1;
then
A15: 1 in dom sg by FINSEQ_3:31;
then
A16: sg.1 in rng sg by FUNCT_1:3;
A17: for u being object holds u in dom sg implies u in {1}
proof
let u be object;
assume
A18: u in dom sg;
assume
A19: not u in {1};
reconsider u as Element of NAT by A18;
sg/.u = sg.u by A18,PARTFUN1:def 6;
then
A20: sg/.u in rng sg by A18,FUNCT_1:3;
A21: u <> 1 by A19,TARSKI:def 1;
A22: 1 < u
proof
consider k being Nat such that
A23: dom sg = Seg k by FINSEQ_1:def 2;
Seg k = {m where m is Nat : 1 <= m & m <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23;
hence thesis by A21,XXREAL_0:1;
end;
sg/.1 = sg.1 by A14,A18,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A15,FUNCT_1:3;
then sg/.1 = EmptyBag n by A13,TARSKI:def 1
.= sg/.u by A13,A20,TARSKI:def 1;
hence thesis by A7,A15,A18,A22,PRE_POLY:def 2;
end;
for u being object holds u in {1} implies u in dom sg
by A15,TARSKI:def 1;
then
A24: dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2;
then
A25: 1 in dom sg by FINSEQ_1:2,TARSKI:def 1;
sg/.1 = sg.1 by A15,PARTFUN1:def 6;
then sg/.1 in rng sg by A25,FUNCT_1:3;
then
A26: sg/.1 = EmptyBag n by A13,TARSKI:def 1;
A27: len sg = 1 by A24,FINSEQ_1:def 3;
dom c = Bags n by FUNCT_2:def 1;
then 1 in dom (c * sg) by A13,A15,A16,FUNCT_1:11;
then
A28: (c * sg)/.1 = (c * sg).1 by PARTFUN1:def 6
.= c.(sg.1) by A15,FUNCT_1:13
.= c.(EmptyBag n) by A13,A16,TARSKI:def 1
.= coefficient(c) by Lm2;
dom y = Seg(len y) by FINSEQ_1:def 3
.= dom sg by A1,FINSEQ_1:def 3;
then y.1 = y/.1 by A25,PARTFUN1:def 6
.= coefficient(c) * eval(EmptyBag n,x) by A1,A3,A27,A26,A28
.= coefficient(c) * 1.L by POLYNOM2:14
.= coefficient(c);
then y = <* coefficient(c) *> by A1,A27,FINSEQ_1:40;
hence thesis by A2,RLVECT_1:44;
end;
end;
hence thesis;
end;
theorem Th25:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, a
being Element of L, x being Function of n,L holds eval(a |(n,L),x) = a
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, a be Element of L, x be
Function of n,L;
thus eval(a |(n,L),x) = coefficient(a |(n,L)) by Th24
.= a by Th23;
end;
begin :: Multiplication with Coefficients
definition
let X be set, L be non empty multLoopStr_0, p be Series of X,L, a be Element
of L;
func a * p -> Series of X,L means
:Def9:
for b being bag of X holds it.b = a * p.b;
existence
proof
deffunc F(Element of Bags X) = a * p.$1;
consider f being Function of Bags X, the carrier of L such that
A1: for x being Element of Bags X holds f.x = F(x) from FUNCT_2:sch 4;
reconsider f as Function of Bags X,L;
reconsider f as Series of X,L;
reconsider f as Series of X,L;
take f;
let x be bag of X;
x in Bags X by PRE_POLY:def 12;
hence thesis by A1;
end;
uniqueness
proof
let p1,p2 be Series of X,L such that
A2: for b being bag of X holds p1.b = a * p.b and
A3: for b being bag of X holds p2.b = a * p.b;
now
let b be Element of Bags X;
reconsider b9 = b as bag of X;
thus p1.b = a * p.b9 by A2
.= p2.b by A3;
end;
hence p1 = p2;
end;
func p * a -> Series of X,L means
:Def10:
for b being bag of X holds it.b = p.b * a;
existence
proof
deffunc F(Element of Bags X) = p.$1 * a;
consider f being Function of Bags X, the carrier of L such that
A4: for x being Element of Bags X holds f.x = F(x) from FUNCT_2:sch 4;
reconsider f as Function of Bags X,L;
reconsider f as Series of X,L;
reconsider f as Series of X,L;
take f;
let x be bag of X;
x in Bags X by PRE_POLY:def 12;
hence thesis by A4;
end;
uniqueness
proof
let p1,p2 be Series of X,L such that
A5: for b being bag of X holds p1.b = p.b * a and
A6: for b being bag of X holds p2.b = p.b * a;
now
let b be Element of Bags X;
reconsider b9 = b as bag of X;
thus p1.b = p.b9 * a by A5
.= p2.b by A6;
end;
hence p1 = p2;
end;
end;
registration
let X be set, L be left_zeroed right_zeroed add-cancelable distributive non
empty doubleLoopStr, p be finite-Support Series of X,L, a be Element of L;
cluster a * p -> finite-Support;
coherence
proof
set ap = a * p;
now
let u be object;
assume
A1: u in Support ap;
then reconsider u9 = u as Element of Bags X;
ap.u <> 0.L by A1,POLYNOM1:def 4;
then a * p.u9 <> 0.L by Def9;
then p.u9 <> 0.L by BINOM:2;
hence u in Support p by POLYNOM1:def 4;
end;
then Support p is finite & Support ap c= Support p by POLYNOM1:def 5
,TARSKI:def 3;
hence thesis by POLYNOM1:def 5;
end;
cluster p * a -> finite-Support;
coherence
proof
set ap = p * a;
now
let u be object;
assume
A2: u in Support ap;
then reconsider u9 = u as Element of Bags X;
ap.u <> 0.L by A2,POLYNOM1:def 4;
then p.u9 * a <> 0.L by Def10;
then p.u9 <> 0.L by BINOM:1;
hence u in Support p by POLYNOM1:def 4;
end;
then Support p is finite & Support ap c= Support p by POLYNOM1:def 5
,TARSKI:def 3;
hence thesis by POLYNOM1:def 5;
end;
end;
theorem
for X being set, L being commutative non empty multLoopStr_0, p
being Series of X,L, a being Element of L holds a * p = p * a
proof
let n be set, L be commutative non empty multLoopStr_0, p be Series of n,L
, a be Element of L;
now
let b be Element of Bags n;
reconsider b9 = b as bag of n;
thus (a * p).b = a * p.b9 by Def9
.= (p * a).b by Def10;
end;
hence thesis;
end;
theorem Th27:
for n being Ordinal, L being add-associative
right_complementable right_zeroed left-distributive non empty doubleLoopStr,
p being Series of n,L, a being Element of L holds a * p = a |(n,L) *' p
proof
let n be Ordinal, L be add-associative right_complementable
left-distributive right_zeroed non empty doubleLoopStr, p be Series of n,L, a
be Element of L;
for x being object st x in Bags n holds (a * p).x = (a |(n,L) *' p).x
proof
set O = a |(n,L), cL = the carrier of L;
let x be object;
assume x in Bags n;
then reconsider b = x as bag of n;
A1: for b being Element of Bags n holds (a |(n,L) *' p).b = a * p.b
proof
let b be Element of Bags n;
consider s being FinSequence of cL such that
A2: (O*'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 = (O.b1)*(p.b2) by POLYNOM1:def 10;
s is non empty by A3;
then consider
s1 being Element of cL, t being FinSequence of cL such that
A5: s1 = s.1 and
A6: s = <*s1*>^t by FINSEQ_3:102;
A7: Sum s = (Sum <*s1*>) + (Sum t) by A6,RLVECT_1:41;
A8: now
per cases;
suppose
t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:43;
end;
suppose
A9: t <> <*>(cL);
now
let k be Nat;
A10: len s = len t + len <*s1*> by A6,FINSEQ_1:22
.= len t +1 by FINSEQ_1:39;
assume
A11: k in dom t;
then
A12: t/.k = t.k by PARTFUN1:def 6
.= s.(k+1) by A6,A11,FINSEQ_3:103;
1 <= k by A11,FINSEQ_3:25;
then
A13: 1 < k+1 by NAT_1:13;
k <= len t by A11,FINSEQ_3:25;
then
A14: k+1 <= len s by A10,XREAL_1:6;
then
A15: k+1 in dom decomp b by A3,A13,FINSEQ_3:25;
A16: dom s = dom decomp b by A3,FINSEQ_3:29;
then
A17: s/.(k+1) = s.(k+1) by A15,PARTFUN1:def 6;
per cases by A14,XXREAL_0:1;
suppose
A18: k+1 < len s;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
consider b1, b2 being bag of n such that
A19: (decomp b)/.(k1+1) = <*b1, b2*> and
A20: s/.(k1+1) = O.b1*p.b2 by A4,A16,A15;
b1 <> EmptyBag n by A3,A13,A18,A19,PRE_POLY:72;
hence t/.k = 0.L*p.b2 by A12,A17,A20,Th18
.= 0.L;
end;
suppose
A21: k+1 = len s;
A22: now
assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73;
then len t +1 = 0+1 by A3,A10,FINSEQ_1:39;
hence contradiction by A9;
end;
consider b1, b2 being bag of n such that
A23: (decomp b)/.(k+1) = <*b1, b2*> and
A24: s/.(k+1) = O.b1*p.b2 by A4,A16,A15;
(decomp b)/.(len s) = <*b,EmptyBag n*> by A3,PRE_POLY:71;
then b2 = EmptyBag n & b1 = b by A21,A23,FINSEQ_1:77;
then s.(k+1) = 0.L*(p.EmptyBag n) by A17,A24,A22,Th18
.= 0.L;
hence t/.k = 0.L by A12;
end;
end;
hence Sum t = 0.L by MATRLIN:11;
end;
end;
A25: s is non empty by A3;
then consider b1, b2 being bag of n such that
A26: (decomp b)/.1 = <*b1, b2*> and
A27: s/.1 = O.b1*p.b2 by A4,FINSEQ_5:6;
1 in dom s by A25,FINSEQ_5:6;
then
A28: s/.1 = s.1 by PARTFUN1:def 6;
(decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71;
then
A29: b2 = b & b1 = EmptyBag n by A26,FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= a * p.b by A5,A27,A29,A28,Th18;
hence thesis by A2,A7,A8,RLVECT_1:4;
end;
b is Element of Bags n by PRE_POLY:def 12;
then (O*'p).b = a * p.b by A1
.= (a * p).b by Def9;
hence thesis;
end;
hence thesis;
end;
theorem Th28:
for n being Ordinal, L being add-associative
right_complementable right_zeroed right-distributive non empty doubleLoopStr,
p being Series of n,L, a being Element of L holds p * a = p *' (a |(n,L))
proof
let n be Ordinal, L be add-associative right_complementable
right-distributive right_zeroed non empty doubleLoopStr, p be Series of n,L,
a be Element of L;
for x being object st x in Bags n holds (p * a).x = (p *' (a |(n,L))).x
proof
set O = a |(n,L), cL = the carrier of L;
let x be object;
assume x in Bags n;
then reconsider b = x as bag of n;
A1: for b being Element of Bags n holds (p *' (a |(n,L))).b = p.b * a
proof
let b be Element of Bags n;
consider s being FinSequence of cL such that
A2: (p*'O).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)*(O.b2) by POLYNOM1:def 10;
consider t being FinSequence of cL,s1 being Element of cL such that
A5: s = t^<*s1*> by A3,FINSEQ_2:19;
A6: now
per cases;
suppose
t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:43;
end;
suppose
A7: t <> <*>(cL);
now
let k be Nat;
A8: len s = len t + len <*s1*> by A5,FINSEQ_1:22
.= len t +1 by FINSEQ_1:39;
assume
A9: k in dom t;
then
A10: t/.k = t.k by PARTFUN1:def 6
.= s.k by A5,A9,FINSEQ_1:def 7;
k <= len t by A9,FINSEQ_3:25;
then
A11: k < len s by A8,NAT_1:13;
A12: 1 <= k by A9,FINSEQ_3:25;
then
A13: k in dom decomp b by A3,A11,FINSEQ_3:25;
A14: dom s = dom decomp b by A3,FINSEQ_3:29;
then
A15: s/.k = s.k by A13,PARTFUN1:def 6;
per cases by A12,XXREAL_0:1;
suppose
A16: 1 < k;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
consider b1, b2 being bag of n such that
A17: (decomp b)/.k1 = <*b1, b2*> and
A18: s/.k1 = p.b1*O.b2 by A4,A14,A13;
b2 <> EmptyBag n by A3,A11,A16,A17,PRE_POLY:72;
hence t/.k = p.b1*0.L by A10,A15,A18,Th18
.= 0.L;
end;
suppose
A19: k = 1;
A20: now
assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73;
then len t +1 = 0+1 by A3,A8,FINSEQ_1:39;
hence contradiction by A7;
end;
consider b1, b2 being bag of n such that
A21: (decomp b)/.k = <*b1, b2*> and
A22: s/.k = p.b1*O.b2 by A4,A14,A13;
(decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71;
then b1 = EmptyBag n & b2 = b by A19,A21,FINSEQ_1:77;
then s.k = (p.EmptyBag n)*0.L by A15,A22,A20,Th18
.= 0.L;
hence t/.k = 0.L by A10;
end;
end;
hence Sum t = 0.L by MATRLIN:11;
end;
end;
A23: s.len s = (t^<*s1*>).(len t +1) by A5,FINSEQ_2:16
.= s1 by FINSEQ_1:42;
A24: Sum s = (Sum t) + (Sum <*s1*>) by A5,RLVECT_1:41;
s is non empty by A3;
then
A25: len s in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A26: (decomp b)/.len s = <*b1, b2*> and
A27: s/.len s = p.b1*O.b2 by A4;
A28: s/.len s = s.len s by A25,PARTFUN1:def 6;
(decomp b)/.len s = <*b,EmptyBag n*> by A3,PRE_POLY:71;
then
A29: b1 = b & b2 = EmptyBag n by A26,FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= p.b * a by A27,A29,A28,A23,Th18;
hence thesis by A2,A24,A6,RLVECT_1:4;
end;
b is Element of Bags n by PRE_POLY:def 12;
then (p*'O).b = p.b * a by A1
.= (p * a).b by Def10;
hence thesis;
end;
hence thesis;
end;
Lm4: for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval((a |(n,L))*'p,x) = a * eval(p,
x)
proof
let n be Ordinal, L be left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative Abelian distributive
non trivial doubleLoopStr, p be Polynomial of n,L, a be Element of L, x being
Function of n,L;
thus eval((a |(n,L))*'p,x) = eval(a |(n,L),x) * eval(p,x) by POLYNOM2:25
.= a * eval(p,x) by Th25;
end;
Lm5: for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(p*'(a |(n,L)),x) = eval(p,x) *
a
proof
let n be Ordinal, L be left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative Abelian distributive
non trivial doubleLoopStr, p be Polynomial of n,L, a be Element of L, x being
Function of n,L;
thus eval(p*'(a |(n,L)),x) = eval(p,x) * eval(a |(n,L),x) by POLYNOM2:25
.= eval(p,x) * a by Th25;
end;
theorem
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(a*p,x) = a * eval(p,x)
proof
let n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative distributive non
trivial doubleLoopStr, p be Polynomial of n,L, a be Element of L, x be
Function of n,L;
thus eval(a*p,x) = eval((a |(n,L)) *' p,x) by Th27
.= a * eval(p,x) by Lm4;
end;
theorem
for n being Ordinal, L being left_zeroed right_zeroed
left_add-cancelable add-associative right_complementable well-unital
associative domRing-like distributive non trivial doubleLoopStr, p being
Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(a*p
,x) = a * eval(p,x)
proof
let n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable
add-associative right_complementable well-unital associative domRing-like
distributive non trivial doubleLoopStr, p be Polynomial of n,L, a be Element
of L, x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support(a*p)) and
A2: eval(a*p,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = ((a*p
) * SgmX(BagOrder n, Support(a*p)))/.i * eval(((SgmX(BagOrder n, Support(a*p)))
/.i),x) by POLYNOM2:def 4;
A4: BagOrder n linearly_orders Support(a*p) by POLYNOM2:18;
consider z being FinSequence of the carrier of L such that
A5: len z = len SgmX(BagOrder n, Support p) and
A6: eval(p,x) = Sum z and
A7: for i being Element of NAT st 1 <= i & i <= len z holds z/.i = (p *
SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x)
by POLYNOM2:def 4;
per cases;
suppose
A8: a = 0.L;
A9: now
let b be bag of n;
thus (a*p).b = a * p.b by Def9
.= 0.L by A8;
end;
now
assume Support(a*p) <> {};
then reconsider sp = Support(a*p) as non empty Subset of Bags n;
set c = the Element of sp;
(a*p).c <> 0.L by POLYNOM1:def 4;
hence contradiction by A9;
end;
then rng(SgmX(BagOrder n, Support(a*p))) = {} by A4,PRE_POLY:def 2;
then SgmX(BagOrder n, Support(a*p)) = {} by RELAT_1:41;
then y = <*>(the carrier of L) by A1;
then Sum y = 0.L by RLVECT_1:43
.= a * Sum z by A8;
hence thesis by A2,A6;
end;
suppose
A10: a <> 0.L;
A11: for u being object holds u in Support(a*p) implies u in Support p
proof
let u be object;
assume
A12: u in Support(a*p);
then reconsider u9 = u as Element of Bags n;
(a*p).u <> 0.L by A12,POLYNOM1:def 4;
then a * p.u9 <> 0.L by Def9;
then p.u9 <> 0.L;
hence thesis by POLYNOM1:def 4;
end;
A13: for u being object holds u in Support p implies u in Support(a*p)
proof
let u be object;
assume
A14: u in Support p;
then reconsider u9 = u as Element of Bags n;
p.u <> 0.L by A14,POLYNOM1:def 4;
then a * p.u9 <> 0.L by A10,VECTSP_2:def 1;
then (a * p).u9 <> 0.L by Def9;
hence thesis by POLYNOM1:def 4;
end;
then
A15: len z = len y by A1,A5,A11,TARSKI:2;
then
A16: dom z = Seg(len y) by FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3;
A17: Support(a*p) = Support(p) by A13,A11,TARSKI:2;
now
A18: dom(a*p) = Bags n by FUNCT_2:def 1;
now
let u be object;
assume u in rng(SgmX(BagOrder n, Support(a*p)));
then u in Support(a*p) by A4,PRE_POLY:def 2;
hence u in dom(a*p) by A18;
end;
then rng SgmX(BagOrder n, Support(a*p)) c= dom(a*p) by TARSKI:def 3;
then reconsider
r = (a*p) * SgmX(BagOrder n, Support(a*p)) as FinSequence by FINSEQ_1:16;
for u being object holds u in rng r implies u in the carrier of L
proof
let u be object;
assume u in rng r;
then
A19: u in rng(a*p) by FUNCT_1:14;
rng(a*p) c= the carrier of L by RELAT_1:def 19;
hence thesis by A19;
end;
then
A20: rng r c= the carrier of L by TARSKI:def 3;
A21: dom p = Bags n by FUNCT_2:def 1;
now
let u be object;
assume u in rng(SgmX(BagOrder n, Support(a*p)));
then u in Support(a*p) by A4,PRE_POLY:def 2;
hence u in dom p by A21;
end;
then rng SgmX(BagOrder n, Support(a*p)) c= dom p by TARSKI:def 3;
then reconsider
q = p * SgmX(BagOrder n, Support(a*p)) as FinSequence by FINSEQ_1:16;
for u being object holds u in rng q implies u in the carrier of L
proof
let u be object;
assume u in rng q;
then
A22: u in rng p by FUNCT_1:14;
rng p c= the carrier of L by RELAT_1:def 19;
hence thesis by A22;
end;
then
A23: rng q c= the carrier of L by TARSKI:def 3;
reconsider r as FinSequence of the carrier of L by A20,FINSEQ_1:def 4;
reconsider q as FinSequence of the carrier of L by A23,FINSEQ_1:def 4;
let i be object;
assume
A24: i in dom z;
then i in Seg(len z) by FINSEQ_1:def 3;
then i in { k where k is Nat : 1 <= k & k <= len z } by FINSEQ_1:def 1;
then consider k being Nat such that
A25: i = k and
A26: 1 <= k & k <= len z;
reconsider k as Element of NAT by ORDINAL1:def 12;
A27: dom z = Seg(len SgmX(BagOrder n, Support(a*p))) by A1,A16,FINSEQ_1:def 3
.= dom(SgmX(BagOrder n, Support(a*p))) by FINSEQ_1:def 3;
then
(SgmX(BagOrder n, Support(a*p))).k = (SgmX(BagOrder n, Support(a*p)
))/.k by A24,A25,PARTFUN1:def 6;
then k in dom q by A24,A25,A27,A21,FUNCT_1:11;
then
A28: (p * SgmX(BagOrder n, Support(a*p)))/.k = q.k by PARTFUN1:def 6
.= p.(SgmX(BagOrder n, Support(a*p)).k) by A24,A25,A27,FUNCT_1:13
.= p.(SgmX(BagOrder n, Support(a*p))/.k) by A24,A25,A27,PARTFUN1:def 6;
reconsider c = SgmX(BagOrder n, Support(a*p))/.k as Element of Bags n;
reconsider c as bag of n;
A29: a * z/.k = a * ((p * SgmX(BagOrder n, Support p))/.k * eval(((SgmX(
BagOrder n, Support p))/.k),x)) by A7,A26
.= (a * (p * SgmX(BagOrder n, Support(a*p)))/.k) * eval(((SgmX(
BagOrder n, Support(a*p)))/.k),x) by A17,GROUP_1:def 3;
A30: (a*p).(SgmX(BagOrder n, Support(a*p))/.k)
= a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A28,Def9;
(SgmX(BagOrder n, Support(a*p))).k = (SgmX(BagOrder n, Support(a*p)
))/.k by A24,A25,A27,PARTFUN1:def 6;
then k in dom r by A24,A25,A27,A18,FUNCT_1:11;
then ((a*p) * SgmX(BagOrder n, Support(a*p)))/.k = r.k by PARTFUN1:def 6
.= (a*p).(SgmX(BagOrder n, Support(a*p)).k) by A24,A25,A27,FUNCT_1:13
.= a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A24,A25,A27,A30,
PARTFUN1:def 6;
hence y/.i = a * z/.i by A3,A15,A25,A26,A29;
end;
then y = a * z by A16,POLYNOM1:def 1;
hence thesis by A2,A6,BINOM:4;
end;
end;
theorem
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(p*a,x) = eval(p,x) * a
proof
let n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative distributive non
trivial doubleLoopStr, p be Polynomial of n,L, a be Element of L, x be
Function of n,L;
thus eval(p*a,x) = eval(p*'(a |(n,L)),x) by Th28
.= eval(p,x) * a by Lm5;
end;
theorem
for n being Ordinal, L being left_zeroed right_zeroed
left_add-cancelable add-associative right_complementable well-unital
associative commutative distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, a being Element of L, x being Function of n,L holds
eval(p*a,x) = eval(p,x) * a
proof
let n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable
add-associative right_complementable well-unital associative commutative
distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n,L,
a be Element of L, x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support(p*a)) and
A2: eval(p*a,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = ((p*a
) * SgmX(BagOrder n, Support(p*a)))/.i * eval(((SgmX(BagOrder n, Support(p*a)))
/.i),x) by POLYNOM2:def 4;
consider z being FinSequence of the carrier of L such that
A4: len z = len SgmX(BagOrder n, Support p) and
A5: eval(p,x) = Sum z and
A6: for i being Element of NAT st 1 <= i & i <= len z holds z/.i = (p *
SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x)
by POLYNOM2:def 4;
now
per cases;
case
A7: a = 0.L;
A8: now
let b be bag of n;
thus (p*a).b = p.b * a by Def10
.= 0.L by A7;
end;
A9: now
assume Support(p*a) <> {};
then reconsider sp = Support(p*a) as non empty Subset of Bags n;
set c = the Element of sp;
(p*a).c <> 0.L by POLYNOM1:def 4;
hence contradiction by A8;
end;
BagOrder n linearly_orders Support(p*a) by POLYNOM2:18;
then rng(SgmX(BagOrder n, Support(p*a))) = {} by A9,PRE_POLY:def 2;
then SgmX(BagOrder n, Support(p*a)) = {} by RELAT_1:41;
then y = <*>(the carrier of L) by A1;
then Sum y = 0.L by RLVECT_1:43
.= Sum z * a by A7;
hence thesis by A2,A5;
end;
case
A10: a <> 0.L;
A11: for u being object holds u in Support(p*a) implies u in Support p
proof
let u be object;
assume
A12: u in Support(p*a);
then reconsider u9 = u as Element of Bags n;
(p*a).u <> 0.L by A12,POLYNOM1:def 4;
then p.u9 * a <> 0.L by Def10;
then p.u9 <> 0.L;
hence thesis by POLYNOM1:def 4;
end;
A13: for u being object holds u in Support p implies u in Support(p*a)
proof
let u be object;
assume
A14: u in Support p;
then reconsider u9 = u as Element of Bags n;
p.u <> 0.L by A14,POLYNOM1:def 4;
then p.u9 * a <> 0.L by A10,VECTSP_2:def 1;
then (p *a).u9 <> 0.L by Def10;
hence thesis by POLYNOM1:def 4;
end;
then
A15: len z = len y by A1,A4,A11,TARSKI:2;
then
A16: dom z = Seg(len y) by FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3;
A17: BagOrder n linearly_orders Support(p*a) by POLYNOM2:18;
A18: Support(p*a) = Support(p) by A13,A11,TARSKI:2;
now
A19: dom(p*a) = Bags n by FUNCT_2:def 1;
now
let u be object;
assume u in rng(SgmX(BagOrder n, Support(p*a)));
then u in Support(p*a) by A17,PRE_POLY:def 2;
hence u in dom(p*a) by A19;
end;
then rng SgmX(BagOrder n, Support(p*a)) c= dom(p*a) by TARSKI:def 3;
then reconsider
r = (p*a) * SgmX(BagOrder n, Support(p*a)) as FinSequence
by FINSEQ_1:16;
for u being object holds u in rng r implies u in the carrier of L
proof
let u be object;
assume u in rng r;
then
A20: u in rng(p*a) by FUNCT_1:14;
rng(p*a) c= the carrier of L by RELAT_1:def 19;
hence thesis by A20;
end;
then
A21: rng r c= the carrier of L by TARSKI:def 3;
A22: dom p = Bags n by FUNCT_2:def 1;
now
let u be object;
assume u in rng(SgmX(BagOrder n, Support(p*a)));
then u in Support(p*a) by A17,PRE_POLY:def 2;
hence u in dom p by A22;
end;
then rng SgmX(BagOrder n, Support(p*a)) c= dom p by TARSKI:def 3;
then reconsider
q = p * SgmX(BagOrder n, Support(p*a)) as FinSequence by FINSEQ_1:16;
for u being object holds u in rng q implies u in the carrier of L
proof
let u be object;
assume u in rng q;
then
A23: u in rng p by FUNCT_1:14;
rng p c= the carrier of L by RELAT_1:def 19;
hence thesis by A23;
end;
then
A24: rng q c= the carrier of L by TARSKI:def 3;
reconsider r as FinSequence of the carrier of L by A21,FINSEQ_1:def 4;
reconsider q as FinSequence of the carrier of L by A24,FINSEQ_1:def 4;
let i be object;
assume
A25: i in dom z;
then i in Seg(len z) by FINSEQ_1:def 3;
then
i in { k where k is Nat : 1 <= k & k <= len z } by FINSEQ_1:def 1;
then consider k being Nat such that
A26: i = k and
A27: 1 <= k & k <= len z;
reconsider k as Element of NAT by ORDINAL1:def 12;
A28: dom z = Seg(len SgmX(BagOrder n, Support(p*a))) by A1,A16,
FINSEQ_1:def 3
.= dom(SgmX(BagOrder n, Support(p*a))) by FINSEQ_1:def 3;
then
(SgmX(BagOrder n, Support(p*a))).k = (SgmX(BagOrder n, Support(p*
a)))/.k by A25,A26,PARTFUN1:def 6;
then k in dom q by A25,A26,A28,A22,FUNCT_1:11;
then
A29: (p * SgmX(BagOrder n, Support(p*a)))/.k = q.k by PARTFUN1:def 6
.= p.(SgmX(BagOrder n, Support(p*a)).k) by A25,A26,A28,FUNCT_1:13
.= p.(SgmX(BagOrder n, Support(p*a))/.k) by A25,A26,A28,
PARTFUN1:def 6;
reconsider c = SgmX(BagOrder n, Support(p*a))/.k as Element of Bags n;
reconsider c as bag of n;
A30: z/.k * a = (p * SgmX(BagOrder n, Support(p*a)))/.k * (eval(((SgmX
(BagOrder n, Support(p*a)))/.k),x)) * a by A6,A18,A27
.= ((p * SgmX(BagOrder n, Support(p*a)))/.k * a) * eval(((SgmX(
BagOrder n, Support(p*a)))/.k),x) by GROUP_1:def 3;
A31: (p*a).(SgmX(BagOrder n, Support(p*a))/.k)
= (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A29,Def10;
(SgmX(BagOrder n, Support(p*a))).k = (SgmX(BagOrder n, Support(p*
a)))/.k by A25,A26,A28,PARTFUN1:def 6;
then k in dom r by A25,A26,A28,A19,FUNCT_1:11;
then ((p*a) * SgmX(BagOrder n, Support(p*a)))/.k = r.k by
PARTFUN1:def 6
.= (p*a).(SgmX(BagOrder n, Support(p*a)).k) by A25,A26,A28,FUNCT_1:13
.= (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A25,A26,A28,A31,
PARTFUN1:def 6;
hence y/.i = z/.i * a by A3,A15,A26,A27,A30;
end;
then y = z * a by A16,POLYNOM1:def 2;
hence thesis by A2,A5,BINOM:5;
end;
end;
hence thesis;
end;
theorem
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval((a |(n,L))*'p,x) = a * eval(p,
x) by Lm4;
theorem
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(p*'(a |(n,L)),x) = eval(p,x) *
a
proof
let n be Ordinal, L be left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative Abelian distributive
non trivial doubleLoopStr, p be Polynomial of n,L, a be Element of L, x being
Function of n,L;
thus eval(p*'(a |(n,L)),x) = eval(p,x) * eval(a |(n,L),x) by POLYNOM2:25
.= eval(p,x) * a by Th25;
end;