Copyright (c) 2001 Association of Mizar Users
environ
vocabulary POLYNOM1, POLYNOM2, POLYNOM7, BOOLE, FUNCT_1, CAT_1, TRIANG_1,
FINSEQ_1, ALGSTR_1, ALGSTR_2, VECTSP_1, RLVECT_1, ORDINAL1, LATTICES,
ALGSEQ_1, QUOFIELD, ORDERS_2, ANPROJ_1, QC_LANG1, FUNCOP_1, FINSET_1,
PRE_TOPC, CAT_3, FUNCT_4, GRCAT_1, ENDALG, GROUP_1, ARYTM_3, RELAT_1,
REALSET1, BINOP_1, FINSEQ_4, COHSP_1, VECTSP_2, BINOM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, STRUCT_0, RELAT_1,
BINOM, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4,
NAT_1, ALGSTR_1, RLVECT_1, ORDERS_2, FINSEQ_1, CQC_LANG, FUNCOP_1,
GROUP_1, QUOFIELD, PRE_TOPC, GRCAT_1, ENDALG, TRIANG_1, REALSET1,
VECTSP_2, POLYNOM1, POLYNOM2, VECTSP_1, FINSEQ_4;
constructors ORDERS_2, CQC_LANG, WELLFND1, ALGSTR_2, QUOFIELD, BINOM, GRCAT_1,
TRIANG_1, ENDALG, MONOID_0, POLYNOM2, MEMBERED;
clusters STRUCT_0, FINSET_1, RELSET_1, FUNCOP_1, CQC_LANG, ORDINAL1, VECTSP_2,
CARD_1, ALGSTR_1, BINOM, POLYNOM1, POLYNOM2, MONOID_0, VECTSP_1,
MEMBERED;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
theorems TARSKI, RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1,
VECTSP_1, POLYNOM1, PBOOLE, STRUCT_0, QUOFIELD, REAL_1, FUNCT_7, FUNCT_4,
CQC_LANG, ENDALG, FINSEQ_4, GRCAT_1, BINOM, TRIANG_1, FINSEQ_3, RLVECT_1,
FUNCOP_1, REALSET1, VECTSP_2, GROUP_1, FINSET_1, NAT_1, FINSEQ_2, AXIOMS,
FSM_1, GROUP_7, FINSEQ_5, MATRLIN, POLYNOM2, XBOOLE_0, XCMPLX_1;
schemes FUNCT_2;
begin
definition
cluster non trivial (non empty ZeroStr);
existence
proof
consider R being non degenerated comRing;
take R;
thus thesis;
end;
end;
definition
cluster non trivial -> non empty ZeroStr;
coherence
proof
let R be ZeroStr;
assume R is non trivial;
then the carrier of R is non trivial by REALSET1:def 13;
then not(the carrier of R is empty or
ex x being set st the carrier of R = {x}) by REALSET1:def 12;
hence thesis by STRUCT_0:def 1;
end;
end;
definition
cluster Abelian left_zeroed right_zeroed add-associative
right_complementable unital associative commutative
distributive domRing-like (non trivial doubleLoopStr);
existence
proof
consider R being domRing;
take R;
thus thesis;
end;
end;
definition
let R be non trivial ZeroStr;
cluster non-zero Element of R;
existence
proof
consider a being Element of (the carrier of R)\{0.R};
the carrier of R is non trivial by REALSET1:def 13;
then (the carrier of R)\{0.R} is non empty by REALSET1:32;
then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
then reconsider a as Element of R;
take a;
a <> 0.R by A1,TARSKI:def 1;
hence thesis by RLVECT_1:def 13;
end;
end;
definition
let X be set,
R be non empty ZeroStr,
p be Series of X,R;
canceled;
attr p is non-zero means :Def2:
p <> 0_(X,R);
end;
definition
let X be set,
R be non trivial ZeroStr;
cluster non-zero Series of X,R;
existence
proof
consider a being Element of (the carrier of R)\{0.R};
the carrier of R is non trivial by REALSET1:def 13;
then (the carrier of R)\{0.R} is non empty by REALSET1:32;
then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
then 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 24;
then dom 0_(X,R) = Bags X by FUNCOP_1:19;
then A2: p.(EmptyBag X) = a by FUNCT_7:33;
a <> 0.R by A1,TARSKI:def 1;
then p <> 0_(X,R) by A2,POLYNOM1:81;
hence thesis by Def2;
end;
end;
definition
let n be Ordinal,
R be non trivial ZeroStr;
cluster non-zero Polynomial of n,R;
existence
proof
consider a being Element of (the carrier of R)\{0.R};
the carrier of R is non trivial by REALSET1:def 13;
then (the carrier of R)\{0.R} is non empty by REALSET1:32;
then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
then 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 ;
0_(n,R) = (Bags n --> 0.R) by POLYNOM1:def 24;
then dom 0_(n,R) = Bags n by FUNCOP_1:19;
then A2: p.(EmptyBag n) = a by FUNCT_7:33;
A3: now let u be set;
assume u in {EmptyBag n};
then A4: u = EmptyBag n by TARSKI:def 1;
a <> 0.R by A1,TARSKI:def 1;
hence u in Support p by A2,A4,POLYNOM1:def 9;
end;
now let u be set;
assume A5: u in Support p;
then A6: u is Element of Bags n;
now assume u <> EmptyBag n;
then p.u = (0_(n,R)).u by FUNCT_7:34
.= 0.R by A6,POLYNOM1:81;
hence contradiction by A5,POLYNOM1:def 9;
end;
hence u in {EmptyBag n} by TARSKI:def 1;
end;
then Support p = {EmptyBag n} by A3,TARSKI:2;
then reconsider p as Polynomial of n,R by POLYNOM1:def 10;
take p;
a <> 0.R by A1,TARSKI:def 1;
then p <> 0_(n,R) by A2,POLYNOM1:81;
hence thesis by Def2;
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: s = 0_(X,R);
now assume A3: Support s <> {};
consider x being Element of Support s;
A4: x in Support s by A3;
then reconsider x as bag of X by POLYNOM1:def 14;
s.x <> 0.R by A4,POLYNOM1:def 9;
hence contradiction by A2,POLYNOM1:81;
end;
hence Support s = {};
end;
now assume A5: Support s = {};
A6: dom s = Bags X & dom 0_(X,R) = Bags X by FUNCT_2:def 1;
now let x be set;
assume x in Bags X;
then reconsider x' = x as Element of Bags X;
s.x' = 0.R by A5,POLYNOM1:def 9;
hence s.x = (0_(X,R)).x by POLYNOM1:81;
end;
hence s = 0_(X,R) by A6,FUNCT_1:9;
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 assume ex s being Series of X,R st Support(s) <> {};
then consider s being Series of X,R such that
A2: Support(s) <> {};
consider b being Element of Support s;
b in Support s by A2;
then reconsider b as Element of Bags X;
now assume ex x being set st the carrier of R = {x};
then consider x being set such that
A3: the carrier of R = {x};
0.R = x by A3,TARSKI:def 1 .= s.b by A3,TARSKI:def 1;
hence contradiction by A2,POLYNOM1:def 9;
end;
then the carrier of R is non trivial by REALSET1:def 12;
hence R is non trivial by REALSET1:def 13;
end;
now assume R is non trivial;
then A4: the carrier of R is non trivial by REALSET1:def 13;
now assume A5: not(ex a being Element of R st a <> 0.R);
A6: for a be Element of R holds a = 0.R by A5;
ex x being set st the carrier of R = {x}
proof
take 0.R;
A7: for u being set holds u in {0.R} implies u in the carrier of R;
now let u be set;
assume u in the carrier of R;
then u = 0.R by A6;
hence u in {0.R} by TARSKI:def 1;
end;
hence thesis by A7,TARSKI:2;
end;
hence contradiction by A4,REALSET1:def 12;
end;
then consider a being Element of R such that
A8: a <> 0.R;
set s = (Bags X) --> a;
reconsider s as Function of Bags X,the carrier of R by FUNCOP_1:57;
reconsider s as Function of Bags X,R ;
reconsider s as Series of X,R ;
take s;
set x = EmptyBag X;
s.x = a by FUNCOP_1:13;
then EmptyBag X in Support s by A8,POLYNOM1:def 9;
hence ex s being Series of X,R st Support(s) <> {};
end;
hence thesis by A1;
end;
definition
let X be set,
b be bag of X;
attr b is univariate means :Def3:
ex u being Element of X st support b = {u};
end;
definition
let X be non empty set;
cluster univariate bag of X;
existence
proof
consider x being Element of X;
set b = EmptyBag X +* (x,1);
take b;
A1: dom (x.-->1) = {x} by CQC_LANG:5;
then A2: x in dom (x.-->1) by TARSKI:def 1;
A3: dom (EmptyBag X) = X by PBOOLE:def 3;
then b.x = ((EmptyBag X)+*(x.-->1)).x by FUNCT_7:def 3;
then A4: b.x = (x.-->1).x by A2,FUNCT_4:14
.= 1 by CQC_LANG:6;
A5: for u being set holds u in {x} implies u in support b
proof
let u be set;
assume u in {x};
then u = x by TARSKI:def 1;
hence thesis by A4,POLYNOM1:def 7;
end;
for u being set holds u in support b implies u in {x}
proof
let u be set;
assume A6: u in support b;
now assume u <> x;
then A7: not(u in dom (x.-->1)) by A1,TARSKI:def 1;
b.u = ((EmptyBag X)+*(x.-->1)).u by A3,FUNCT_7:def 3;
then b.u = (EmptyBag X).u by A7,FUNCT_4:12
.= 0 by POLYNOM1:56;
hence contradiction by A6,POLYNOM1:def 7;
end;
hence thesis by TARSKI:def 1;
end;
then support b = {x} by A5,TARSKI:2;
hence thesis by Def3;
end;
end;
definition
let X be non empty set;
cluster univariate -> non empty 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} by Def3;
x in support b by A1,TARSKI:def 1;
then b.x <> 0 by POLYNOM1:def 7;
then b.x <> (EmptyBag X).x by POLYNOM1:56;
hence thesis by POLYNOM2:def 1;
end;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Polynomials without Variables
begin
theorem
for b being bag of {} holds b = EmptyBag {}
proof
let b be bag of {};
set n = {};
A1: for b being bag of n holds b = {}
proof
let b be bag of n;
b in Bags n by POLYNOM1:def 14;
hence thesis by POLYNOM1:55,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
let L be (non empty doubleLoopStr),
p be Polynomial of {},L;
set n = {};
A1: for b being bag of {} holds b = {}
proof
let b be bag of {};
b in Bags {} by POLYNOM1:def 14;
hence thesis by POLYNOM1:55,TARSKI:def 1;
end;
then A2: EmptyBag n = {};
reconsider p as Function of Bags {},L;
reconsider p as Function of {{}},the carrier of L by POLYNOM1:55;
A3: dom p = {{}} by FUNCT_2:def 1 .= {EmptyBag n} by A1;
set a = p/.{};
take a;
A4: for u being set holds u in p implies u in [:{EmptyBag n},{a}:]
proof
let u be set;
assume A5: u in p;
then consider p1,p2 being set such that
A6: u = [p1,p2] by RELAT_1:def 1;
A7: p1 in dom p & p2 in rng p by A5,A6,RELAT_1:def 4,def 5;
then reconsider p1 as bag of n by A3,TARSKI:def 1;
A8: p1 = {} by A1;
then p2 = p.{} by A5,A6,A7,FUNCT_1:def 4
.= p/.{} by A7,A8,FINSEQ_4:def 4;
then p2 in {a} by TARSKI:def 1;
hence thesis by A3,A6,A7,ZFMISC_1:def 2;
end;
for u being set holds u in [:{EmptyBag n},{a}:] implies u in p
proof
let u be set;
assume u in [:{EmptyBag n},{a}:];
then consider u1,u2 being set such that
A9: u1 in {EmptyBag n} & u2 in {a} & u = [u1,u2] by ZFMISC_1:def 2;
A10: u1 = {} by A2,A9,TARSKI:def 1;
u2 = a by A9,TARSKI:def 1 .= p.{} by A3,A9,A10,FINSEQ_4:def 4;
hence thesis by A3,A9,A10,FUNCT_1:8;
end;
then p = [:{EmptyBag n},{a}:] by A4,TARSKI:2;
hence thesis by FUNCOP_1:def 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
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;
set n = {};
A1: for b being bag of n holds b = {}
proof
let b be bag of n;
b in Bags n by POLYNOM1:def 14;
hence thesis by POLYNOM1:55,TARSKI:def 1;
end;
then A2: EmptyBag n = {};
consider a being Element of L such that
A3: p = {EmptyBag n} --> a by Lm1;
A4: dom p = {EmptyBag n} by A3,FUNCOP_1:19;
A5: EmptyBag n in {EmptyBag n} by TARSKI:def 1;
then A6: p.(EmptyBag n) = a by A3,FUNCOP_1:13;
now per cases;
case A7: a = 0.L;
Support p = {}
proof
assume A8: Support p <> {};
consider u being Element of Support p;
u in Support p by A8;
then reconsider u as Element of Bags n;
p.u <> 0.L by A8,POLYNOM1:def 9;
hence thesis by A1,A2,A6,A7;
end;
then reconsider Sp = Support p as empty Subset of Bags n;
BagOrder n linearly_orders Sp by POLYNOM2:20;
then A9: SgmX(BagOrder n, Sp) = {} by POLYNOM2:9;
consider y being FinSequence of the carrier of L such that
A10: len y = len SgmX(BagOrder n, Support p) &
eval(p,x) = Sum y &
for i being 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;
len y = 0 by A9,A10,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
hence eval(p,x) = a by A7,A10,RLVECT_1:60;
case A11: a <> 0.L;
A12: for u being set holds u in Support p implies u in {{}}
proof
let u be set;
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 set holds u in {{}} implies u in Support p
proof
let u be set;
assume u in {{}};
then u = EmptyBag n by A2,TARSKI:def 1;
hence thesis by A6,A11,POLYNOM1:def 9;
end;
then A13: Support p = {{}} by A12,TARSKI:2;
reconsider sp = Support p as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sp);
A14: BagOrder n linearly_orders sp by POLYNOM2:20;
then A15: rng sg = {{}} &
for l,m being Nat st l in dom sg & m in dom sg & l < m
holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n)
by A13,TRIANG_1:def 2;
then {} in rng sg by TARSKI:def 1;
then A16: 1 in dom sg by FINSEQ_3:33;
then A17: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
for u being set holds u in dom sg implies u in {1}
proof
let u be set;
assume A18: u in dom sg;
assume A19: not(u in {1});
reconsider u as Nat by A18;
A20: u <> 1 by A19,TARSKI:def 1;
A21: 1 < u
proof
consider k being Nat such that A22: 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 consider m' being Nat such that
A23: m' = u & 1 <= m' & m' <= k by A18,A22;
thus thesis by A20,A23,REAL_1:def 5;
end;
sg/.1 = sg.1 & sg/.u = sg.u by A16,A18,FINSEQ_4:def 4;
then A24: sg/.1 in rng sg & sg/.u in rng sg by A16,A18,FUNCT_1:12;
then sg/.1 = {} by A15,TARSKI:def 1 .= sg/.u by A15,A24,TARSKI:def 1;
hence thesis by A14,A16,A18,A21,TRIANG_1:def 2;
end;
then dom sg = Seg 1 by A17,FINSEQ_1:4,TARSKI:2;
then A25: len sg = 1 by FINSEQ_1:def 3;
consider y being FinSequence of the carrier of L such that
A26: len y = len sg &
Sum y = eval(p,x) &
for i being Nat st 1 <= i & i <= len y holds
y/.i = (p * sg)/.i * eval((sg/.i)@,x) by POLYNOM2:def 4;
A27: sg.1 in rng sg by A16,FUNCT_1:12;
sg.1 in dom p by A2,A4,A15,A16,FUNCT_1:12;
then 1 in dom (p * sg) by A16,FUNCT_1:21;
then A28: (p * sg)/.1 = (p * sg).1 by FINSEQ_4:def 4
.= p.(sg.1) by A16,FUNCT_1:23
.= a by A2,A3,A15,A27,FUNCOP_1:13;
dom y = Seg(len y) by FINSEQ_1:def 3
.= dom sg by A26,FINSEQ_1:def 3;
then y.1 = y/.1 by A16,FINSEQ_4:def 4
.= (p * sg)/.1 * eval((sg/.1)@,x) by A25,A26
.= (p * sg)/.1 * eval(EmptyBag n,x) by A1,A2
.= (p * sg)/.1 * 1.L by POLYNOM2:16
.= (p * sg)/.1 * 1_ L by POLYNOM2:3
.= a by A28,VECTSP_1:def 13;
then y = <* a *> by A25,A26,FINSEQ_1:57;
hence eval(p,x) = a by A26,RLVECT_1:61;
end;
hence thesis by A3,A5,FUNCOP_1:13;
end;
theorem
for L being right_zeroed add-associative right_complementable
well-unital distributive (non trivial doubleLoopStr)
holds Polynom-Ring({},L) is_ringisomorph_to L
proof
let L be right_zeroed add-associative right_complementable
well-unital distributive
(non trivial doubleLoopStr);
set n = {};
set PL = Polynom-Ring(n,L);
A1: for b being bag of {} holds b = {}
proof
let b be bag of {};
b in Bags {} by POLYNOM1:def 14;
hence thesis by POLYNOM1:55,TARSKI:def 1;
end;
then A2: EmptyBag n = {};
then reconsider i = {} as bag of n;
defpred P[set,set] means
ex p being Polynomial of n,L st p = $1 & p.{} = $2;
A3: 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 27;
take p.{};
dom p = Bags n by FUNCT_2:def 1;
then A4: p.{} in rng p by A2,FUNCT_1:12;
rng p c= the carrier of L by RELSET_1:12;
hence thesis by A4;
end;
consider f being Function of the carrier of PL,the carrier of L
such that A5: for x being Element of PL holds P[x,f.x]
from FuncExD(A3);
A6: dom f = the carrier of PL by FUNCT_2:def 1;
reconsider f as map of PL,L;
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
A7: p = x & p.{} = f.x by A5;
consider q being Polynomial of n,L such that
A8: q = y & q.{} = f.y by A5;
consider a being Element of L such that
A9: p = {EmptyBag n} --> a by Lm1;
A10: EmptyBag n in {EmptyBag n} by TARSKI:def 1;
then A11: p.{} = a by A2,A9,FUNCOP_1:13;
consider b being Element of L such that
A12: q = {EmptyBag n} --> b by Lm1;
q.{} = b by A2,A10,A12,FUNCOP_1:13;
then A13: f.x + f.y = a + b by A2,A7,A8,A9,A10,FUNCOP_1:13;
consider pq being Polynomial of n,L such that
A14: pq = x + y & pq.{} = f.(x+y) by A5;
(p+q).{} = p.i + q.i by POLYNOM1:def 21 .= a + b by A2,A10,A11,A12,FUNCOP_1
:13;
hence thesis by A7,A8,A13,A14,POLYNOM1:def 27;
end;
then A15: f is additive by GRCAT_1:def 13;
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
A16: p = x & p.{} = f.x by A5;
consider q being Polynomial of n,L such that
A17: q = y & q.{} = f.y by A5;
consider pq being Polynomial of n,L such that
A18: pq = x * y & pq.{} = f.(x*y) by A5;
(p*'q).{} = p.i * q.i
proof
set z = p.i * q.i;
A19: decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> by POLYNOM1:77;
then A20: len decomp EmptyBag n = 1 by FINSEQ_1:56;
consider s being FinSequence of the carrier of L such that
A21: (p*'q).(EmptyBag n) = Sum s &
len s = len decomp EmptyBag n &
for k being 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 26;
len s = 1 by A19,A21,FINSEQ_1:56;
then Seg 1 = dom s by FINSEQ_1:def 3;
then A22: 1 in dom s by FINSEQ_1:4,TARSKI:def 1;
then consider b1,b2 being bag of n such that
A23: (decomp EmptyBag n)/.1 = <*b1, b2*> &
s/.1 = p.b1*q.b2 by A21;
s.1 = p.b1 * q.b2 by A22,A23,FINSEQ_4:def 4
.= p.i * q.b2 by A1
.= p.i * q.i by A1;
then s = <* z *> by A20,A21,FINSEQ_1:57;
then Sum s = z by RLVECT_1:61;
hence thesis by A1,A21;
end;
hence thesis by A16,A17,A18,POLYNOM1:def 27;
end;
then A24: f is multiplicative by ENDALG:def 7;
consider p being Polynomial of n,L such that
A25: p = 1_ PL & p.{} = f.(1_ PL) by A5;
A26: p = 1_(n,L) by A25,POLYNOM1:def 27
.= 0_(n,L)+*(EmptyBag n,1.L) by POLYNOM1:def 25;
A27: dom 0_(n,L) = Bags n by FUNCT_2:def 1;
dom(EmptyBag n .--> 1.L) = {EmptyBag n} by CQC_LANG:5;
then A28: EmptyBag n in dom(EmptyBag n .--> 1.L) by TARSKI:def 1;
p.i = p.(EmptyBag n) by A1
.= (0_(n,L)+*(EmptyBag n .--> 1.L)).(EmptyBag n) by A26,A27,FUNCT_7:def 3
.= (EmptyBag n .--> 1.L).(EmptyBag n) by A28,FUNCT_4:14
.= 1.L by CQC_LANG:6
.= 1_ L by POLYNOM2:3;
then f is unity-preserving by A25,ENDALG:def 8;
then A29: f is RingHomomorphism by A15,A24,QUOFIELD:def 21;
for x1,x2 being set
st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be set;
assume A30: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then reconsider x1,x2 as Element of PL;
consider p being Polynomial of n,L such that
A31: p = x1 & p.{} = f.x1 by A5;
consider q being Polynomial of n,L such that
A32: q = x2 & q.{} = f.x2 by A5;
consider a1 being Element of L such that
A33: p = {EmptyBag n} --> a1 by Lm1;
consider a2 being Element of L such that
A34: q = {EmptyBag n} --> a2 by Lm1;
EmptyBag n in {EmptyBag n} by TARSKI:def 1;
then A35: p.(EmptyBag n) = a1 & q.(EmptyBag n) = a2 by A33,A34,FUNCOP_1:13;
p.{} = p.(EmptyBag n) & q.{} = q.(EmptyBag n) by A1;
hence thesis by A30,A31,A32,A33,A34,A35;
end;
then f is one-to-one by FUNCT_1:def 8;
then A36: f is RingMonomorphism by A29,QUOFIELD:def 23;
rng f c= the carrier of L by RELSET_1:12;
then A37: for u being set holds u in rng f implies u in the carrier of L;
for u being set holds u in the carrier of L implies u in rng f
proof
let u be set;
assume u in the carrier of L;
then reconsider u as Element of L;
set p = EmptyBag n .--> u;
reconsider p as Function;
dom p = {EmptyBag n} & rng p = {u} by CQC_LANG:5;
then dom p = Bags n & rng p c= the carrier of L by POLYNOM1:55,TARSKI:def 1;
then reconsider p as Function of Bags n, the carrier of L by FUNCT_2:4;
reconsider p as Function of Bags n, L ;
reconsider p as Series of n, L ;
now per cases;
case A38: u = 0.L;
Support p = {}
proof
assume A39: Support p <> {};
consider v being Element of Support p;
A40: v in Support p by A39;
then v is bag of n by POLYNOM1:def 14;
then p.v = p.(EmptyBag n) by A1,A2 .= u by CQC_LANG:6;
hence thesis by A38,A40,POLYNOM1:def 9;
end;
hence Support p is finite;
case A41: u <> 0.L;
A42: for v being set holds v in Support p implies v in {EmptyBag n}
proof
let v be set;
assume v in Support p;
then reconsider v as bag of n by POLYNOM1:def 14;
v = EmptyBag n by A1,A2;
hence thesis by TARSKI:def 1;
end;
for v being set holds v in {EmptyBag n} implies v in Support p
proof
let v be set;
assume A43: v in {EmptyBag n};
then reconsider v as Element of Bags n by TARSKI:def 1;
p.v = p.(EmptyBag n) by A43,TARSKI:def 1 .= u by CQC_LANG:6;
hence thesis by A41,POLYNOM1:def 9;
end;
hence Support p is finite by A42,TARSKI:2;
end;
then reconsider p as Polynomial of n,L by POLYNOM1:def 10;
reconsider p' = p as Element of PL by POLYNOM1:def 27;
consider q being Polynomial of n,L such that
A44: q = p' & q.{} = f.p' by A5;
q.{} = p.(EmptyBag n) by A1,A44
.= u by CQC_LANG:6;
hence thesis by A6,A44,FUNCT_1:12;
end;
then rng f = the carrier of L by A37,TARSKI:2;
then f is RingEpimorphism by A29,QUOFIELD:def 22;
then f is RingIsomorphism by A36,QUOFIELD:def 24;
hence thesis by QUOFIELD:def 26;
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 :Def4:
ex b being bag of X
st for b' being bag of X st b' <> b holds p.b' = 0.L;
end;
definition
let X be set,
L be non empty ZeroStr;
cluster monomial-like Series of X,L;
existence
proof
set p = 0_(X,L);
take p;
for b' being bag of X st b' <> EmptyBag X holds p.b' = 0.L by POLYNOM1:81;
hence thesis by Def4;
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;
definition
let X be set,
L be non empty ZeroStr;
cluster monomial-like -> finite-Support 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 b' being bag of X st b' <> b holds s.b' = 0.L by Def4;
per cases;
suppose A2: s.b = 0.L;
now assume Support s <> {};
then reconsider sp = Support s as non empty Subset of Bags X;
consider c being Element of sp;
c in Support s;
then s.c <> 0.L by POLYNOM1:def 9;
hence contradiction by A1,A2;
end;
hence thesis by POLYNOM1:def 10;
suppose A3: s.b <> 0.L;
A4: now let u be set;
assume u in {b};
then A5: u = b by TARSKI:def 1;
then reconsider u' = u as Element of Bags X by POLYNOM1:def 14;
u' in Support s by A3,A5,POLYNOM1:def 9;
hence u in Support s;
end;
now let u be set;
assume A6: u in Support s;
then reconsider u' = u as Element of Bags X;
s.u' <> 0.L by A6,POLYNOM1:def 9;
then u' = b by A1;
hence u in {b} by TARSKI:def 1;
end;
then Support s = {b} by A4,TARSKI:2;
hence thesis by POLYNOM1:def 10;
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 A2: Support p = {};
consider b being bag of n;
for b' being bag of n st b' <> b holds p.b' = 0.L
proof
let b' be bag of n;
assume b' <> b;
assume A3: p.b' <> 0.L;
reconsider c = b' as Element of Bags n by POLYNOM1:def 14;
c in Support p by A3,POLYNOM1:def 9;
hence thesis by A2;
end;
hence p is Monomial of n,L by Def4;
end;
A4: now assume ex b being bag of n st Support p = {b};
then consider b being bag of n such that
A5: Support p = {b};
for b' being bag of n st b' <> b holds p.b' = 0.L
proof
let b' be bag of n;
assume A6: b' <> b;
assume A7: p.b' <> 0.L;
reconsider b' as Element of Bags n by POLYNOM1:def 14;
b' in Support p by A7,POLYNOM1:def 9;
hence thesis by A5,A6,TARSKI:def 1;
end;
hence p is Monomial of n,L by Def4;
end;
now assume p is Monomial of n,L;
then consider b being bag of n such that
A8: for b' being bag of n st b' <> b holds p.b' = 0.L by Def4;
now per cases;
case A9: p.b <> 0.L;
A10: for u being set holds u in Support p implies u in {b}
proof
let u be set;
assume A11: u in Support p;
then A12: p.u <> 0.L by POLYNOM1:def 9;
reconsider u' = u as bag of n by A11,POLYNOM1:def 14;
u' = b by A8,A12;
hence thesis by TARSKI:def 1;
end;
for u being set holds u in {b} implies u in Support p
proof
let u be set;
assume A13: u in {b};
then u = b by TARSKI:def 1;
then reconsider u' = u as Element of Bags n by POLYNOM1:def 14;
p.u' <> 0.L by A9,A13,TARSKI:def 1;
hence thesis by POLYNOM1:def 9;
end;
then Support p = {b} by A10,TARSKI:2;
hence ex b being bag of n st Support p = {b};
case A14: p.b = 0.L;
thus Support p = {}
proof
assume Support p <> {};
then reconsider sp = Support p as non empty Subset of Bags n;
consider c being Element of sp;
c in Support p;
then p.c <> 0.L by POLYNOM1:def 9;
hence thesis by A8,A14;
end;
end;
hence Support p = {} or ex b being bag of n st Support p = {b};
end;
hence thesis by A1,A4;
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 :Def5:
0_(X,L)+*(b,a);
coherence
proof
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 ;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
A2: b in Bags X by POLYNOM1:def 14;
then A3: m = 0_(X,L)+*(b .--> a) by A1,FUNCT_7:def 3;
dom(b .--> a) = {b} by CQC_LANG:5;
then A4: b in dom(b .--> a) by TARSKI:def 1;
A5: m.b = (0_(X,L)+*(b .--> a)).b by A1,A2,FUNCT_7:def 3
.= (b .--> a).b by A4,FUNCT_4:14
.= a by CQC_LANG:6;
now per cases;
case a <> 0.L;
then b in Support m by A2,A5,POLYNOM1:def 9;
then A6: for u being set holds u in {b} implies u in Support m by TARSKI:def 1
;
for u being set holds u in Support m implies u in {b}
proof
let u be set;
assume A7: u in Support m;
assume not(u in {b});
then A8: not(u in dom(b .--> a)) by CQC_LANG:5;
reconsider u as bag of X by A7,POLYNOM1:def 14;
m.u = (0_(X,L)).u by A3,A8,FUNCT_4:12
.= 0.L by POLYNOM1:81;
hence thesis by A7,POLYNOM1:def 9;
end;
then Support m = {b} by A6,TARSKI:2;
hence thesis by Th6;
case A9: a = 0.L;
now assume Support m <> {};
then reconsider sm = Support m as non empty Subset of Bags X;
consider c being Element of sm;
A10: c in Support m;
then m.c <> 0.L by POLYNOM1:def 9;
then not(c in {b}) by A5,A9,TARSKI:def 1;
then A11: not(c in dom(b .--> a)) by CQC_LANG:5;
reconsider c as bag of X;
m.c = (0_(X,L)).c by A3,A11,FUNCT_4:12
.= 0.L by POLYNOM1:81;
hence contradiction by A10,POLYNOM1:def 9;
end;
hence thesis by Th6;
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 :Def6:
m.it <> 0.L or (Support m = {} & it = EmptyBag X);
existence
proof
consider b being bag of X such that
A1: for b' being bag of X st b' <> b holds m.b' = 0.L by Def4;
now per cases;
case m.b <> 0.L;
hence thesis;
case A2: m.b = 0.L;
Support m = {}
proof
assume Support m <> {};
then reconsider sm = Support m as non empty Subset of Bags X;
consider c being Element of sm;
c in Support m;
then m.c <> 0.L by POLYNOM1:def 9;
hence thesis by A1,A2;
end;
hence thesis;
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);
assume A4: m.b2 <> 0.L or (Support m = {} & b2 = EmptyBag X);
consider b being bag of X such that
A5: for b' being bag of X st b' <> b holds m.b' = 0.L by Def4;
now per cases;
case A6: m.b1 <> 0.L;
reconsider b1' = b1 as Element of Bags X by POLYNOM1:def 14;
A7: b1' in Support m by A6,POLYNOM1:def 9;
thus b1 = b by A5,A6 .= b2 by A4,A5,A7;
case A8: m.b1 = 0.L;
now per cases by A4;
case A9: m.b2 <> 0.L;
reconsider b2' = b2 as Element of Bags X by POLYNOM1:def 14;
b2' in Support m by A9,POLYNOM1:def 9;
hence b1 = b2 by A3,A8;
case Support m = {} & b2 = EmptyBag X;
hence b1 = b2 by A3,A8;
end;
hence b1 = b2;
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 :Def7:
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;
assume A1: Support(m) <> {};
then consider b being bag of X such that
A2: Support(m) = {b} by Th6;
A3: m.term(m) <> 0.L by A1,Def6;
term(m) is Element of Bags X by POLYNOM1:def 14;
then term(m) in Support(m) by A3,POLYNOM1:def 9;
hence thesis by A2,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;
A1: Monom(0.L,b) = 0_(n,L)+*(b,0.L) by Def5;
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 ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
then A4: m = 0_(n,L)+*(b .--> 0.L) by A2,FUNCT_7:def 3;
A5: dom(b .--> 0.L) = {b} by CQC_LANG:5;
then A6: b in dom(b .--> 0.L) by TARSKI:def 1;
A7: m.b = (0_(n,L)+*(b .--> 0.L)).b by A2,A3,FUNCT_7:def 3
.= (b .--> 0.L).b by A6,FUNCT_4:14
.= 0.L by CQC_LANG:6;
A8: now let b' be bag of n;
now per cases;
case b' = b;
hence m.b' = 0.L by A7;
case b' <> b;
then not(b' in dom(b .--> 0.L)) by A5,TARSKI:def 1;
hence m.b' = (0_(n,L)).b' by A4,FUNCT_4:12 .= 0.L by POLYNOM1:81;
end;
hence m.b' = 0.L;
end;
thus coefficient(Monom(0.L,b)) = (Monom(0.L,b)).(term(Monom(0.L,b))) by Def7
.= 0.L by A1,A8;
(Monom(0.L,b)).(term(Monom(0.L,b))) = 0.L by A1,A8;
hence thesis by Def6;
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;
A1: Monom(a,b) = 0_(n,L)+*(b,a) by Def5;
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 ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
dom(b .--> a) = {b} by CQC_LANG:5;
then A4: b in dom(b .--> a) by TARSKI:def 1;
A5: m.b = (0_(n,L)+*(b .--> a)).b by A2,A3,FUNCT_7:def 3
.= (b .--> a).b by A4,FUNCT_4:14
.= a by CQC_LANG:6;
per cases;
suppose A6: m.b <> 0.L;
thus coefficient(Monom(a,b)) = Monom(a,b).(term(Monom(a,b))) by Def7
.= a by A1,A5,A6,Def6;
suppose m.b = 0.L;
hence thesis by A5,Th8;
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;
A1: Monom(a,b) = 0_(n,L)+*(b,a) by Def5;
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 ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
dom(b .--> a) = {b} by CQC_LANG:5;
then A4: b in dom(b .--> a) by TARSKI:def 1;
m.b = (0_(n,L)+*(b .--> a)).b by A2,A3,FUNCT_7:def 3
.= (b .--> a).b by A4,FUNCT_4:14
.= a by CQC_LANG:6;
then m.b <> 0.L by RLVECT_1:def 13;
hence term(Monom(a,b)) = b by A1,Def6;
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;
A1: dom m = Bags X & dom Monom(coefficient(m),term(m)) = Bags X
by FUNCT_2:def 1;
per cases by Th6;
suppose A2: Support m = {};
then A3: term(m) = EmptyBag X by Def6;
A4: m = 0_(X,L) by A2,Th1;
set m' = Monom(coefficient(m),term(m));
A5: now assume coefficient(m) <> 0.L;
then A6: m.(term(m)) <> 0.L by Def7;
term(m) is Element of Bags X by POLYNOM1:def 14;
hence contradiction by A2,A6,POLYNOM1:def 9;
end;
then A7: Monom(coefficient(m),term(m)) = 0_(X,L)+*(EmptyBag X,0.L)
by A3,Def5;
A8: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
A9: dom(EmptyBag X .--> 0.L) = {EmptyBag X} by CQC_LANG:5;
then A10: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
A11: m'.EmptyBag X
= (0_(X,L)+*(EmptyBag X .--> 0.L)).EmptyBag X by A7,A8,FUNCT_7:def 3
.= (EmptyBag X .--> 0.L).EmptyBag X by A10,FUNCT_4:14
.= 0.L by CQC_LANG:6;
now let x be set;
assume x in Bags X;
then reconsider x'= x as Element of Bags X;
now per cases;
case x' = EmptyBag X;
hence m'.x' = 0.L by A11;
case x <> EmptyBag X;
then A12: not(x' in dom(EmptyBag X .--> 0.L)) by A9,TARSKI:def 1;
m'.x' = (0_(X,L)+*(EmptyBag X,0.L)).x' by A3,A5,Def5
.= (0_(X,L)+*(EmptyBag X .--> 0.L)).x' by A8,FUNCT_7:def 3
.= 0_(X,L).x' by A12,FUNCT_4:12;
hence m'.x' = 0.L by POLYNOM1:81;
end;
hence m.x = m'.x by A4,POLYNOM1:81;
end;
hence thesis by A1,FUNCT_1:9;
suppose ex b being bag of X st Support m = {b};
then consider b being bag of X such that
A13: Support m = {b};
set a = m.b;
A14: b in Support m by A13,TARSKI:def 1;
then a <> 0.L by POLYNOM1:def 9;
then A15: term(m) = b by Def6;
then A16: coefficient(m) = a by Def7;
then A17: Monom(coefficient(m),term(m)) = 0_(X,L)+*(b,a) by A15,Def5;
set m' = Monom(coefficient(m),term(m));
A18: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
A19: b in Bags X by POLYNOM1:def 14;
dom(b .--> a) = {b} by CQC_LANG:5;
then A20: b in dom(b .--> a) by TARSKI:def 1;
A21: m'.b = (0_(X,L)+*(b .--> a)).b by A17,A18,A19,FUNCT_7:def 3
.= (b .--> a).b by A20,FUNCT_4:14
.= a by CQC_LANG:6;
A22: now let u be set;
assume u in {b};
then A23: u = b by TARSKI:def 1;
m'.b <> 0.L & b is Element of Bags X by A14,A21,POLYNOM1:def 9;
hence u in Support(Monom(coefficient(m),term(m))) by A23,POLYNOM1:def 9;
end;
now let u be set;
assume A24: u in Support(Monom(coefficient(m),term(m)));
then reconsider u' = u as Element of Bags X;
now assume A25: u <> b;
A26: b in dom 0_(X,L) by A18,POLYNOM1:def 14;
dom(b .--> a) = {b} by CQC_LANG:5;
then A27: not(u' in dom(b .--> a)) by A25,TARSKI:def 1;
m'.u' = (0_(X,L)+*(b,a)).u' by A15,A16,Def5
.= (0_(X,L)+*(b .--> a)).u' by A26,FUNCT_7:def 3
.= 0_(X,L).u' by A27,FUNCT_4:12;
hence m'.u' = 0.L by POLYNOM1:81;
end;
hence u in {b} by A24,POLYNOM1:def 9,TARSKI:def 1;
end;
then A28: Support(Monom(coefficient(m),term(m))) = {b} by A22,TARSKI:2;
now let x be set;
assume x in Bags X;
then reconsider x' = x as Element of Bags X;
now per cases;
case x = b;
hence Monom(coefficient(m),term(m)).x' = m.x' by A21;
case A29: x <> b;
then A30: not(x in Support m) by A13,TARSKI:def 1;
A31: not(x in Support(Monom(coefficient(m),term(m))))
by A28,A29,TARSKI:def 1;
thus m.x' = 0.L by A30,POLYNOM1:def 9
.= Monom(coefficient(m),term(m)).x' by A31,POLYNOM1:def 9;
end;
hence m.x = Monom(coefficient(m),term(m)).x;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem Th12:
for n being Ordinal,
L being right_zeroed add-associative right_complementable
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
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) &
eval(m,x) = Sum y &
for i being 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
A2: for b' being bag of n st b' <> b holds m.b' = 0.L by Def4;
now per cases;
case A3: m.b <> 0.L;
A4: for u being set holds u in Support m implies u in {b}
proof
let u be set;
assume A5: u in Support m;
assume A6: not(u in {b});
reconsider u as Element of Bags n by A5;
u <> b by A6,TARSKI:def 1;
then m.u = 0.L by A2;
hence thesis by A5,POLYNOM1:def 9;
end;
for u being set holds u in {b} implies u in Support m
proof
let u be set;
assume A7: u in {b};
then u = b by TARSKI:def 1;
then reconsider u as Element of Bags n by POLYNOM1:def 14;
m.u <> 0.L by A3,A7,TARSKI:def 1;
hence thesis by POLYNOM1:def 9;
end;
then A8: Support m = {b} by A4,TARSKI:2;
reconsider sm = Support m as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sm);
A9: BagOrder n linearly_orders sm by POLYNOM2:20;
then A10: rng sg = {b} &
for l,m being Nat st l in dom sg & m in dom sg & l < m
holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n) by A8,TRIANG_1:def 2;
then b in rng sg by TARSKI:def 1;
then A11: 1 in dom sg by FINSEQ_3:33;
then A12: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
for u being set holds u in dom sg implies u in {1}
proof
let u be set;
assume A13: u in dom sg;
assume A14: not(u in {1});
reconsider u as Nat by A13;
A15: u <> 1 by A14,TARSKI:def 1;
A16: 1 < u
proof
consider k being Nat such that A17: 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 consider m' being Nat such that
A18: m' = u & 1 <= m' & m' <= k by A13,A17;
thus thesis by A15,A18,REAL_1:def 5;
end;
sg/.1 = sg.1 & sg/.u = sg.u by A11,A13,FINSEQ_4:def 4;
then A19: sg/.1 in rng sg & sg/.u in rng sg by A11,A13,FUNCT_1:12;
then sg/.1 = b by A10,TARSKI:def 1
.= sg/.u by A10,A19,TARSKI:def 1;
hence thesis by A9,A11,A13,A16,TRIANG_1:def 2;
end;
then A20: dom sg = Seg 1 by A12,FINSEQ_1:4,TARSKI:2;
then A21: len sg = 1 by FINSEQ_1:def 3;
A22: 1 in dom sg by A20,FINSEQ_1:4,TARSKI:def 1;
sg/.1 = sg.1 by A11,FINSEQ_4:def 4;
then sg/.1 in rng sg by A22,FUNCT_1:12;
then A23: sg/.1 = b by A10,TARSKI:def 1;
A24: sg.1 in rng sg by A11,FUNCT_1:12;
then A25: sg.1 = b by A10,TARSKI:def 1;
A26: b in Bags n by POLYNOM1:def 14;
dom m = Bags n by FUNCT_2:def 1;
then 1 in dom (m * sg) by A11,A25,A26,FUNCT_1:21;
then A27: (m * sg)/.1 = (m * sg).1 by FINSEQ_4:def 4
.= m.(sg.1) by A11,FUNCT_1:23
.= m.b by A10,A24,TARSKI:def 1
.= m.(term(m)) by A3,Def6
.= coefficient(m) by Def7;
dom y = Seg(len y) by FINSEQ_1:def 3
.= dom sg by A1,FINSEQ_1:def 3;
then y.1 = y/.1 by A22,FINSEQ_4:def 4
.= (m * sg)/.1 * eval((sg/.1)@,x) by A1,A21
.= (m * sg)/.1 * eval(b,x) by A23,POLYNOM2:def 3;
then y = <* coefficient(m) * eval(b,x) *>
by A1,A21,A27,FINSEQ_1:57;
hence eval(m,x) = coefficient(m) * eval(b,x) by A1,RLVECT_1:61
.= coefficient(m) * eval(term(m),x) by A3,Def6;
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;
consider c being Element of sm;
c in Support m;
then m.c <> 0.L by POLYNOM1:def 9;
hence thesis by A2,A28;
end;
then A30: term(m) = EmptyBag n by Def6;
m.(EmptyBag n) = 0.L by A29,POLYNOM1:def 9;
then A31: coefficient(m) * eval(term(m),x) = 0.L * eval(term(m),x) by A30,Def7
.= 0.L by VECTSP_1:39;
consider y being FinSequence of the carrier of L such that
A32: len y = len SgmX(BagOrder n, Support m) &
eval(m,x) = Sum y &
for i being 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:20;
then rng SgmX(BagOrder n, Support m) = {} by A29,TRIANG_1:def 2;
then SgmX(BagOrder n, Support m) = {} by FINSEQ_1:27;
then len y = 0 by A32,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
hence eval(m,x) = coefficient(m) * eval(term(m),x) by A31,A32,RLVECT_1:60;
end;
hence thesis;
end;
theorem
for n being Ordinal,
L being right_zeroed add-associative right_complementable
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
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 by RLVECT_1:def 13;
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;
case A2: a = 0.L;
for b' being bag of n holds m.b' = 0.L
proof
let b' be bag of n;
now per cases;
case A3: b' = b;
A4: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19;
A5: b in Bags n by POLYNOM1:def 14;
A6: m = 0_(n,L)+*(b,a) by Def5
.= 0_(n,L)+*(b .--> a) by A4,A5,FUNCT_7:def 3;
dom(b .--> a) = {b} by CQC_LANG:5;
then b in dom(b .--> a) by TARSKI:def 1;
hence m.b' = (b .--> a).b by A3,A6,FUNCT_4:14
.= 0.L by A2,CQC_LANG:6;
case A7: b' <> b;
thus m.b' = 0_(n,L)+*(b,a).b' by Def5
.= 0_(n,L).b' by A7,FUNCT_7:34
.= 0.L by POLYNOM1:81;
end;
hence thesis;
end;
then A8: m.(term(m)) = 0.L;
thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12
.= m.(term(m)) * eval(term(m),x) by Def7
.= 0.L by A8,VECTSP_1:39
.= a * eval(b,x) by A2,VECTSP_1:39;
end;
hence thesis;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Constant Polynomials
begin
definition
let X be set,
L be non empty ZeroStr,
p be Series of X,L;
attr p is Constant means :Def8:
for b being bag of X st b <> EmptyBag X holds p.b = 0.L;
end;
definition
let X be set,
L be non empty ZeroStr;
cluster Constant 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:81;
hence thesis by Def8;
end;
end;
definition
let X be set,
L be non empty ZeroStr;
mode ConstPoly of X,L is Constant Series of X,L;
end;
definition
let X be set,
L be non empty ZeroStr;
cluster Constant -> monomial-like Series of X,L;
coherence
proof
let p be Series of X,L;
assume p is Constant;
then for b being bag of X st b <> EmptyBag X holds p.b = 0.L by Def8;
hence thesis by Def4;
end;
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 set holds u in Support p implies u in {EmptyBag n}
proof
let u be set;
assume A4: u in Support p;
then reconsider u as Element of Bags n;
reconsider u' = u as bag of n;
p.u' <> 0.L by A4,POLYNOM1:def 9;
then u' = EmptyBag n by A2,Def8;
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 set 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
assume A8: Support p <> {};
consider v being Element of Support p;
A9: v in Support p by A8;
v in {EmptyBag n} by A3,A8;
hence thesis by A6,A9,TARSKI:def 1;
end;
A10: for b being bag of n holds p.b = 0.L
proof
let b be bag of n;
assume A11: p.b <> 0.L;
b is Element of Bags n by POLYNOM1:def 14;
hence thesis by A7,A11,POLYNOM1:def 9;
end;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being set holds u in rng p implies u in {0.L}
proof
let u be set;
assume u in rng p;
then consider x being set such that
A14: x in dom p & p.x = u by FUNCT_1:def 5;
x is bag of n by A14,POLYNOM1:def 14;
then u = 0.L by A10,A14;
hence thesis by TARSKI:def 1;
end;
for u being set holds u in {0.L} implies u in rng p
proof
let u be set;
assume u in {0.L};
then A15: u = 0.L by TARSKI:def 1;
consider b being bag of n;
A16: p.b = u by A10,A15;
b in dom p by A12,POLYNOM1:def 14;
hence thesis by A16,FUNCT_1:def 5;
end;
then rng p = {0.L} by A13,TARSKI:2;
then p = (Bags n) --> 0.L by A12,FUNCOP_1:15;
hence p = 0_(n,L) by POLYNOM1:def 24;
end;
end;
now assume A17: p = 0_(n,L) or Support p = {EmptyBag n};
per cases by A17;
suppose p = 0_(n,L);
then for b being bag of n st b <> EmptyBag n holds p.b = 0.L by POLYNOM1:81
;
hence p is ConstPoly of n,L by Def8;
suppose A18: 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 A19: b <> EmptyBag n;
reconsider b as Element of Bags n by POLYNOM1:def 14;
not(b in Support p) by A18,A19,TARSKI:def 1;
hence thesis by POLYNOM1:def 9;
end;
hence p is ConstPoly of n,L by Def8;
end;
hence thesis by A1;
end;
definition
let X be set,
L be non empty ZeroStr;
cluster 0_(X,L) -> Constant;
coherence
proof
for b being bag of X st b <> EmptyBag X holds (0_(X,L)).b = 0.L
by POLYNOM1:81;
hence thesis by Def8;
end;
end;
definition
let X be set,
L be unital (non empty doubleLoopStr);
cluster 1_(X,L) -> Constant;
coherence
proof
for b being bag of X st b <> EmptyBag X holds (1_(X,L)).b = 0.L
by POLYNOM1:84;
hence thesis by Def8;
end;
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 Def6;
case A2: c.eb = 0.L;
Support c = {}
proof
assume A3: Support c <> {};
consider u being Element of Support c;
u in Support c by A3;
then reconsider u as Element of Bags n;
c.u <> 0.L by A3,POLYNOM1:def 9;
hence thesis by A2,Def8;
end;
hence term(c) = EmptyBag n by Def6;
end;
hence term(c) = EmptyBag n;
thus coefficient(c) = c.(EmptyBag n) by A1,Def7;
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 :Def9:
0_(X,L)+*(EmptyBag X,a);
coherence;
end;
definition
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 O' = O as Function of Bags X,L;
reconsider O' as Series of X,L;
A1: O = a _(X,L) by Def9;
now let b be bag of X;
assume A2: b <> EmptyBag X;
dom(Z) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
then A3: O' = 0_(X,L)+*(EmptyBag X .--> a) by FUNCT_7:def 3;
dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
then not(b in dom(EmptyBag X .--> a)) by A2,TARSKI:def 1;
hence (O').b = (0_(X,L)).b by A3,FUNCT_4:12 .= 0.L by POLYNOM1:81;
end;
hence thesis by A1,Def8;
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);
A1: Bags X = dom o1 by FUNCT_2:def 1;
A2: Bags X = dom o2 by FUNCT_2:def 1;
now let x be set;
assume x in Bags X;
then reconsider x' = x as bag of X by POLYNOM1:def 14;
A3: o2.x' = 0.L by POLYNOM1:81;
set m = 0_(X,L)+*(EmptyBag X,0.L);
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 ;
A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
then A5: m = 0_(X,L)+*(EmptyBag X .--> 0.L) by FUNCT_7:def 3;
A6: dom(EmptyBag X .--> 0.L) = {EmptyBag X} by CQC_LANG:5;
then A7: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
A8: m.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> 0.L)).(EmptyBag X) by A4,FUNCT_7:def 3
.= (EmptyBag X .--> 0.L).(EmptyBag X) by A7,FUNCT_4:14
.= 0.L by CQC_LANG:6;
per cases;
suppose x' = EmptyBag X;
hence o1.x = o2.x by A3,A8,Def9;
suppose x' <> EmptyBag X;
then not(x' in dom(EmptyBag X .--> 0.L)) by A6,TARSKI:def 1;
then m.x' = (0_(X,L)).x' by A5,FUNCT_4:12;
hence o1.x = o2.x by Def9;
end;
hence thesis by A1,A2,FUNCT_1:9;
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);
case A2: Support p = {EmptyBag X};
set q = 0_(X,L)+*(EmptyBag X,p.(EmptyBag X));
A3: q = p.(EmptyBag X) _(X,L) by Def9;
A4: Bags X = dom p by FUNCT_2:def 1;
A5: Bags X = dom q by FUNCT_2:def 1;
now let x be set;
assume x in Bags X;
then reconsider x' = x as bag of X by POLYNOM1:def 14;
A6: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
then A7: q = 0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X)) by FUNCT_7:def 3;
A8: dom(EmptyBag X .--> p.(EmptyBag X)) = {EmptyBag X} by CQC_LANG:5;
then A9: EmptyBag X in dom(EmptyBag X .--> p.(EmptyBag X))
by TARSKI:def 1;
A10: q.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X))).(EmptyBag X)
by A6,FUNCT_7:def 3
.= (EmptyBag X .--> p.(EmptyBag X)).(EmptyBag X)
by A9,FUNCT_4:14
.= p.(EmptyBag X) by CQC_LANG:6;
now per cases;
case x' = EmptyBag X;
hence p.x = q.x by A10;
case A11: x' <> EmptyBag X;
then not(x' in dom(EmptyBag X .--> p.(EmptyBag X)))
by A8,TARSKI:def 1;
then A12: q.x' = (0_(X,L)).x' by A7,FUNCT_4:12;
A13: not(x' in Support p) by A2,A11,TARSKI:def 1;
x' is Element of Bags X by POLYNOM1:def 14;
then p.x' = 0.L by A13,POLYNOM1:def 9;
hence p.x = q.x by A12,POLYNOM1:81;
end;
hence p.x = q.x;
end;
then p = q by A4,A5,FUNCT_1:9;
hence ex a being Element of L st p = a _(X,L) by A3;
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 24;
then A2: dom Z = Bags n by FUNCOP_1:19;
A3: Z+*(EmptyBag n,a) = a _(n,L) by Def9;
hence (a _(n,L)).EmptyBag n = a by A2,FUNCT_7:33;
let b be bag of n;
assume A4: b <> EmptyBag n;
A5: b in Bags n by POLYNOM1:def 14;
thus (a _(n,L)).b = Z.b by A3,A4,FUNCT_7:34 .= 0.L by A1,A5,FUNCOP_1:13;
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 unital (non empty multLoopStr_0)
holds 1.L _(X,L) = 1_(X,L)
proof
let X be set,
L be unital (non empty multLoopStr_0);
set o1 = 1.L _(X,L), o2 = 1_(X,L);
A1: Bags X = dom o1 by FUNCT_2:def 1;
A2: Bags X = dom o2 by FUNCT_2:def 1;
now let x be set;
assume x in Bags X;
then reconsider x' = x as bag of X by POLYNOM1:def 14;
set m = 0_(X,L)+*(EmptyBag X,1.L);
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 ;
A3: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
then A4: m = 0_(X,L)+*(EmptyBag X .--> 1.L) by FUNCT_7:def 3;
A5: dom(EmptyBag X .--> 1.L) = {EmptyBag X} by CQC_LANG:5;
then A6: EmptyBag X in dom(EmptyBag X .--> 1.L) by TARSKI:def 1;
A7: m.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> 1.L)).(EmptyBag X) by A3,FUNCT_7:def 3
.= (EmptyBag X .--> 1.L).(EmptyBag X) by A6,FUNCT_4:14
.= 1.L by CQC_LANG:6;
per cases;
suppose A8: x' = EmptyBag X;
hence o1.x = 1.L by A7,Def9 .= o2.x by A8,POLYNOM1:84;
suppose A9: x' <> EmptyBag X;
then not(x' in dom(EmptyBag X .--> 1.L)) by A5,TARSKI:def 1;
then m.x' = (0_(X,L)).x' by A4,FUNCT_4:12
.= 0.L by POLYNOM1:81
.= o2.x' by A9,POLYNOM1:84;
hence o1.x = o2.x by Def9;
end;
hence thesis by A1,A2,FUNCT_1:9;
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 ;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
then A2: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
A3: m.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by A1,FUNCT_7:def 3
.= (EmptyBag X .--> a).(EmptyBag X) by A2,FUNCT_4:14
.= a by CQC_LANG:6;
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 ;
A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
dom(EmptyBag X .--> b) = {EmptyBag X} by CQC_LANG:5;
then A5: EmptyBag X in dom(EmptyBag X .--> b) by TARSKI:def 1;
A6: k.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> b)).(EmptyBag X) by A4,FUNCT_7:def 3
.= (EmptyBag X .--> b).(EmptyBag X) by A5,FUNCT_4:14
.= b by CQC_LANG:6;
m = a _(X,L) & k = b _(X,L) by Def9;
hence thesis by A3,A6;
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: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19;
dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
then A2: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
A3: m.(EmptyBag X)
= (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by A1,FUNCT_7:def 3
.= (EmptyBag X .--> a).(EmptyBag X) by A2,FUNCT_4:14
.= a by CQC_LANG:6;
coefficient(a _(X,L)) = (a _(X,L)).(EmptyBag X) by Lm2
.= a by A3,Def9;
hence thesis by Lm2;
end;
theorem Th24:
for n being Ordinal,
L being right_zeroed add-associative right_complementable
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
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) &
eval(c,x) = Sum y &
for i being 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 A2: coefficient(c) = 0.L;
Support c = {}
proof
assume A3: Support c <> {};
consider u being Element of Support c;
u in Support c by A3;
then reconsider u as Element of Bags n;
c.u <> 0.L by A3,POLYNOM1:def 9;
then u <> EmptyBag n by A2,Lm2;
then c.u = 0.L by Def8;
hence thesis by A3,POLYNOM1:def 9;
end;
then reconsider Sc = Support c as empty Subset of Bags n;
BagOrder n linearly_orders Sc by POLYNOM2:20;
then SgmX(BagOrder n, Sc) = {} by POLYNOM2:9;
then len y = 0 by A1,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
hence eval(c,x) = coefficient(c) by A1,A2,RLVECT_1:60;
case A4: coefficient(c) <> 0.L;
A5: for u being set holds u in Support c implies u in {EmptyBag n}
proof
let u be set;
assume A6: u in Support c;
assume A7: not(u in {EmptyBag n});
reconsider u as Element of Bags n by A6;
u <> EmptyBag n by A7,TARSKI:def 1;
then c.u = 0.L by Def8;
hence thesis by A6,POLYNOM1:def 9;
end;
for u being set holds u in {EmptyBag n} implies u in Support c
proof
let u be set;
assume A8: u in {EmptyBag n};
then A9: u = EmptyBag n by TARSKI:def 1;
reconsider u as Element of Bags n by A8,TARSKI:def 1;
c.u <> 0.L by A4,A9,Lm2;
hence thesis by POLYNOM1:def 9;
end;
then A10: Support c = {EmptyBag n} by A5,TARSKI:2;
reconsider sc = Support c as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sc);
A11: BagOrder n linearly_orders sc by POLYNOM2:20;
then A12: rng sg = {EmptyBag n} &
for l,m being Nat st l in dom sg & m in dom sg & l < m
holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n) by A10,TRIANG_1:def 2;
then EmptyBag n in rng sg by TARSKI:def 1;
then A13: 1 in dom sg by FINSEQ_3:33;
then A14: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
for u being set holds u in dom sg implies u in {1}
proof
let u be set;
assume A15: u in dom sg;
assume A16: not(u in {1});
reconsider u as Nat by A15;
A17: u <> 1 by A16,TARSKI:def 1;
A18: 1 < u
proof
consider k being Nat such that A19: 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 consider m' being Nat such that
A20: m' = u & 1 <= m' & m' <= k by A15,A19;
thus thesis by A17,A20,REAL_1:def 5;
end;
sg/.1 = sg.1 & sg/.u = sg.u by A13,A15,FINSEQ_4:def 4;
then A21: sg/.1 in rng sg & sg/.u in rng sg by A13,A15,FUNCT_1:12;
then sg/.1 = EmptyBag n by A12,TARSKI:def 1
.= sg/.u by A12,A21,TARSKI:def 1;
hence thesis by A11,A13,A15,A18,TRIANG_1:def 2;
end;
then A22: dom sg = Seg 1 by A14,FINSEQ_1:4,TARSKI:2;
then A23: len sg = 1 by FINSEQ_1:def 3;
A24: 1 in dom sg by A22,FINSEQ_1:4,TARSKI:def 1;
sg/.1 = sg.1 by A13,FINSEQ_4:def 4;
then sg/.1 in rng sg by A24,FUNCT_1:12;
then A25: sg/.1 = EmptyBag n by A12,TARSKI:def 1;
A26: sg.1 in rng sg by A13,FUNCT_1:12;
then A27: sg.1 = EmptyBag n by A12,TARSKI:def 1;
dom c = Bags n by FUNCT_2:def 1;
then 1 in dom (c * sg) by A13,A27,FUNCT_1:21;
then A28: (c * sg)/.1 = (c * sg).1 by FINSEQ_4:def 4
.= c.(sg.1) by A13,FUNCT_1:23
.= c.(EmptyBag n) by A12,A26,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 A24,FINSEQ_4:def 4
.= (c * sg)/.1 * eval((sg/.1)@,x) by A1,A23
.= coefficient(c) * eval(EmptyBag n,x) by A25,A28,POLYNOM2:def 3
.= coefficient(c) * 1. L by POLYNOM2:16
.= coefficient(c) by GROUP_1:def 4;
then y = <* coefficient(c) *> by A1,A23,FINSEQ_1:57;
hence eval(c,x) = coefficient(c) by A1,RLVECT_1:61;
end;
hence thesis;
end;
theorem Th25:
for n being Ordinal,
L being right_zeroed add-associative right_complementable
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
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;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Multiplication with Coefficients
begin
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 :Def10:
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 LambdaD;
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 POLYNOM1:def 14;
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 b' = b as bag of X;
thus p1.b = a * p.b' by A2 .= p2.b by A3;
end;
hence p1 = p2 by FUNCT_2:113;
end;
func p * a -> Series of X,L means :Def11:
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 LambdaD;
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 POLYNOM1:def 14;
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 b' = b as bag of X;
thus p1.b = p.b' * a by A5 .= p2.b by A6;
end;
hence p1 = p2 by FUNCT_2:113;
end;
end;
definition
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;
A1: Support p is finite by POLYNOM1:def 10;
now
now let u be set;
assume A2: u in Support ap;
then A3: ap.u <> 0.L by POLYNOM1:def 9;
reconsider u' = u as Element of Bags X by A2;
a * p.u' <> 0.L by A3,Def10;
then p.u' <> 0.L by BINOM:2;
hence u in Support p by POLYNOM1:def 9;
end;
then Support ap c= Support p by TARSKI:def 3;
then Support ap is finite by A1,FINSET_1:13;
hence thesis by POLYNOM1:def 10;
end;
hence thesis;
end;
cluster p * a -> finite-Support;
coherence
proof
set ap = p * a;
A4: Support p is finite by POLYNOM1:def 10;
now
let u be set;
assume A5: u in Support ap;
then A6: ap.u <> 0.L by POLYNOM1:def 9;
reconsider u' = u as Element of Bags X by A5;
p.u' * a <> 0.L by A6,Def11;
then p.u' <> 0.L by BINOM:1;
hence u in Support p by POLYNOM1:def 9;
end;
then Support ap c= Support p by TARSKI:def 3;
then Support ap is finite by A4,FINSET_1:13;
hence thesis by POLYNOM1:def 10;
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 b' = b as bag of n;
thus (a * p).b = a * p.b' by Def10
.= (p * a).b by Def11;
end;
hence a * p = p * a by FUNCT_2:113;
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;
A1: Bags n = dom(a * p) by FUNCT_2:def 1;
A2: Bags n = dom(a _(n,L) *' p) by FUNCT_2:def 1;
for x being set st x in Bags n holds (a * p).x = (a _(n,L) *' p).x
proof
let x be set;
assume x in Bags n;
then reconsider b = x as bag of n by POLYNOM1:def 14;
A3: b is Element of Bags n by POLYNOM1:def 14;
set O = a _(n,L), cL = the carrier of L;
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
A4: (O*'p).b = Sum s and
A5: len s = len decomp b and
A6: for k being 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 26;
A7: len s <> 0 by A5,FINSEQ_1:25;
then s is non empty by FINSEQ_1:25;
then consider s1 being Element of cL, t being FinSequence of cL such that
A8: s1 = s.1 and
A9: s = <*s1*>^t by FSM_1:5;
A10: Sum s = (Sum <*s1*>) + (Sum t) by A9,RLVECT_1:58;
s is non empty by A7,FINSEQ_1:25;
then A11: 1 in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A12: (decomp b)/.1 = <*b1, b2*> and
A13: s/.1 = O.b1*p.b2 by A6;
(decomp b)/.1 = <*EmptyBag n, b*> by POLYNOM1:75;
then A14: b2 = b & b1 = EmptyBag n by A12,GROUP_7:2;
A15: s/.1 = s.1 by A11,FINSEQ_4:def 4;
A16: Sum <*s1*> = s1 by RLVECT_1:61
.= a * p.b by A8,A13,A14,A15,Th18;
now per cases;
suppose t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:60;
suppose A17: t <> <*>(cL);
now let k be Nat;
assume A18: k in dom t;
then A19: t/.k = t.k by FINSEQ_4:def 4
.= s.(k+1) by A9,A18,FSM_1:6;
1 <= k by A18,FINSEQ_3:27;
then A20: 1 < k+1 by NAT_1:38;
A21: dom s = dom decomp b by A5,FINSEQ_3:31;
A22: len s = len t + len <*s1*> by A9,FINSEQ_1:35
.= len t +1 by FINSEQ_1:56;
k <= len t by A18,FINSEQ_3:27;
then A23: k+1 <= len s by A22,AXIOMS:24;
then A24: k+1 in dom decomp b by A5,A20,FINSEQ_3:27;
then A25: s/.(k+1) = s.(k+1) by A21,FINSEQ_4:def 4;
per cases by A23,AXIOMS:21;
suppose A26: k+1 < len s;
consider b1, b2 being bag of n such that
A27: (decomp b)/.(k+1) = <*b1, b2*> and
A28: s/.(k+1) = O.b1*p.b2 by A6,A21,A24;
b1 <> EmptyBag n by A5,A20,A26,A27,POLYNOM1:76;
hence t/.k = 0.L*p.b2 by A19,A25,A28,Th18
.= 0.L by VECTSP_1:39;
suppose A29: k+1 = len s;
consider b1, b2 being bag of n such that
A30: (decomp b)/.(k+1) = <*b1, b2*> and
A31: s/.(k+1) = O.b1*p.b2 by A6,A21,A24;
(decomp b)/.(len s) = <*b,EmptyBag n*> by A5,POLYNOM1:75;
then A32: b2 = EmptyBag n & b1 = b by A29,A30,GROUP_7:2;
now assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *>
by POLYNOM1:77;
then len t +1 = 0+1 by A5,A22,FINSEQ_1:56;
then len t = 0 by XCMPLX_1:2;
hence contradiction by A17,FINSEQ_1:25;
end;
then s.(k+1) = 0.L*(p.EmptyBag n) by A25,A31,A32,Th18
.= 0.L by VECTSP_1:39;
hence t/.k = 0.L by A19;
end;
hence Sum t = 0.L by MATRLIN:15;
end;
hence (O*'p).b = a * p.b by A4,A10,A16,RLVECT_1:10;
end;
then (O*'p).b = a * p.b by A3 .= (a * p).b by Def10;
hence (O*'p).x = (a * p).x;
end;
hence thesis by A1,A2,FUNCT_1:9;
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;
A1: Bags n = dom(p * a) by FUNCT_2:def 1;
A2: Bags n = dom(p *' (a _(n,L))) by FUNCT_2:def 1;
for x being set st x in Bags n holds (p * a).x = (p *' (a _(n,L))).x
proof
let x be set;
assume x in Bags n;
then reconsider b = x as bag of n by POLYNOM1:def 14;
A3: b is Element of Bags n by POLYNOM1:def 14;
set O = a _(n,L), cL = the carrier of L;
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
A4: (p*'O).b = Sum s and
A5: len s = len decomp b and
A6: for k being Nat st k in dom s
ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*>
& s/.k = (p.b1)*(O.b2) by POLYNOM1:def 26;
A7: len s <> 0 by A5,FINSEQ_1:25;
then consider t being FinSequence of cL,s1 being Element of cL such that
A8: s = t^<*s1*> by FINSEQ_2:22;
A9: Sum s = (Sum t) + (Sum <*s1*>) by A8,RLVECT_1:58;
s is non empty by A7,FINSEQ_1:25;
then A10: len s in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A11: (decomp b)/.len s = <*b1, b2*> and
A12: s/.len s = p.b1*O.b2 by A6;
(decomp b)/.len s = <*b,EmptyBag n*> by A5,POLYNOM1:75;
then A13: b1 = b & b2 = EmptyBag n by A11,GROUP_7:2;
A14: s/.len s = s.len s by A10,FINSEQ_4:def 4;
A15: s.len s = (t^<*s1*>).(len t +1) by A8,FINSEQ_2:19
.= s1 by FINSEQ_1:59;
A16: Sum <*s1*> = s1 by RLVECT_1:61
.= p.b * a by A12,A13,A14,A15,Th18;
now per cases;
suppose t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:60;
suppose A17: t <> <*>(cL);
now let k be Nat;
assume A18: k in dom t;
then A19: t/.k = t.k by FINSEQ_4:def 4
.= s.k by A8,A18,FINSEQ_1:def 7;
A20: 1 <= k by A18,FINSEQ_3:27;
A21: dom s = dom decomp b by A5,FINSEQ_3:31;
A22: len s = len t + len <*s1*> by A8,FINSEQ_1:35
.= len t +1 by FINSEQ_1:56;
k <= len t by A18,FINSEQ_3:27;
then A23: k < len s by A22,NAT_1:38;
then A24: k in dom decomp b by A5,A20,FINSEQ_3:27;
then A25: s/.k = s.k by A21,FINSEQ_4:def 4;
per cases by A20,AXIOMS:21;
suppose A26: 1 < k;
consider b1, b2 being bag of n such that
A27: (decomp b)/.k = <*b1, b2*> and
A28: s/.k = p.b1*O.b2 by A6,A21,A24;
b2 <> EmptyBag n by A5,A23,A26,A27,POLYNOM1:76;
hence t/.k = p.b1*0.L by A19,A25,A28,Th18
.= 0.L by VECTSP_1:36;
suppose A29: k = 1;
consider b1, b2 being bag of n such that
A30: (decomp b)/.k = <*b1, b2*> and
A31: s/.k = p.b1*O.b2 by A6,A21,A24;
(decomp b)/.1 = <*EmptyBag n, b*> by POLYNOM1:75;
then A32: b1 = EmptyBag n & b2 = b by A29,A30,GROUP_7:2;
now assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *>
by POLYNOM1:77;
then len t +1 = 0+1 by A5,A22,FINSEQ_1:56;
then len t = 0 by XCMPLX_1:2;
hence contradiction by A17,FINSEQ_1:25;
end;
then s.k = (p.EmptyBag n)*0.L by A25,A31,A32,Th18
.= 0.L by VECTSP_1:36;
hence t/.k = 0.L by A19;
end;
hence Sum t = 0.L by MATRLIN:15;
end;
hence (p*'O).b = p.b * a by A4,A9,A16,RLVECT_1:10;
end;
then (p*'O).b = p.b * a by A3 .= (p * a).b by Def11;
hence (p*'O).x = (p * a).x;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
Lm4:
for n being Ordinal,
L being Abelian left_zeroed right_zeroed add-associative
right_complementable 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 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:27
.= a * eval(p,x) by Th25;
end;
Lm5:
for n being Ordinal,
L being Abelian left_zeroed right_zeroed add-associative
right_complementable 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 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:27
.= eval(p,x) * a by Th25;
end;
theorem
for n being Ordinal,
L being Abelian left_zeroed right_zeroed add-associative
right_complementable 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 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 add-left-cancelable add-associative
right_complementable 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 add-left-cancelable add-associative
right_complementable 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)) &
eval(a*p,x) = Sum y &
for i being 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;
consider z being FinSequence of the carrier of L such that
A2: len z = len SgmX(BagOrder n, Support p) &
eval(p,x) = Sum z &
for i being 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;
A3: BagOrder n linearly_orders Support(a*p) by POLYNOM2:20;
per cases;
suppose A4: a = 0.L;
A5: now let b be bag of n;
thus (a*p).b = a * p.b by Def10 .= 0.L by A4,BINOM:1;
end;
now assume Support(a*p) <> {};
then reconsider sp = Support(a*p) as non empty Subset of Bags n;
consider c being Element of sp;
c in sp;
then (a*p).c <> 0.L by POLYNOM1:def 9;
hence contradiction by A5;
end;
then rng(SgmX(BagOrder n, Support(a*p))) = {} by A3,TRIANG_1:def 2;
then SgmX(BagOrder n, Support(a*p)) = {} by FINSEQ_1:27;
then len y = 0 by A1,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
then Sum y = 0.L by RLVECT_1:60 .= a * Sum z by A4,BINOM:1;
hence thesis by A1,A2;
suppose A6: a <> 0.L;
A7: for u being set holds u in Support p implies u in Support(a*p)
proof
let u be set;
assume A8: u in Support p;
then A9: p.u <> 0.L by POLYNOM1:def 9;
reconsider u' = u as Element of Bags n by A8;
a * p.u' <> 0.L by A6,A9,VECTSP_2:def 5;
then (a * p).u' <> 0.L by Def10;
hence thesis by POLYNOM1:def 9;
end;
A10: for u being set holds u in Support(a*p) implies u in Support p
proof
let u be set;
assume A11: u in Support(a*p);
then reconsider u' = u as Element of Bags n;
(a*p).u <> 0.L by A11,POLYNOM1:def 9;
then a * p.u' <> 0.L by Def10;
then p.u' <> 0.L by BINOM:2;
hence thesis by POLYNOM1:def 9;
end;
then A12: Support(a*p) = Support(p) by A7,TARSKI:2;
A13: len z = len y by A1,A2,A7,A10,TARSKI:2;
then A14: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3;
now let i be set;
assume A15: 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
A16: i = k & 1 <= k & k <= len z;
A17: a * z/.k = a * ((p * SgmX(BagOrder n, Support p))/.k *
eval(((SgmX(BagOrder n, Support p))/.k)@,x)) by A2,A16
.= (a * (p * SgmX(BagOrder n, Support(a*p)))/.k) *
eval(((SgmX(BagOrder n, Support(a*p)))/.k)@,x) by A12,VECTSP_1:def 16;
A18: dom z = Seg(len SgmX(BagOrder n, Support(a*p))) by A1,A14,FINSEQ_1:def 3
.= dom(SgmX(BagOrder n, Support(a*p))) by FINSEQ_1:def 3;
A19: dom p = Bags n by FUNCT_2:def 1;
now let u be set;
assume u in rng(SgmX(BagOrder n, Support(a*p)));
then u in Support(a*p) by A3,TRIANG_1:def 2;
hence u in dom p by A19;
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:20;
for u being set holds u in rng q implies u in the carrier of L
proof
let u be set;
assume u in rng q;
then A20: u in rng p by FUNCT_1:25;
rng p c= the carrier of L by RELSET_1:12;
hence thesis by A20;
end;
then rng q c= the carrier of L by TARSKI:def 3;
then reconsider q as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX(BagOrder n, Support(a*p))).k
= (SgmX(BagOrder n, Support(a*p)))/.k by A15,A16,A18,FINSEQ_4:def 4;
then k in dom q by A15,A16,A18,A19,FUNCT_1:21;
then A21: (p * SgmX(BagOrder n, Support(a*p)))/.k
= q.k by FINSEQ_4:def 4
.= p.(SgmX(BagOrder n, Support(a*p)).k) by A15,A16,A18,FUNCT_1:23
.= p.(SgmX(BagOrder n, Support(a*p))/.k) by A15,A16,A18,FINSEQ_4:def 4
;
reconsider c = SgmX(BagOrder n, Support(a*p))/.k as Element of Bags n;
reconsider c as bag of n;
A22: (a*p).(SgmX(BagOrder n, Support(a*p))/.k)
= (a*p).c
.= a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A21,Def10;
A23: dom(a*p) = Bags n by FUNCT_2:def 1;
now let u be set;
assume u in rng(SgmX(BagOrder n, Support(a*p)));
then u in Support(a*p) by A3,TRIANG_1:def 2;
hence u in dom(a*p) by A23;
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:20;
for u being set holds u in rng r implies u in the carrier of L
proof
let u be set;
assume u in rng r;
then A24: u in rng(a*p) by FUNCT_1:25;
rng(a*p) c= the carrier of L by RELSET_1:12;
hence thesis by A24;
end;
then rng r c= the carrier of L by TARSKI:def 3;
then reconsider r as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX(BagOrder n, Support(a*p))).k
= (SgmX(BagOrder n, Support(a*p)))/.k by A15,A16,A18,FINSEQ_4:def 4;
then k in dom r by A15,A16,A18,A23,FUNCT_1:21;
then ((a*p) * SgmX(BagOrder n, Support(a*p)))/.k
= r.k by FINSEQ_4:def 4
.= (a*p).(SgmX(BagOrder n, Support(a*p)).k) by A15,A16,A18,FUNCT_1:23
.= a * (p * SgmX(BagOrder n, Support(a*p)))/.k
by A15,A16,A18,A22,FINSEQ_4:def 4;
hence y/.i = a * z/.i by A1,A13,A16,A17;
end;
then y = a * z by A14,POLYNOM1:def 2;
hence thesis by A1,A2,BINOM:4;
end;
theorem
for n being Ordinal,
L being Abelian left_zeroed right_zeroed add-associative
right_complementable 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 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 add-left-cancelable add-associative
right_complementable 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 add-left-cancelable add-associative
right_complementable 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)) &
eval(p*a,x) = Sum y &
for i being 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
A2: len z = len SgmX(BagOrder n, Support p) &
eval(p,x) = Sum z &
for i being 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 A3: a = 0.L;
A4: now let b be bag of n;
thus (p*a).b = p.b * a by Def11 .= 0.L by A3,BINOM:2;
end;
A5: now assume Support(p*a) <> {};
then reconsider sp = Support(p*a) as non empty Subset of Bags n;
consider c being Element of sp;
c in sp;
then (p*a).c <> 0.L by POLYNOM1:def 9;
hence contradiction by A4;
end;
BagOrder n linearly_orders Support(p*a) by POLYNOM2:20;
then rng(SgmX(BagOrder n, Support(p*a))) = {} by A5,TRIANG_1:def 2;
then SgmX(BagOrder n, Support(p*a)) = {} by FINSEQ_1:27;
then len y = 0 by A1,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
then Sum y = 0.L by RLVECT_1:60 .= Sum z * a by A3,BINOM:2;
hence thesis by A1,A2;
case A6: a <> 0.L;
A7: BagOrder n linearly_orders Support(p*a) by POLYNOM2:20;
A8: for u being set holds u in Support p implies u in Support(p*a)
proof
let u be set;
assume A9: u in Support p;
then A10: p.u <> 0.L by POLYNOM1:def 9;
reconsider u' = u as Element of Bags n by A9;
p.u' * a <> 0.L by A6,A10,VECTSP_2:def 5;
then (p *a).u' <> 0.L by Def11;
hence thesis by POLYNOM1:def 9;
end;
A11: for u being set holds u in Support(p*a) implies u in Support p
proof
let u be set;
assume A12: u in Support(p*a);
then reconsider u' = u as Element of Bags n;
(p*a).u <> 0.L by A12,POLYNOM1:def 9;
then p.u' * a <> 0.L by Def11;
then p.u' <> 0.L by BINOM:1;
hence thesis by POLYNOM1:def 9;
end;
then A13: Support(p*a) = Support(p) by A8,TARSKI:2;
A14: len z = len y by A1,A2,A8,A11,TARSKI:2;
then A15: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3;
now let i be set;
assume A16: 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
A17: i = k & 1 <= k & k <= len z;
A18: z/.k * a = (p * SgmX(BagOrder n, Support(p*a)))/.k *
(eval(((SgmX(BagOrder n, Support(p*a)))/.k)@,x)) * a by A2,A13,A17
.= ((p * SgmX(BagOrder n, Support(p*a)))/.k * a) *
eval(((SgmX(BagOrder n, Support(p*a)))/.k)@,x) by VECTSP_1:def 16;
A19: dom z = Seg(len SgmX(BagOrder n, Support(p*a))) by A1,A15,FINSEQ_1:def 3
.= dom(SgmX(BagOrder n, Support(p*a))) by FINSEQ_1:def 3;
A20: dom p = Bags n by FUNCT_2:def 1;
now let u be set;
assume u in rng(SgmX(BagOrder n, Support(p*a)));
then u in Support(p*a) by A7,TRIANG_1:def 2;
hence u in dom p by A20;
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:20;
for u being set holds u in rng q implies u in the carrier of L
proof
let u be set;
assume u in rng q;
then A21: u in rng p by FUNCT_1:25;
rng p c= the carrier of L by RELSET_1:12;
hence thesis by A21;
end;
then rng q c= the carrier of L by TARSKI:def 3;
then reconsider q as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX(BagOrder n, Support(p*a))).k
= (SgmX(BagOrder n, Support(p*a)))/.k by A16,A17,A19,FINSEQ_4:def 4;
then k in dom q by A16,A17,A19,A20,FUNCT_1:21;
then A22: (p * SgmX(BagOrder n, Support(p*a)))/.k
= q.k by FINSEQ_4:def 4
.= p.(SgmX(BagOrder n, Support(p*a)).k) by A16,A17,A19,FUNCT_1:23
.= p.(SgmX(BagOrder n, Support(p*a))/.k) by A16,A17,A19,FINSEQ_4:def 4
;
reconsider c = SgmX(BagOrder n, Support(p*a))/.k as Element of Bags n;
reconsider c as bag of n;
A23: (p*a).(SgmX(BagOrder n, Support(p*a))/.k)
= (p*a).c
.= (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A22,Def11;
A24: dom(p*a) = Bags n by FUNCT_2:def 1;
now let u be set;
assume u in rng(SgmX(BagOrder n, Support(p*a)));
then u in Support(p*a) by A7,TRIANG_1:def 2;
hence u in dom(p*a) by A24;
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:20;
for u being set holds u in rng r implies u in the carrier of L
proof
let u be set;
assume u in rng r;
then A25: u in rng(p*a) by FUNCT_1:25;
rng(p*a) c= the carrier of L by RELSET_1:12;
hence thesis by A25;
end;
then rng r c= the carrier of L by TARSKI:def 3;
then reconsider r as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX(BagOrder n, Support(p*a))).k
= (SgmX(BagOrder n, Support(p*a)))/.k by A16,A17,A19,FINSEQ_4:def 4;
then k in dom r by A16,A17,A19,A24,FUNCT_1:21;
then ((p*a) * SgmX(BagOrder n, Support(p*a)))/.k
= r.k by FINSEQ_4:def 4
.= (p*a).(SgmX(BagOrder n, Support(p*a)).k) by A16,A17,A19,FUNCT_1:23
.= (p * SgmX(BagOrder n, Support(p*a)))/.k * a
by A16,A17,A19,A23,FINSEQ_4:def 4;
hence y/.i = z/.i * a by A1,A14,A17,A18;
end;
then y = z * a by A15,POLYNOM1:def 3;
hence thesis by A1,A2,BINOM:5;
end;
hence thesis;
end;
theorem
for n being Ordinal,
L being Abelian left_zeroed right_zeroed add-associative
right_complementable 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 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 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:27
.= eval(p,x) * a by Th25;
end;