:: {O}n {B}ag of 1. {P}art {I}
:: by Yasushige Watase
::
:: Received March 31, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, FINSEQ_1, XBOOLE_0, BINOP_1, CARD_3,
FUNCT_1, XXREAL_0, TARSKI, NAT_1, ARYTM_3, ORDERS_1, FINSET_1, ZFMISC_1,
CARD_1, PARTFUN1, ORDINAL1, ARYTM_1, FUNCOP_1, FUNCT_2, PRE_POLY,
GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, SUPINF_2, MESFUNC1,
MOD_4, POLYNOM1, ALGSEQ_1, POLYNOM3, FUNCT_4, VECTSP_2, QUOFIELD,
MSSUBFAM, RING_3, FUNCSDOM, RING_2, FDIFF_1, C0SP1, STRUCT_0, REALSET1,
POLYALG1, ALGSTR_1, PRGCOR_2, POLYALGX;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1,
REALSET1, FINSET_1, CARD_1, ORDERS_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, NAT_D, XXREAL_2, FINSEQ_1, RECDEF_1, FUNCT_7, AFINSQ_1,
PRE_POLY, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_1,
VECTSP_2, VFUNCT_1, POLYNOM1, GROUP_6, RINGCAT1, MOD_4, QUOFIELD,
POLYNOM3, POLYALG1, POLYNOM7, C0SP1, RING_2, RING_3;
constructors RELSET_1, FUNCT_3, REALSET1, ORDERS_1, NAT_D, XXREAL_2, RECDEF_1,
FUNCT_7, AFINSQ_1, VFUNCT_1, RINGCAT1, POLYNOM5, UPROOTS, POLYALG1,
POLYNOM7, RING_3;
registrations RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1, CARD_1,
FINSEQ_1, VALUED_0, RELSET_1, FUNCT_2, RFUNCT_2, STRUCT_0, VECTSP_1,
NAT_6, RING_4, POLYNOM1, PRE_POLY, VFUNCT_1, MEMBERED, POLYNOM2, FVSUM_1,
MOD_4, AFINSQ_1, POLYNOM3, FUNCOP_1, SUBSET_1, PBOOLE, RINGCAT1,
POLYALG1, REALSET1, XXREAL_2, NEWTON04, RVSUM_4, GCD_1, INT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions GROUP_1, VECTSP_1, ALGSTR_0, RLVECT_1;
equalities STRUCT_0, ORDINAL1, FINSEQ_1, VECTSP_1, POLYNOM3, ALGSTR_0,
BINOP_1, REALSET1, POLYNOM1, XBOOLE_0;
expansions TARSKI, FUNCT_2, VECTSP_1, GROUP_6, STRUCT_0, FINSEQ_1, FUNCT_1,
RING_2, GROUP_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, POLYNOM1, NAT_1, FINSEQ_1,
FUNCOP_1, RELAT_1, CARD_1, ORDINAL1, ORDERS_1, GROUP_1, XBOOLE_0, C0SP1,
XBOOLE_1, XXREAL_0, PARTFUN1, NAT_D, PRE_POLY, AFINSQ_1, WELLORD2,
BINOP_1, POLYNOM3, POLYNOM7, FUNCT_7, PBOOLE, ALGSEQ_1, VECTSP_1, RING_3,
POLYALG1, NORMSP_1, XREAL_1, XREAL_0, POLYRED, XXREAL_2, FINSEQ_3, INT_1;
schemes FUNCT_2, BINOP_1;
begin :: Preliminaries
reserve o,o1,o2 for object;
reserve n for Ordinal;
reserve R,L for non degenerated comRing;
reserve b for bag of 1;
theorem Th1:
for f be sequence of R holds
Support f = {} iff f = 0_.R
proof
let f be sequence of R;
f = 0_.R implies Support f = {}
proof
assume
A1: f = 0_.R;
Support f = {}
proof
assume Support f <> {}; then
consider o such that
A2: o in Support f by XBOOLE_0:def 1;
reconsider x1 = o as Element of NAT by A2;
f.x1 <> 0.R by A2,POLYNOM1:def 4;
hence contradiction by A1;
end;
hence thesis;
end;
hence thesis by POLYNOM1:def 4;
end;
theorem Th2:
for f be sequence of R st Support f is finite holds
f is finite-Support sequence of R
proof
let f be sequence of R;
A1: dom f = NAT by FUNCT_2:def 1;
assume
A2: Support f is finite;
per cases;
suppose Support f = {}; then
f = 0_.R by Th1;
hence thesis;
end;
suppose Support f <> {}; then
reconsider S = Support f as finite non empty Subset of NAT by A2;
reconsider m = max(S) as Element of NAT by ORDINAL1:def 12;
A3: for s be Element of S holds m >= s by XXREAL_2:4;
for i be Nat st i >= m+1 holds f.i = 0.R
proof
let i be Nat;
assume
A4: i >= m+1;
assume
A5: f.i <> 0.R;
i in dom f by A1,ORDINAL1:def 12; then
i in Support f by A5,POLYNOM1:def 4;
hence contradiction by A4,A3,NAT_1:13;
end;
hence thesis by ALGSEQ_1:def 1;
end;
end;
theorem Th3:
for f be sequence of R st f is finite-Support sequence of R holds
Support f is finite
proof
let f be sequence of R;
assume
A1: f is finite-Support sequence of R;
consider n1 be Nat such that
A2: for i be Nat st i >= n1 holds f.i = 0.R by A1,ALGSEQ_1:def 1;
A3: for m be Element of NAT st m in Support f holds m < n1
proof
let m be Element of NAT;
assume m in Support f; then
A4: f.m <> 0.R by POLYNOM1:def 4;
assume n1 <= m;
hence contradiction by A4,A2;
end;
Support f c= Segm n1 by A3,NAT_1:44;
hence thesis;
end;
Lm1:
for X be non empty set, n1,n2 be Nat holds
X --> n1 = X --> n2 implies n1 = n2
proof
let X be non empty set,n1,n2 be Nat;
assume
A1: X --> n1 = X -->n2;
{n1} = rng (X --> n1) by FUNCOP_1:8 .= rng (X --> n2) by A1
.= {n2} by FUNCOP_1:8;
hence thesis by ZFMISC_1:3;
end;
::$N Translation Bags 1 notation to NAT.
theorem Th4:
for b be bag of 1 holds dom b = {0} & rng b = {b.0}
proof
let b be bag of 1;
dom b = {0} by CARD_1:49,PARTFUN1:def 2;
hence thesis by FUNCT_1:4;
end;
theorem Th5:
for b be bag of 1 holds b = 1 --> b.0
proof
let b be bag of 1;
for o st o in dom b holds b.o = (1 --> b.0).o
proof
let o;
assume
A1: o in dom b; then
o = 0 by CARD_1:49, TARSKI:def 1;
hence thesis by A1,FUNCOP_1:7;
end;
hence thesis by PARTFUN1:def 2;
end;
theorem
for b1,b2 be bag of 1 holds b1 + b2 = 1 --> ((b1.0) + (b2.0))
proof
let b1,b2 be bag of 1;
reconsider b = b1 + b2 as bag of 1;
A1: dom(b1 + b2) = {0} by Th4 .= dom (1 --> ((b1.0) + (b2.0))) by Th4;
for x being object st x in dom(b1 + b2) holds
(b1 + b2).x = (1 --> ((b1.0) + (b2.0))).x
proof
let x be object;
assume
A2: x in dom(b1 + b2); then
x in {0} by Th4; then
(b1 + b2).x = (b1 + b2).0 by TARSKI:def 1
.= (b1.0) + (b2.0) by PRE_POLY:def 5
.= (1 --> ((b1.0) + (b2.0))).x by A2,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th7:
for b1,b2 be bag of 1 holds b1 -' b2 = 1 --> ((b1.0) -' (b2.0))
proof
let b1,b2 be bag of 1;
reconsider b = b1 -' b2 as bag of 1;
A1: dom(b1 -' b2) = {0} by Th4 .= dom (1 --> ((b1.0) -' (b2.0))) by Th4;
for x being object st x in dom(b1 -' b2) holds
(b1 -' b2).x = (1 --> ((b1.0) -' (b2.0))).x
proof
let x be object;
assume
A2: x in dom(b1 -' b2); then
x in {0} by Th4; then
(b1 -' b2).x = (b1 -' b2).0 by TARSKI:def 1
.= (b1.0) -' (b2.0) by PRE_POLY:def 6
.= (1 --> ((b1.0) -' (b2.0))).x by A2,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A1;
end;
:::Order of Bags 1
theorem Th8:
for b1,b2 be bag of 1 holds b1.0 <= b2.0 iff b1 divides b2
proof
let b1,b2 be bag of 1;
b1.0 <= b2.0 implies b1 divides b2
proof
assume
A1: b1.0 <= b2.0;
for k being object st k in 1 holds b1.k <= b2.k
proof
let k be object;
assume k in 1; then
k = 0 by TARSKI:def 1, CARD_1:49;
hence thesis by A1;
end;
hence thesis by PRE_POLY:46;
end;
hence thesis by PRE_POLY:def 11;
end;
theorem Th9:
for n being Ordinal holds BagOrder n linearly_orders Bags n
proof
let n be Ordinal;
BagOrder n linearly_orders field BagOrder n by ORDERS_1:37;
hence BagOrder n linearly_orders Bags n by ORDERS_1:12;
end;
::$N NBag1 is avvriv. for function NAT to Bags 1
definition
func NBag1 -> Function of NAT, Bags 1 means :Def1:
for m being Element of NAT holds it.m = 1 --> m;
existence
proof
defpred P[Element of NAT,object] means
$2 = 1 --> $1;
A1: for x being Element of NAT
ex y being Element of Bags 1 st P[x,y]
proof
let x be Element of NAT;
reconsider y = 1 --> x as object;
take y;
thus thesis by PRE_POLY:def 12;
end;
consider f be Function of NAT,Bags 1 such that
A2: for x being Element of NAT
holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 be Function of NAT,Bags 1;
assume that
A3: for m be Element of NAT holds f1.m = 1 --> m and
A4: for m be Element of NAT holds f2.m = 1 --> m;
now let m be Element of NAT;
thus f1.m = 1 --> m by A3 .= f2.m by A4;
end;
hence f1 = f2;
end;
end;
definition
func BagN1 -> Function of Bags 1, NAT means :Def2:
for b being Element of Bags 1 holds it.b = b.0;
existence
proof
defpred P[Element of Bags 1,object] means
$2 = $1.0;
A1: for x being Element of Bags 1
ex y being Element of NAT st P[x,y];
consider f be Function of Bags 1,NAT such that
A2: for x being Element of Bags 1
holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 be Function of Bags 1,NAT;
assume that
A3: for m be Element of Bags 1 holds f1.m = m.0 and
A4: for m be Element of Bags 1 holds f2.m = m.0;
now let m be Element of Bags 1;
thus f1.m = m.0 by A3 .= f2.m by A4;
end;
hence f1 = f2;
end;
end;
theorem Th10:
(BagN1)*(NBag1) = id NAT
proof
for o st o in dom ((BagN1)*NBag1) holds ((BagN1)*(NBag1)).o = (id NAT).o
proof
let o;
assume
A1: o in dom ((BagN1)*NBag1); then
reconsider m = o as Element of NAT;
A2: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A2,PRE_POLY:def 12;
A3: 1 --> m = b by Def1;
0 in 1 by CARD_1:49,TARSKI:def 1; then
A4: m = b.0 by A3,FUNCOP_1:7;
((BagN1)*NBag1).o = (BagN1).b by A1,FUNCT_2:15
.= o by A4,Def2
.= (id NAT).o by A1,FUNCT_1:18;
hence thesis;
end;
hence thesis by FUNCT_2:def 1;
end;
theorem Th11:
(NBag1)*(BagN1) = id(Bags 1)
proof
for o st o in dom((NBag1)*(BagN1)) holds
((NBag1)*(BagN1)).o = (id(Bags 1)).o
proof
let o;
assume o in dom ((NBag1)*(BagN1)); then
reconsider b = o as Element of Bags 1;
A1: BagN1.o = b.0 by Def2;
((NBag1)*(BagN1)).o = (NBag1).(b.0) by A1,FUNCT_2:15
.= 1-->b.0 by Def1 .= (id(Bags 1)).o by Th5;
hence thesis;
end;
hence thesis by FUNCT_2:def 1;
end;
registration
cluster NBag1 -> one-to-one onto;
coherence by FUNCT_2:23,Th11,Th10;
cluster BagN1 -> one-to-one onto;
coherence by FUNCT_2:23,Th11,Th10;
end;
theorem Th12:
for b1,b2 be bag of 1 holds (b2 in rng divisors b1 iff b2.0 <= b1.0) &
(b2 in rng divisors b1 iff b2 divides b1)
proof
let b1,b2 be bag of 1;
consider S being non empty finite Subset of (Bags 1) such that
A1: divisors b1 = SgmX ((BagOrder 1),S) &
(for p being bag of 1 holds (p in S iff p divides b1)) by PRE_POLY:def 16;
A2: BagOrder 1 linearly_orders S by Th9,ORDERS_1:38;
A3: b2 in rng(divisors b1) implies b2.0 <= b1.0
proof
assume b2 in rng(divisors b1); then
b2 in S by A1,A2,PRE_POLY:def 2;
hence thesis by A1,PRE_POLY:def 11;
end;
b2.0 <= b1.0 implies b2 in rng(divisors b1)
proof
assume b2.0 <= b1.0; then
b2 in S by A1, Th8;
hence thesis by A1,A2,PRE_POLY:def 2;
end;
hence thesis by A3,Th8;
end;
theorem Th13:
for b be bag of 1 holds
rng(divisors b) = {x where x is bag of 1 : x.0 <= b.0}
proof
let b be bag of 1;
A1: for o holds o in {x where x is bag of 1 : x.0 <= b.0} implies
o in rng(divisors b)
proof
let o;
assume o in {x where x is bag of 1 : x.0 <= b.0}; then
consider x1 be bag of 1 such that
A2: o = x1 & x1.0 <= b.0;
thus thesis by A2, Th12;
end;
for o holds o in rng divisors b implies
o in {x where x is bag of 1 : x.0 <= b.0}
proof
let o;
assume
A3: o in rng(divisors b); then
reconsider x1 = o as bag of 1;
x1.0 <= b.0 by A3,Th12;
hence thesis;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th14:
for b be bag of 1 holds
rng(NBag1|(Segm ((b.0)+1))) = {x where x is bag of 1 : x.0 <= b.0}
proof
let b be bag of 1;
A1: for o holds o in rng(NBag1|(Segm ((b.0)+1))) implies
o in {x where x is bag of 1 : x.0 <= b.0}
proof
let o;
assume o in rng(NBag1|(Segm ((b.0)+1))); then
consider x being object such that
A2: x in dom(NBag1|(Segm ((b.0)+1))) & o = (NBag1|(Segm ((b.0)+1))).x
by FUNCT_1:def 3;
reconsider m1 = x as Element of NAT by A2;
m1 < (b.0)+1 by A2, NAT_1:44; then
A3: m1 <= b.0 by NAT_1:13;
A4: (NBag1|(Segm ((b.0)+1))).x = (NBag1).x by A2,FUNCT_1:47
.= 1--> m1 by Def1;
0 in 1 by CARD_1:49,TARSKI:def 1; then
(1--> m1).0 = m1 by FUNCOP_1:7;
hence thesis by A3, A4,A2;
end;
for o holds o in {x where x is bag of 1 : x.0 <= b.0}
implies o in rng(NBag1|(Segm ((b.0)+1)))
proof
let o;
assume o in {x where x is bag of 1 : x.0 <= b.0}; then
consider x1 be bag of 1 such that
A5: o = x1 & x1.0 <= b.0;
dom x1 = {0} by CARD_1:49, PARTFUN1:def 2; then
rng x1 = {x1.0} by FUNCT_1:4; then
A6: x1 = (dom x1) --> x1.0 by FUNCOP_1:9
.= 1 --> x1.0 by PARTFUN1:def 2;
reconsider m1 = x1.0 as Element of NAT;
m1 < b.0 + 1 by A5,NAT_1:13; then
A7: m1 in dom(NBag1|(Segm ((b.0)+1))) by NAT_1:44; then
(NBag1|(Segm ((b.0)+1))).m1 = (NBag1).m1 by FUNCT_1:47
.= 1--> m1 by Def1;
hence thesis by A5,A6,A7,FUNCT_1:def 3;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th15:
for b be bag of 1 holds len (divisors b) = (b.0) + 1
proof
let b be bag of 1;
A1: card dom(NBag1|(Segm ((b.0)+1))) = card rng(NBag1|(Segm ((b.0)+1)))
by CARD_1:70;
(b.0) + 1 = card{x where x is bag of 1 : x.0 <= b.0} by Th14,A1
.= card rng(divisors b) by Th13 .= card dom (divisors b) by CARD_1:70
.= card (Seg (len (divisors b))) by FINSEQ_1:def 3
.= len (divisors b);
hence thesis;
end;
begin :: Construct Algebra of Multivariate Formal Power Series
:: Construct mutlivariable Formal Series
:: same manner as POLYALG1:def 2
definition
let n be Ordinal;
let L;
func Formal-Series(n,L) -> strict non empty AlgebraStr over L means
:Def3:
(for x be set holds x in the carrier of it iff x is Series of n,L) &
(for x,y be Element of it, p,q be Series of n,L st x = p & y = q holds
x+y = p+q) &
(for x,y be Element of it, p,q be Series of n,L st x = p & y = q holds
x*y = p*'q) &
(for a be Element of L, x be Element of it, p be Series of n,L st x = p
holds a*x = a*p) & 0.it = 0_(n,L) & 1.it = 1_(n,L);
existence
proof
A1: 0_(n,L) in the set of all x where x is Series of n,L; then
reconsider Ca = the set of all x where x is Series of n,L as non empty set;
reconsider Ze = 0_(n,L) as Element of Ca by A1;
defpred P[set,set,set] means
ex p,q be Series of n,L st p=$1 & q=$2 & $3=p+q;
A2: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca; then
consider p be Series of n,L such that
A3: x=p;
y in Ca; then
consider q be Series of n,L such that
A4: y=q;
p+q in Ca; then
reconsider u=p+q as Element of Ca;
take u,p,q;
thus thesis by A3,A4;
end;
consider Ad be Function of [:Ca,Ca:],Ca such that
A5: for x,y be Element of Ca holds P[x,y,Ad.(x,y)] from BINOP_1:sch 3(A2);
1_(n,L) in the set of all x where x is Series of n,L; then
reconsider Un = 1_(n,L) as Element of Ca;
defpred P[set,set,set] means ex p,q be Series of n,L st p=$1 & q=$2 &
$3=p*'q;
A6: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca; then
consider p be Series of n,L such that
A7: x=p;
y in Ca; then
consider q be Series of n,L such that
A8: y=q;
p*'q in Ca; then
reconsider u=p*'q as Element of Ca;
take u,p,q;
thus thesis by A7,A8;
end;
consider Mu be Function of [:Ca,Ca:],Ca such that
A9: for x,y be Element of Ca holds P[x,y,Mu.(x,y)] from BINOP_1:sch 3(A6);
defpred P[Element of L,set,set] means ex p be Series of n,L st p=$2 & $3=
$1*p;
A10: for a being Element of L,x be Element of Ca ex u be Element of Ca st
P[a,x,u]
proof
let a be Element of L,x be Element of Ca;
x in Ca; then
consider q be Series of n,L such that
A11: x = q;
a*q in Ca; then
reconsider u = a*q as Element of Ca;
take u,q;
thus thesis by A11;
end;
consider lm being Function of [:the carrier of L,Ca:],Ca such that
A12: for a being Element of L,x be Element of Ca holds P[a,x,lm.(a,x)]
from BINOP_1:sch 3(A10);
reconsider P = AlgebraStr(# Ca, Ad, Mu, Ze, Un, lm #) as strict non empty
AlgebraStr over L;
take P;
thus for x be set holds x in the carrier of P iff x is Series of n,L
proof
let x be set;
thus x in the carrier of P implies x is Series of n,L
proof
assume x in the carrier of P; then
ex p be Series of n,L st x=p;
hence thesis;
end;
thus thesis;
end;
thus for x,y be Element of P, p,q be Series of n,L st x = p & y = q holds
x+y = p+q
proof
let x,y be Element of P;
let p,q be Series of n,L;
assume
A13: x = p & y = q;
ex p1,q1 be Series of n,L st p1 = x & q1 = y & Ad.(x,y) = p1+q1 by A5;
hence thesis by A13;
end;
thus for x,y be Element of P, p,q be Series of n,L st x = p & y = q holds
x*y = p*'q
proof
let x,y be Element of P;
let p,q be Series of n,L;
assume
A14: x = p & y = q;
ex p1,q1 be Series of n,L st p1 = x & q1 = y & Mu.(x,y) = p1*'q1 by A9;
hence thesis by A14;
end;
thus for a be Element of L, x be Element of P, p be Series of n,L st x = p
holds a*x = a*p
proof
let a be Element of L, x be Element of P, p be Series of n,L such that
A15: x = p;
ex p1 being Series of n,L st x = p1 & lm.(a,x)=a*p1 by A12;
hence thesis by A15;
end;
thus 0.P = 0_(n,L);
thus thesis;
end;
uniqueness
proof
let P1,P2 be strict non empty AlgebraStr over L such that
A16: for x be set holds x in the carrier of P1 iff x is Series of n,L and
A17: for x,y be Element of P1, p,q be Series of n,L st x = p & y = q
holds x+y = p+q and
A18: for x,y be Element of P1, p,q be Series of n,L st x = p & y = q
holds x*y = p*'q and
A19: for a be Element of L, x be Element of P1, p be Series of n,L st
x = p holds a*x = a*p and
A20: 0.P1 = 0_(n,L) & 1.P1 = 1_(n,L) and
A21: for x be set holds x in the carrier of P2 iff x is Series of n,L and
A22: for x,y be Element of P2, p,q be Series of n,L st x = p & y = q
holds x+y = p+q and
A23: for x,y be Element of P2, p,q be Series of n,L st x = p & y = q
holds x*y = p*'q and
A24: for a be Element of L, x be Element of P2, p be Series of n,L st
x = p holds a*x = a*p and
A25: 0.P2 = 0_(n,L) & 1.P2 = 1_(n,L);
A26: now
let x be object;
x in the carrier of P1 iff x is Series of n,L by A16;
hence x in the carrier of P1 iff x in the carrier of P2 by A21;
end;
then
A27: the carrier of P1 = the carrier of P2 by TARSKI:2;
now
let a be Element of L, x be Element of P1;
reconsider p=x as Series of n,L by A16;
reconsider x1=x as Element of P2 by A26;
reconsider a1=a as Element of L;
thus (the lmult of P1).(a,x) = a*x .= a1*p by A19 .= a1*x1 by A24
.= (the lmult of P2).(a,x);
end; then
A28: the lmult of P1=the lmult of P2 by A27,BINOP_1:2;
A29: now
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A26;
reconsider x1=x as Element of P2 by A26;
reconsider p=x as Series of n,L by A16;
reconsider q=y as Series of n,L by A21;
thus (the multF of P1).(x,y) = x*y1 .= p*'q by A18 .= x1*y by A23
.= (the multF of P2).(x,y);
end;
now
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A26;
reconsider x1=x as Element of P2 by A26;
reconsider p=x as Series of n,L by A16;
reconsider q=y as Series of n,L by A21;
thus (the addF of P1).(x,y) = x+y1 .= p+q by A17 .= x1+y by A22
.= (the addF of P2).(x,y);
end;
then the addF of P1 = the addF of P2 by A27,BINOP_1:2;
hence thesis by A20,A25,A27,A29,A28,BINOP_1:2;
end;
end;
registration
let n be Ordinal;
let L;
cluster Formal-Series(n,L) -> Abelian;
coherence
proof
let p,q be Element of Formal-Series(n,L);
reconsider p1=p, q1=q as Series of n,L by Def3;
thus p + q = p1 + q1 by Def3 .= q + p by Def3;
end;
cluster Formal-Series(n,L) -> add-associative;
coherence
proof
let p,q,r be Element of Formal-Series(n,L);
reconsider p1=p, q1=q, r1=r as Series of n,L by Def3;
A1: q + r = q1 + r1 by Def3;
p + q = p1 + q1 by Def3;
hence (p + q) + r = (p1 + q1) + r1 by Def3 .= p1 + (q1 + r1) by POLYNOM1:21
.= p + (q + r) by A1,Def3;
end;
cluster Formal-Series(n,L) -> right_zeroed;
coherence
proof
let p be Element of Formal-Series(n,L);
reconsider p1=p as Series of n,L by Def3;
0.(Formal-Series(n,L)) = 0_(n,L) by Def3;
hence p + 0.(Formal-Series(n,L)) = p1 + 0_(n,L) by Def3
.= p by POLYNOM1:23;
end;
cluster Formal-Series(n,L) -> right_complementable;
coherence
proof
let p be Element of Formal-Series(n,L);
reconsider p1=p as Series of n,L by Def3;
reconsider q = -p1 as Element of Formal-Series(n,L) by Def3;
take q;
thus p + q = p1 - p1 by Def3 .= 0_(n,L) by POLYNOM1:24
.= 0.(Formal-Series(n,L)) by Def3;
end;
cluster Formal-Series(n,L) -> commutative;
coherence
proof
let p,q be Element of Formal-Series(n,L);
reconsider p1=p, q1=q as Series of n,L by Def3;
thus p * q = p1 *' q1 by Def3 .= q * p by Def3;
end;
cluster Formal-Series(n,L) -> associative;
coherence
proof
let p,q,r be Element of Formal-Series(n,L);
reconsider p1=p, q1=q, r1=r as Series of n,L by Def3;
A2: q * r = q1 *' r1 by Def3;
p * q = p1 *' q1 by Def3;
hence (p * q) * r = (p1 *' q1) *' r1 by Def3
.= p1 *' (q1 *' r1) by POLYNOM1:27 .= p * (q * r) by A2,Def3;
end;
end;
registration
cluster add-associative associative right_zeroed left_zeroed well-unital
right_complementable distributive for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
Lm2: now
let n be Ordinal, L;
set F = Formal-Series(n,L);
let x, e be Element of F;
reconsider a=x, b=e as Series of n,L by Def3;
assume
A1: e = 1_(n,L);
thus x * e = a*'b by Def3 .= x by A1,POLYNOM1:29;
thus e * x = b*'a by Def3 .= x by A1,POLYNOM1:30;
end;
registration
let n be Ordinal;
let L;
cluster Formal-Series(n,L) -> well-unital;
coherence
proof
let x be Element of Formal-Series(n,L);
set F = Formal-Series(n,L);
1.F = 1_(n,L) by Def3;
hence thesis by Lm2;
end;
cluster Formal-Series(n,L) -> right-distributive;
coherence
proof
let p,q,r be Element of Formal-Series(n,L);
reconsider p1=p, q1=q, r1=r as Series of n,L by Def3;
A1: p*q = p1*'q1 & p*r = p1*'r1 by Def3;
q+r = q1+r1 by Def3;
hence p*(q+r) = p1*'(q1+r1) by Def3 .= p1*'q1+p1*'r1 by POLYNOM1:26
.= p*q+p*r by A1,Def3;
end;
cluster Formal-Series(n,L) -> left-distributive;
coherence;
end;
theorem Th16:
for n be Ordinal,L
for a being Element of L, p,q being Series of n,L holds a*(p+q)=a*p + a*q
proof
let n be Ordinal, L;
let a be Element of L, p,q be Series of n,L;
for i be Element of Bags n holds (a*(p+q)).i = (a*p + a*q).i
proof
let i be Element of Bags n;
a*((p+q).i) = a*(p.i + q.i) by POLYNOM1:15
.= a*(p.i) + a*(q.i) by VECTSP_1:def 7
.= (a*p).i + a*(q.i) by POLYNOM7:def 9
.= (a*p).i + (a*q).i by POLYNOM7:def 9
.= (a*p + a*q).i by POLYNOM1:15;
hence thesis by POLYNOM7:def 9;
end;
hence thesis;
end;
theorem Th17:
for n be Ordinal, L
for a,b being Element of L, p being Series of n,L holds (a+b)*p = a*p + b*p
proof
let n be Ordinal, L;
let a,b be Element of L, p be Series of n,L;
for i be Element of Bags n holds ((a+b)*p).i = (a*p + b*p).i
proof
let i be Element of Bags n;
thus ((a+b)*p).i = (a+b)*p.i by POLYNOM7:def 9
.= a*p.i + b*p.i by VECTSP_1:def 7 .= (a*p).i + b*p.i by POLYNOM7:def 9
.= (a*p).i + (b*p).i by POLYNOM7:def 9 .= (a*p + b*p).i by POLYNOM1:15;
end;
hence thesis;
end;
theorem Th18:
for n be Ordinal,L
for a,b being Element of L, p being Series of n,L holds (a*b)*p = a*(b*p)
proof
let n be Ordinal, L;
let a,b be Element of L, p be Series of n,L;
for i be Element of Bags n holds ((a*b)*p).i = (a*(b*p)).i
proof
let i be Element of Bags n;
thus ((a*b)*p).i = (a*b)*p.i by POLYNOM7:def 9
.= a*(b*(p.i)) by GROUP_1:def 3 .= a*(b*p).i by POLYNOM7:def 9
.= (a*(b*p)).i by POLYNOM7:def 9;
end;
hence thesis;
end;
theorem Th19:
for n be Ordinal,L
for p being Series of n,L holds 1.L*p = p
proof
let n be Ordinal, L;
let p be Series of n,L;
for i being Element of Bags n holds ((1.L)*p).i = p.i
proof
let i be Element of Bags n;
thus ((1.L)*p).i = (1.L)*p.i by POLYNOM7:def 9 .= p.i;
end;
hence thesis;
end;
registration
let n be Ordinal, L;
cluster Formal-Series(n,L) -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof set F = Formal-Series(n,L);
thus F is vector-distributive
proof
let x be Element of L;
let v,w be Element of Formal-Series(n,L);
reconsider p=v, q=w as Series of n,L by Def3;
reconsider x9=x as Element of L;
reconsider k=v+w as Element of Formal-Series(n,L);
A1: x*v = x*p by Def3;
reconsider r=k as Series of n,L by Def3;
A2: x*w = x*q by Def3;
x*k = x*r by Def3;
hence x*(v+w) = x*(p+q) by Def3 .= x*p + x*q by Th16
.= x*v + x*w by A1,A2,Def3;
end;
thus F is scalar-distributive
proof
let x,y be Element of L;
let v be Element of Formal-Series(n,L);
reconsider p=v as Series of n,L by Def3;
reconsider x9=x, y9=y as Element of L;
A3: x*v = x*p by Def3;
A4: y*v = y*p by Def3;
thus (x+y)*v = (x9+y9)*p by Def3 .= x9*p + y9*p by Th17
.= x*v + y*v by A3,A4,Def3;
end;
thus F is scalar-associative
proof
let x,y be Element of L;
let v be Element of Formal-Series(n,L);
reconsider p=v as Series of n,L by Def3;
reconsider x9=x, y9=y as Element of L;
A5: y*v = y*p by Def3;
thus (x*y)*v = (x9*y9)*p by Def3 .= x9*(y9*p) by Th18
.= x*(y*v) by A5,Def3;
end;
let v be Element of F;
reconsider p=v as Series of n,L by Def3;
thus (1.L)*v = 1.L*p by Def3 .= v by Th19;
end;
end;
theorem Th20:
for n be Ordinal, L holds Formal-Series(n,L) is mix-associative
proof
let n be Ordinal, L;
for a being Element of L
for x, y being Element of Formal-Series(n,L) holds a*(x*y) = (a*x)*y
proof
let a be Element of L;
for x, y being Element of Formal-Series(n,L) holds a*(x*y) = (a*x)*y
proof
let x, y be Element of Formal-Series(n,L);
reconsider x1=x, y1=y as Element of Formal-Series(n,L);
reconsider p=x1, q=y1 as Series of n,L by Def3;
A1: a*x = a*p by Def3;
x*y = p*'q by Def3;
hence a*(x*y) = a*(p*'q) by Def3 .=(a*p)*'q by POLYRED:12
.= (a*x)*y by A1,Def3;
end;
hence thesis;
end;
hence thesis by POLYALG1:def 1;
end;
registration
let n be Ordinal;
let L;
cluster Formal-Series(n,L) -> mix-associative;
coherence by Th20;
end;
begin :: Construction of Isomorphism from Formal-Series(1,R) to Formal-Series R.
theorem Th21:
Polynom-Ring(n,R) is Subring of Formal-Series(n,R)
proof
set PR = Polynom-Ring(n,R),
FS = Formal-Series(n,R),
X = [: the carrier of PR, the carrier of PR:],
Y = [: the carrier of FS, the carrier of FS:];
A1: o in the carrier of PR implies o in the carrier of FS
proof
assume o in the carrier of PR; then
o is Polynomial of n,R by POLYNOM1:def 11;
hence thesis by Def3;
end;
A2: the carrier of PR c= the carrier of FS by A1;
A3: the addF of PR = (the addF of FS)||(the carrier of PR)
proof
A4: dom (the addF of PR) = X by FUNCT_2:def 1;
dom (the addF of FS) = Y by FUNCT_2:def 1; then
A5: dom (the addF of FS) /\ X = X by XBOOLE_1:28, A2,ZFMISC_1:96;
for o st o in dom (the addF of PR) holds
(the addF of PR).o = (the addF of FS).o
proof
let o;
assume o in dom the addF of PR; then
consider o1,o2 such that
A6: o1 in the carrier of PR & o2 in the carrier of PR &
o = [o1,o2] by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of PR by A6;
reconsider s1 = x, s2 = y as finite-Support Series of n,R
by POLYNOM1:def 11;
reconsider x1 = x, y1 = y as Element of the carrier of FS by A1;
(the addF of PR).[x,y] = x + y
.= s1 + s2 by POLYNOM1:def 11 .= x1 + y1 by Def3
.= (the addF of FS).[x1,y1];
hence thesis by A6;
end;
hence thesis by A4,A5,FUNCT_1:46;
end;
A7: the multF of PR = (the multF of FS)||(the carrier of PR)
proof
A8: dom (the multF of FS) = Y by FUNCT_2:def 1;
A9: dom (the multF of PR) = X by FUNCT_2:def 1;
A10: dom (the multF of FS) /\ X = X by A8,XBOOLE_1:28, A2,ZFMISC_1:96;
for o st o in dom the multF of PR holds
(the multF of PR).o = (the multF of FS).o
proof
let o;
assume o in dom the multF of PR; then
consider o1,o2 such that
A11: o1 in the carrier of PR & o2 in the carrier of PR &
o = [o1,o2] by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of PR by A11;
reconsider s1 = x, s2 = y as finite-Support Series of n,R
by POLYNOM1:def 11;
reconsider x1 = x, y1 = y as Element of the carrier of FS by A1;
(the multF of PR).[x,y] = x * y .= s1 *' s2 by POLYNOM1:def 11
.= x1 * y1 by Def3.= (the multF of FS).[x1,y1];
hence thesis by A11;
end;
hence thesis by A9,A10,FUNCT_1:46;
end;
A12: 0.PR = 0_(n,R) by POLYNOM1:def 11 .= 0.FS by Def3;
1.PR = 1_(n,R) by POLYNOM1:def 11 .= 1.FS by Def3;
hence thesis by A1,TARSKI:def 3, A3,A7,A12,C0SP1:def 3;
end;
::borrow from C0SP1:def 3
Lm3:
for V be Ring, V1 be Subring of V holds
( for v1,w1 be Element of V1, v,w be Element of V st v1=v & w1=w
holds v1+w1=v+w ) &
( for v1, w1 be Element of V1, v,w be Element of V st v1=v & w1=w
holds v1*w1=v*w ) & 1_V1 = 1_V & 0.V1=0.V
proof
let V be Ring, V1 be Subring of V;
hereby
let x1,y1 be Element of V1, x,y be Element of V;
assume
A1: x1=x & y1=y;
x1 + y1 = ((the addF of V)||the carrier of V1).[x1,y1] by C0SP1:def 3;
hence x1 + y1 = x+y by A1,FUNCT_1:49;
end;
hereby
let x1,y1 be Element of V1, x,y be Element of V;
assume
A2: x1=x & y1=y;
x1 * y1 = ((the multF of V)||the carrier of V1).[x1,y1] by C0SP1:def 3;
hence x1 * y1 = x*y by A2,FUNCT_1:49;
end;
thus thesis by C0SP1:def 3;
end;
theorem
for R holds (0_(1,R))*NBag1 = 0_.R
proof
let R;
for o st o in dom ((0_(1,R))*NBag1) holds ((0_(1,R))*NBag1).o = (0_.R).o
proof
let o;
assume
A1: o in dom ((0_(1,R))*NBag1); then
reconsider m = o as Element of NAT;
A2: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A2,PRE_POLY:def 12;
((0_(1,R))*NBag1).o = (0_(1,R)).b by A1,FUNCT_2:15
.= (0_.R).m .= (0_.R).o;
hence thesis;
end;
hence thesis by FUNCT_2:def 1;
end;
theorem Th23:
for R holds (0_(1,R)+*(EmptyBag 1,1.R))*NBag1 = 0_.R +* (0,1.R)
proof
let R;
A1: dom(0_.R +* (0,1.R)) = NAT by FUNCT_2:def 1
.= dom ((0_(1,R)+*(EmptyBag 1,1.R))*NBag1) by FUNCT_2:def 1;
for o st o in dom(0_.R +* (0,1.R)) holds
((0_(1,R)+*(EmptyBag 1,1.R))*NBag1).o = (0_.R +* (0,1.R)).o
proof
let o;
assume
A2: o in dom(0_.R +* (0,1.R)); then
reconsider m = o as Element of NAT;
A3: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A3,PRE_POLY:def 12;
A4: EmptyBag 1 in dom(0_(1,R));
A5: 0 in dom(0_.R);
per cases;
suppose
A6: m = 0; then
NBag1.o = EmptyBag 1 by A3, PBOOLE:def 3; then
((0_(1,R)+*(EmptyBag 1,1.R))*NBag1).o =
(0_(1,R)+*(EmptyBag 1,1.R)).(EmptyBag 1) by A2,FUNCT_2:15
.= 1.R by A4,FUNCT_7:31 .= (0_.R +* (0,1.R)).0 by A5,FUNCT_7:31;
hence thesis by A6;
end;
suppose
A7: m <> 0;
A8: 1 --> m in Bags 1 by PRE_POLY:def 12;
((0_(1,R)+*(EmptyBag 1,1.R))*NBag1).o =
(0_(1,R)+*(EmptyBag 1,1.R)).(1-->m) by A3,FUNCT_2:15
.= (Bags 1 --> 0.R).(1-->m) by A7,FUNCT_7:32
.= (0_.R).o by A8,FUNCOP_1:7
.= (0_.R +* (0,1.R)).o by A7,FUNCT_7:32;
hence thesis;
end;
end;
hence thesis by A1;
end;
theorem
for R holds (0_(1,R)+*(1-->1,1.R))*NBag1 = 0_.R +* (1,1.R)
proof
let R;
A1: dom(0_.R +* (1,1.R)) = NAT by FUNCT_2:def 1
.= dom ((0_(1,R)+*(1-->1,1.R))*NBag1) by FUNCT_2:def 1;
for o st o in dom(0_.R +* (1,1.R)) holds
((0_(1,R)+*(1-->1,1.R))*NBag1).o = (0_.R +* (1,1.R)).o
proof
let o;
assume
A2: o in dom(0_.R +* (1,1.R)); then
reconsider m = o as Element of NAT;
A3: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A3,PRE_POLY:def 12;
A4: 1-->1 in dom(0_(1,R)) by PRE_POLY:def 12;
A5: 1 in dom(0_.R);
per cases;
suppose
A6: m = 1; then
NBag1.o = 1-->1 by Def1; then
((0_(1,R)+* (1-->1,1.R))*NBag1).o =
(0_(1,R)+* (1-->1,1.R)).(1-->1) by A2,FUNCT_2:15
.= 1.R by A4,FUNCT_7:31 .= (0_.R +* (1,1.R)).1 by A5,FUNCT_7:31;
hence thesis by A6;
end;
suppose
A7: m <> 1;
A8: 1 --> m in Bags 1 by PRE_POLY:def 12;
((0_(1,R)+*(1-->1,1.R))*NBag1).o =
(0_(1,R)+*(1-->1,1.R)).(1-->m) by A3,FUNCT_2:15
.= (0_(1,R)).(1-->m) by A7,Lm1,FUNCT_7:32
.= (0_.R).o by A8,FUNCOP_1:7
.= (0_.R +* (1,1.R)).o by A7,FUNCT_7:32;
hence thesis;
end;
end;
hence thesis by A1;
end;
theorem Th25:
for b be bag of 1 holds
SgmX((BagOrder 1),rng(divisors b)) = XFS2FS(NBag1|(Segm ((b.0)+1))) &
divisors b = XFS2FS(NBag1|(Segm ((b.0)+1)))
proof
let b be bag of 1;
set F = NBag1|(Segm((b.0)+1));
A1: rng XFS2FS(NBag1|(Segm ((b.0)+1))) = rng(NBag1|(Segm ((b.0)+1)))
by AFINSQ_1:97
.= {x where x is bag of 1 : x.0 <= b.0} by Th14
.= rng(divisors b) by Th13;
A2: len (NBag1|(Segm ((b.0)+1))) = (b.0) + 1;
A3: for n,m be Nat st n in dom XFS2FS(F) & m in dom XFS2FS(F) & n < m holds
(XFS2FS(F))/.n <> (XFS2FS(F))/.m &
[(XFS2FS(F))/.n,(XFS2FS(F))/.m] in BagOrder 1
proof
let n,m be Nat;
assume
A4: n in dom XFS2FS(F) & m in dom XFS2FS(F) & n < m;
A5: (XFS2FS(F))/.n <> (XFS2FS(F))/.m
proof
assume (XFS2FS(F))/.n = (XFS2FS(F))/.m; then
(XFS2FS(F)).n = (XFS2FS(F))/.m by A4,PARTFUN1:def 6
.= (XFS2FS(F)).m by A4,PARTFUN1:def 6;
hence contradiction by A4,FUNCT_1:def 4;
end;
len XFS2FS(F) = len F by AFINSQ_1:def 9; then
A6: n in Seg len F & m in Seg len F by A4,FINSEQ_1:def 3; then
A7: 1 <= n <= (b.0) +1 & 1 <= m <= (b.0) +1 by FINSEQ_1:1; then
A8: n - 1 = n -' 1 by XREAL_1:233;
A9: n < m <= (b.0) +1 by A6, FINSEQ_1:1,A4; then
A10: n < (b.0) + 1 by XXREAL_0:2;
A11: 1 <= n < ((b.0) +1) by A6, FINSEQ_1:1,A9,XXREAL_0:2;
A12: m - 1 = m -' 1 by A7,XREAL_1:233;
n - 1 <= n by A8,NAT_D:35; then
n - 1 < (b.0) + 1 by A10, XXREAL_0:2; then
A13: n - 1 in dom(NBag1|Segm((b.0)+1)) by A8,NAT_1:44;
A14: (XFS2FS(F))/.n = (XFS2FS(F)).n by A4,PARTFUN1:def 6
.= (NBag1|Segm((b.0)+1)).(n-1) by A2,A11,AFINSQ_1:def 9
.= (NBag1).(n-1) by A13,FUNCT_1:47 .= 1--> (n-1) by A8,Def1;
A15: 0 in 1 by CARD_1:49,TARSKI:def 1; then
A16: (1--> (n -'1)).0 = (n -'1) by FUNCOP_1:7;
A17: (1--> (m -'1)).0 = m -'1 by A15,FUNCOP_1:7;
[(XFS2FS(F))/.n,(XFS2FS(F))/.m] in BagOrder 1
proof
A18: m -'1 in dom(NBag1|Segm ((b.0)+1))
proof
per cases;
suppose
A19: m = (b.0) + 1;
(b.0) +0 < (b.0) +1 by XREAL_1:8;
hence thesis by A19,NAT_1:44;
end;
suppose
m <> (b.0) + 1; then
A20: 1 <= m < (b.0) +1 by A7,XXREAL_0:1;
m -' 1 <= m by NAT_D:35; then
m -'1 < (b.0) + 1 by A20, XXREAL_0:2;
hence thesis by NAT_1:44;
end;
end;
A21: (XFS2FS(F))/.m = (XFS2FS(F)).m by A4,PARTFUN1:def 6
.= (NBag1|Segm((b.0)+1)).(m-1) by A2,A7,AFINSQ_1:def 9
.= (NBag1).(m-1) by A12,A18,FUNCT_1:47 .= 1--> (m -1) by A12,Def1;
1--> (n -'1) divides 1--> (m -'1)
by A16,A8,A12,A4,XREAL_1:9,A17,Th8; then
1--> (n -'1) <=' 1--> (m -'1) by PRE_POLY:49;
hence thesis by A8,A12,A21,A14,PRE_POLY:def 14;
end;
hence thesis by A5;
end;
reconsider S = rng divisors b
as non empty finite Subset of Bags 1;
A22: SgmX((BagOrder 1),S)
= XFS2FS(NBag1|(Segm ((b.0)+1))) by A3,PRE_POLY:9,A1;
for p being bag of 1 holds p in S iff p divides b by Th12;
hence thesis by A22,PRE_POLY:def 16;
end;
begin :: Construct Isomorphism Formal-Series(1,R) -> Formal-Series R
definition
let R;
func BSFSeri(R) -> Function of Formal-Series(1,R), Formal-Series R means
:Def4:
for x being object st x in the carrier of Formal-Series(1,R) holds
ex x1 being Series of 1,R st x1 = x & it.x = x1*(NBag1);
existence
proof
defpred P[object,object] means
ex x1 be Series of 1,R st x1 = $1 & $2 = x1*NBag1;
A1: for x being object st x in the carrier of Formal-Series(1,R)
ex y being object st y in the carrier of Formal-Series R & P[x,y]
proof
let x be object;
assume x in the carrier of Formal-Series(1,R); then
reconsider x1 = x as Series of 1,R by Def3;
take y = x1*NBag1;
thus thesis by POLYALG1:def 2;
end;
ex g being Function of Formal-Series(1,R), Formal-Series R
st for x being object st x in the carrier of Formal-Series(1,R) holds
P[x,g.x] from FUNCT_2:sch 1(A1); then
consider g being Function of Formal-Series(1,R),Formal-Series R such that
A2: for x being object st x in the carrier of Formal-Series(1,R) holds
ex x1 being Series of 1,R st x1 = x & g.x = x1*NBag1;
take g;
thus thesis by A2;
end;
uniqueness
proof
set FS1 = Formal-Series(1,R);
set FS = Formal-Series R;
let f,g be Function of FS1, FS such that
A3: for x be object st x in the carrier of FS1 holds
ex x1 be Series of 1,R st x1 = x & f.x = x1*NBag1 and
A4: for x be object st x in the carrier of FS1 holds
ex x1 be Series of 1,R st x1 = x & g.x = x1*NBag1;
now
let x be object;
assume
A5: x in the carrier of FS1; then
consider x1 be Series of 1,R such that
A6: x1 = x & f.x = x1*NBag1 by A3;
consider x2 be Series of 1,R such that
A7: x2 = x & g.x = x2*NBag1 by A4,A5;
f.x = x2*NBag1 by A6,A7 .= g.x by A7;
hence f.x = g.x;
end;
hence thesis;
end;
end;
Lm4:
for R holds BSFSeri(R) is one-to-one onto
proof
let R;
A1: for x1,x2 be object st x1 in dom BSFSeri(R) & x2 in dom BSFSeri(R) &
(BSFSeri(R)).x1 = (BSFSeri(R)).x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A2: x1 in dom BSFSeri(R) & x2 in dom BSFSeri(R) &
(BSFSeri(R)).x1 = (BSFSeri(R)).x2; then
consider xx1 being Series of 1,R such that
A3: xx1 = x1 & (BSFSeri(R)).x1 = xx1*(NBag1) by Def4;
consider xx2 being Series of 1,R such that
A4: xx2 = x2 & (BSFSeri(R)).x2 = xx2*(NBag1) by A2,Def4;
A5: for o be object st o in Bags 1 holds (xx1).o = (xx2).o
proof
let o be object;
assume o in Bags 1; then
reconsider b = o as Element of Bags 1;
A6: b = 1 --> (b.0) by Th5 .= NBag1.(b.0) by Def1;
(xx1).o = ((xx2)*(NBag1)).(b.0) by A3,A4,A2,A6,FUNCT_2:15
.= (xx2).o by A6,FUNCT_2:15;
hence thesis;
end;
x1 = xx1 by A3 .= xx2 by A5 .= x2 by A4;
hence thesis;
end;
rng BSFSeri(R) = the carrier of Formal-Series R
proof
for o st o in the carrier of Formal-Series R
ex x be object st x in the carrier of Formal-Series(1,R) &
o = (BSFSeri(R)).x
proof
let o;
assume o in the carrier of Formal-Series R; then
reconsider s = o as sequence of R by POLYALG1:def 2;
s*BagN1 in the carrier of Formal-Series(1,R) by Def3; then
consider x be object such that
A7: x in the carrier of Formal-Series(1,R) & x = s*BagN1;
consider x1 being Series of 1,R such that
A8: x1 = x & (BSFSeri(R)).x = x1*(NBag1) by A7, Def4;
(BSFSeri(R)).x = s*((BagN1)*(NBag1)) by A7,A8,RELAT_1:36
.= o by FUNCT_2:17, Th10;
hence thesis by A7;
end;
hence thesis by FUNCT_2:10;
end;
hence thesis by A1;
end;
registration
let R;
cluster BSFSeri(R) -> one-to-one onto;
coherence by Lm4;
end;
theorem Th26:
for R be Ring, f,g be Series of 1,R holds
(f+g)*(NBag1) = f*(NBag1) + g*(NBag1)
proof
let R be Ring, f,g be Series of 1,R;
for o st o in NAT holds ((f+g)*NBag1).o = (f*(NBag1) + g*(NBag1)).o
proof
let o;
assume
A1: o in NAT; then
reconsider m = o as Element of NAT;
A2: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A2,PRE_POLY:def 12;
A3: f.b = (f*(NBag1)).m by FUNCT_2:15;
A4: g.b = (g*(NBag1)).m by FUNCT_2:15;
((f+g)*NBag1).o = (f+g).b by A1,FUNCT_2:15
.= (f*(NBag1)).m + (g*(NBag1)).m by A3,A4,POLYNOM1:15
.= (f*(NBag1) + g*(NBag1)).o by NORMSP_1:def 2;
hence thesis;
end;
hence thesis;
end;
theorem Th27:
for f,g be Element of Formal-Series(1,R) holds
(BSFSeri(R)).(f+g) = (BSFSeri(R)).f + (BSFSeri(R)).g
proof
let f,g be Element of Formal-Series(1,R);
consider f1 being Series of 1,R such that
A1: f1 = f & (BSFSeri(R)).f = f1*(NBag1) by Def4;
consider g1 being Series of 1,R such that
A2: g1 = g & (BSFSeri(R)).g = g1*(NBag1) by Def4;
consider fg1 being Series of 1,R such that
A3: fg1 = f+g & (BSFSeri(R)).(f+g) = fg1*(NBag1) by Def4;
A4: fg1 = f1 + g1 by A1,A2,A3,Def3;
(BSFSeri(R)).(f+g) = f1*(NBag1) + g1*(NBag1) by A3,A4,Th26
.= (BSFSeri(R)).f + (BSFSeri(R)).g by A1,A2,POLYALG1:def 2;
hence thesis;
end;
theorem Th28:
for f,g be Series of 1,R holds (f*'g)*(NBag1) = (f*(NBag1)) *' (g*(NBag1))
proof
let f,g be Series of 1,R;
for o st o in NAT holds ((f*'g)*(NBag1)).o = ((f*(NBag1))*'(g*(NBag1))).o
proof
let o;
assume
A1: o in NAT; then
reconsider m = o as Element of NAT;
A2: NBag1.o = 1 --> m by Def1;
reconsider b = (NBag1).o as Element of Bags 1 by A2,PRE_POLY:def 12;
A3: 0 in 1 by CARD_1:49,TARSKI:def 1; then
A4: (b.0) = m by A2,FUNCOP_1:7;
set F = NBag1|(Segm((b.0)+1));
consider s being FinSequence of the carrier of R such that
A5: (f*'g).b = Sum s & len s = len decomp b &
for k being Element of NAT st k in dom s ex b1, b2 being bag of 1 st
(decomp b)/.k = <*b1, b2*> & s/.k = f.b1*g.b2 by POLYNOM1:def 10;
A6: ((f*'g)*NBag1).o = (f*'g).b by A1,FUNCT_2:15 .= Sum s by A5;
consider r be FinSequence of the carrier of R such that
A7: len r = m+1 & ((f*(NBag1)) *' (g*(NBag1))).m = Sum r &
for k be Element of NAT st k in dom r holds
r.k = (f*(NBag1)).(k-'1) * (g*(NBag1)).(m+1-'k) by POLYNOM3:def 9;
A8: Seg len decomp b = dom decomp b by FINSEQ_1:def 3
.= dom divisors b by PRE_POLY:def 17
.= Seg len divisors b by FINSEQ_1:def 3; then
len decomp b = len divisors b by FINSEQ_1:6; then
A9: len s = (b.0) + 1 by A5,Th15
.= len r by A2,A3,FUNCOP_1:7,A7;
A10: dom decomp b = Seg len decomp b by FINSEQ_1:def 3
.= Seg ((b.0) +1) by A8,Th15;
A11: dom decomp b = Seg len s by A5,FINSEQ_1:def 3
.= dom s by FINSEQ_1:def 3;
for k be Nat st 1 <= k & k <= len s holds s.k = r.k
proof
let k be Nat;
assume A12: 1 <= k & k <= len s; then
A13: k in Seg len s;
A14: k in dom s by A12,FINSEQ_3:25; then
consider b1, b2 being bag of 1 such that
A15: (decomp b)/.k = <*b1, b2*> & s/.k = f.b1*g.b2 by A5;
A16: k in dom decomp b & (decomp b)/.k = <*b1, b2*>
by A13, FINSEQ_1:def 3,A11,A15; then
b1 = (divisors b)/.k by PRE_POLY:70; then
A17: <*b1, b-'b1*> = (decomp b)/.k by A16,PRE_POLY:def 17
.= <*b1, b2*> by A15;
dom decomp b = Seg len divisors b by A8,FINSEQ_1:def 3
.= dom divisors b by FINSEQ_1:def 3
.= dom XFS2FS(F) by Th25; then
A18: k in dom XFS2FS(F) by A13, FINSEQ_1:def 3,A11;
A19: k in Seg ((b.0) +1) by A13, FINSEQ_1:def 3,A11,A10; then
A20: 1 <= k & k <= len F by FINSEQ_1:1;
then reconsider k1 = k-1 as Element of NAT by INT_1:3;
A21: 1 <= k <= (b.0) +1 by A19,FINSEQ_1:1;
k - 1 < k - 0 by XREAL_1:10; then
A22: k - 1 < (b.0) + 1 by A21,XXREAL_0:2; then
A23: k1 in dom(NBag1|Segm((b.0)+1)) by NAT_1:44;
A24: b1 = (divisors b)/.k by PRE_POLY:70,A16
.= (XFS2FS(F))/.k by Th25
.= (XFS2FS(F)).k by A18,PARTFUN1:def 6
.= (NBag1|Segm((b.0)+1)).(k-1) by A20,AFINSQ_1:def 9
.= (NBag1).k1 by A23,FUNCT_1:47 .= 1--> k1 by Def1;
A25: 0 in 1 by CARD_1:49,TARSKI:def 1;
aaa: k -'1 = k -1 by A21,XREAL_0:def 2; then
A26: (b.0) >= k - 1 by A22,NAT_1:13;
A27: (b.0) -' (k -'1) = (b.0) -' (k-1) by A21,XREAL_0:def 2
.= (b.0)-(k-1) by A26,XREAL_1:233
.= (b.0)+1 - k .= (b.0)+1 -' k by A21,XREAL_1:233;
A28: b2 = b-'b1 by A17,FINSEQ_1:77
.= 1 --> ((b.0) -' (b1.0)) by Th7
.= 1 --> ((b.0)+ 1 -' k) by aaa,A27,A25,A24,FUNCOP_1:7;
A29: (f*NBag1).(k-1) = f.((NBag1).k1) by FUNCT_2:15
.= f.b1 by Def1,A24;
A30: (g*NBag1).((b.0)+1-'k) = g.((NBag1).((b.0)+1-'k)) by FUNCT_2:15
.= g.b2 by A28,Def1;
k in dom r by A9,A13,FINSEQ_1:def 3; then
r.k = (f*(NBag1)).(k-'1) * (g*(NBag1)).((b.0)+1-'k) by A4,A7
.= f.b1 * g.b2 by aaa,A29,A30
.= s.k by A14,A15,PARTFUN1:def 6;
hence thesis;
end; then
s = r by A9; then
((f*'g)*(NBag1)).o = Sum r by A6
.= ((f*(NBag1)) *' (g*(NBag1))).o by A7;
hence thesis;
end;
hence thesis;
end;
theorem Th29:
for f,g be Element of Formal-Series(1,R) holds
(BSFSeri(R)).(f*g) = (BSFSeri(R)).f * (BSFSeri(R)).g
proof
let f,g be Element of Formal-Series(1,R);
consider f1 being Series of 1,R such that
A1: f1 = f & (BSFSeri(R)).f = f1*(NBag1) by Def4;
consider g1 being Series of 1,R such that
A2: g1 = g & (BSFSeri(R)).g = g1*(NBag1) by Def4;
consider fg1 being Series of 1,R such that
A3: fg1 = f*g & (BSFSeri(R)).(f*g) = fg1*(NBag1) by Def4;
A4: fg1 = f1 *' g1 by A1,A2,A3,Def3;
(BSFSeri(R)).(f*g) = (f1*(NBag1)) *' (g1*(NBag1)) by A3,A4,Th28
.= (BSFSeri(R)).f * (BSFSeri(R)).g by A1,A2,POLYALG1:def 2;
hence thesis;
end;
theorem Th30:
for R holds (BSFSeri(R)).(1.Formal-Series(1,R)) = 1.(Formal-Series R)
proof
let R;
consider e1 being Series of 1,R such that
A1: e1 = (1.Formal-Series(1,R)) &
(BSFSeri(R)).(1.Formal-Series(1,R)) = e1*(NBag1) by Def4;
e1 = 1_(1,R) by A1,Def3; then
(BSFSeri(R)).(1.Formal-Series(1,R))
= (0_(1,R)+*(EmptyBag 1,1.R))*(NBag1) by A1 .= 1_.(R) by Th23
.= 1.(Formal-Series R) by POLYALG1:def 2;
hence thesis;
end;
registration
let R;
cluster BSFSeri(R) -> additive multiplicative unity-preserving;
coherence by Th27,Th29,Th30;
end;
theorem
for R holds BSFSeri(R) is RingIsomorphism &
Formal-Series R is (Formal-Series(1,R))-isomorphic
proof
let R;
BSFSeri(R) is RingHomomorphism & BSFSeri(R) is isomorphism;
hence thesis by RING_3:def 4;
end;
registration
let R;
cluster Formal-Series R -> (Formal-Series(1,R))-homomorphic
(Formal-Series(1,R))-monomorphic
(Formal-Series(1,R))-isomorphic;
coherence
proof
A1: BSFSeri(R) is linear one-to-one;
hence Formal-Series R is (Formal-Series(1,R))-homomorphic;
thus
Formal-Series R is (Formal-Series(1,R))-monomorphic by A1,RING_3:def 3;
thus
Formal-Series R is (Formal-Series(1,R))-isomorphic by A1,RING_3:def 4;
end;
end;
definition
let R;
func SBFSeri(R) -> Function of Formal-Series R, Formal-Series(1,R) means
:Def5:
for x being object st x in the carrier of Formal-Series R holds
ex x1 being sequence of R st x1 = x & it.x = x1*(BagN1);
existence
proof
defpred P[object,object] means
ex x1 be sequence of R st x1 = $1 & $2 = x1*BagN1;
A1: for x being object st x in the carrier of Formal-Series R
ex y being object st y in the carrier of Formal-Series(1,R) & P[x,y]
proof
let x be object;
assume x in the carrier of Formal-Series R; then
reconsider x1 = x as sequence of R by POLYALG1:def 2;
take y = x1*BagN1;
thus thesis by Def3;
end;
ex g being Function of Formal-Series R, Formal-Series(1,R)
st for x being object st x in the carrier of Formal-Series R holds
P[x,g.x] from FUNCT_2:sch 1(A1); then
consider g being Function of Formal-Series R,Formal-Series(1,R)
such that
A2: for x being object st x in the carrier of Formal-Series R holds
ex x1 being sequence of R st x1 = x & g.x = x1*BagN1;
take g;
thus thesis by A2;
end;
uniqueness
proof
set FS1 = Formal-Series(1,R),
FS = Formal-Series R;
let f,g be Function of FS,FS1 such that
A3: for x be object st x in the carrier of FS holds
ex x1 be sequence of R st x1 = x & f.x = x1*BagN1
and
A4: for x be object st x in the carrier of FS holds
ex x1 be sequence of R st x1 = x & g.x = x1*BagN1;
now
let x be object;
assume
A5: x in the carrier of FS; then
consider x1 be sequence of R such that
A6: x1 = x & f.x = x1*BagN1 by A3;
consider x2 be sequence of R such that
A7: x2 = x & g.x = x2*BagN1 by A4,A5;
thus f.x = g.x by A6,A7;
end;
hence thesis;
end;
end;
theorem Th32:
for R holds (BSFSeri(R))" = SBFSeri(R)
proof
let R;
A1: rng (BSFSeri(R)) = the carrier of Formal-Series R by FUNCT_2:def 3
.= dom SBFSeri(R) by FUNCT_2:def 1;
for o st o in dom ((SBFSeri(R))*(BSFSeri(R))) holds
((SBFSeri(R))*(BSFSeri(R))).o = (id dom(BSFSeri(R))).o
proof
let o;
assume
A2: o in dom ((SBFSeri(R))*(BSFSeri(R))); then
A3: o in dom BSFSeri(R) by FUNCT_2:123;
consider x1 being Series of 1,R such that
A4: x1 = o & (BSFSeri(R)).o = x1*(NBag1) by A2,Def4;
reconsider y = x1*(NBag1) as Element of Formal-Series R
by FUNCT_2:5,A2,A4;
consider y1 being sequence of R such that
A5: y1 = y & (SBFSeri(R)).y = y1*(BagN1) by Def5;
((SBFSeri(R))*(BSFSeri(R))).o = (SBFSeri(R)).(x1*(NBag1))
by A4,A2,FUNCT_2:15
.= (SBFSeri(R)).y .= y1*(BagN1) by A5
.= x1*((NBag1)*(BagN1)) by A5,RELAT_1:36
.= x1 by Th11,FUNCT_2:17 .= (id dom(BSFSeri(R))).o by A3,A4,FUNCT_1:18;
hence thesis;
end; then
(SBFSeri(R))*(BSFSeri(R)) = id dom BSFSeri(R) by FUNCT_2:123;
hence thesis by A1,FUNCT_1:41;
end;
Lm5:
for R holds SBFSeri(R) is one-to-one
proof
let R;
(BSFSeri(R))" is one-to-one;
hence thesis by Th32;
end;
Lm6:
for R holds SBFSeri(R) is onto
proof
let R;
rng((BSFSeri(R))*(SBFSeri(R))) = rng((BSFSeri(R))*(BSFSeri(R))") by Th32
.= rng (BSFSeri(R)) by FUNCT_1:37
.= the carrier of Formal-Series R by FUNCT_2:def 3;
hence thesis by FUNCT_2:22;
end;
registration
let R;
cluster SBFSeri(R) -> one-to-one onto;
coherence by Lm5,Lm6;
end;
theorem Th33:
for R holds SBFSeri(R) is RingHomomorphism
proof
let R;
set P = BSFSeri(R);
set FS1 = Formal-Series(1,R);
set FS = Formal-Series R;
A1: P is onto;
A2: P is additive multiplicative unity-preserving;
A3: for x,y being Element of FS holds
P".(x+y) = P".x + P".y & P".(x*y) = P".x * P".y & P".(1_FS) = 1_FS1
proof
A4: P".(1_FS) = ((P qua Function)").(P.(1_FS1)) by GROUP_1:def 13
.= 1_FS1 by FUNCT_2:26;
let x,y be Element of FS;
consider x9 being object such that
A5: x9 in the carrier of FS1 and
A6: P.(x9) = x by A1,FUNCT_2:11;
reconsider x9 as Element of FS1 by A5;
A7: x9 = ((P qua Function)").(P.(x9)) by FUNCT_2:26
.= P".x by A6;
consider y9 being object such that
A8: y9 in the carrier of FS1 and
A9: P.y9 = y by A1,FUNCT_2:11;
reconsider y9 as Element of FS1 by A8;
A10: y9 = ((P qua Function)").(P.(y9)) by FUNCT_2:26
.= P".y by A9;
A11: P".(x*y) = P".(P.(x9*y9)) by A2,A6,A9
.= ((P qua Function)").(P.(x9*y9))
.= P".x * P".y by A7,A10,FUNCT_2:26;
P".(x+y) = P".(P.(x9+y9)) by A2,A6,A9
.= ((P qua Function)").(P.(x9+y9))
.= P".x + P".y by A7,A10,FUNCT_2:26;
hence thesis by A11,A4;
end;
P" is additive multiplicative unity-preserving by A3;
hence thesis by Th32;
end;
registration
let R;
cluster SBFSeri(R) -> additive multiplicative unity-preserving;
coherence
proof
SBFSeri(R) is linear by Th33;
hence thesis;
end;
end;
theorem
for R holds SBFSeri(R) is RingIsomorphism &
Formal-Series(1,R) is (Formal-Series R)-isomorphic
proof
let R;
SBFSeri(R) is RingHomomorphism & SBFSeri(R) is isomorphism;
hence thesis by RING_3:def 4;
end;
registration
let R;
cluster Formal-Series(1,R) -> (Formal-Series R)-homomorphic
(Formal-Series R)-monomorphic
(Formal-Series R)-isomorphic;
coherence
proof
A1: SBFSeri(R) is linear one-to-one;
hence Formal-Series(1,R) is (Formal-Series R)-homomorphic;
thus
Formal-Series(1,R) is (Formal-Series R)-monomorphic by A1,RING_3:def 3;
SBFSeri(R) is Isomorphism of Formal-Series R,Formal-Series(1,R);
hence Formal-Series(1,R) is (Formal-Series R)-isomorphic by RING_3:def 4;
end;
end;
begin :: Construct Isomorphism Polynom-Ring(1,R) to Polynom-Ring R.
theorem Th35:
Polynom-Ring R is Subring of Formal-Series R
proof
set PR = Polynom-Ring R,
FS = Formal-Series R,
X = [: the carrier of PR, the carrier of PR:],
Y = [: the carrier of FS, the carrier of FS:];
A1: o in the carrier of PR implies o in the carrier of FS
proof
assume o in the carrier of PR; then
o is Polynomial of R by POLYNOM3:def 10;
hence thesis by POLYALG1:def 2;
end;
A2: the carrier of PR c= the carrier of FS by A1;
A3: the addF of PR = (the addF of FS)||(the carrier of PR)
proof
A4: dom (the addF of PR) = X by FUNCT_2:def 1;
dom (the addF of FS) = Y by FUNCT_2:def 1; then
A5: dom (the addF of FS) /\ X = X by XBOOLE_1:28, A2,ZFMISC_1:96;
for o st o in dom (the addF of PR) holds
(the addF of PR).o = (the addF of FS).o
proof
let o;
assume o in dom the addF of PR; then
consider o1,o2 such that
A6: o1 in the carrier of PR & o2 in the carrier of PR &
o = [o1,o2] by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of PR by A6;
reconsider s1 = x, s2 = y as sequence of R by POLYNOM3:def 10;
reconsider x1 = x, y1 = y as Element of the carrier of FS by A1;
(the addF of PR).[x,y] = x + y
.= s1 + s2 by POLYNOM3:def 10
.= x1 + y1 by POLYALG1:def 2 .= (the addF of FS).[x1,y1];
hence thesis by A6;
end;
hence thesis by A4,A5,FUNCT_1:46;
end;
A7: the multF of PR = (the multF of FS)||(the carrier of PR)
proof
A8: dom (the multF of FS) = Y by FUNCT_2:def 1;
A9: dom (the multF of PR) = X by FUNCT_2:def 1;
A10: dom (the multF of FS) /\ X = X by A8,XBOOLE_1:28, A2,ZFMISC_1:96;
for o st o in dom (the multF of PR) holds
(the multF of PR).o = (the multF of FS).o
proof
let o;
assume o in dom the multF of PR; then
consider o1,o2 such that
A11: o1 in the carrier of PR & o2 in the carrier of PR &
o = [o1,o2] by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of PR by A11;
reconsider s1 = x, s2 = y as sequence of R by POLYNOM3:def 10;
reconsider x1 = x, y1 = y as Element of the carrier of FS by A1;
(the multF of PR).[x,y] = x * y .= s1 *' s2 by POLYNOM3:def 10
.= x1 * y1 by POLYALG1:def 2 .= (the multF of FS).[x1,y1];
hence thesis by A11;
end;
hence thesis by A9,A10,FUNCT_1:46;
end;
A12: 0.PR = 0_.(R) by POLYNOM3:def 10 .= 0.FS by POLYALG1:def 2;
1.PR = 1_.(R) by POLYNOM3:def 10 .= 1.FS by POLYALG1:def 2;
hence thesis by A1,TARSKI:def 3,A3,A7,A12,C0SP1:def 3;
end;
theorem
for f1,g1 be sequence of R holds (f1+g1)*(BagN1) = f1*(BagN1) + g1*(BagN1)
proof
let f1,g1 be sequence of R;
A1: dom((f1+g1)*(BagN1)) = Bags 1 by FUNCT_2:def 1;
for o st o in dom((f1+g1)*(BagN1)) holds
((f1+g1)*(BagN1)).o = (f1*(BagN1) + g1*(BagN1)).o
proof
let o;
assume o in dom((f1+g1)*(BagN1)); then
reconsider b = o as Element of Bags 1;
A2: (BagN1).o = b.0 by Def2;
reconsider s1 = f1*(BagN1) as Series of 1,R;
reconsider t1 = g1*(BagN1) as Series of 1,R;
A3: (f1*BagN1).b = f1.(b.0) by A2,FUNCT_2:15;
A4: (g1*BagN1).b = g1.(b.0) by A2,FUNCT_2:15;
((f1+g1)*(BagN1)).o = (f1+g1).(b.0) by A2,FUNCT_2:15
.= f1.(b.0) + g1.(b.0) by NORMSP_1:def 2
.= ((f1*BagN1) + (g1*BagN1)).o by A3,A4,POLYNOM1:15;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th37:
for f be sequence of the carrier of R holds f = (f*(BagN1))*NBag1
proof
let f be sequence of the carrier of R;
(f*(BagN1))*NBag1 = f*(id(NAT)) by Th10,RELAT_1:36 .= f by FUNCT_2:17;
hence thesis;
end;
theorem Th38:
for f be Series of 1,R holds f = (f*(NBag1))*BagN1
proof
let f be Series of 1,R;
(f*(NBag1))*BagN1 = f*(id(Bags 1)) by Th11,RELAT_1:36 .= f by FUNCT_2:17;
hence thesis;
end;
theorem Th39:
for f be sequence of R holds NBag1.:(Support f) = Support (f*BagN1)
proof
let f be sequence of R;
for o holds o in (NBag1).:(Support f) iff o in Support(f*BagN1)
proof
let o;
A1: dom (NBag1) = NAT by FUNCT_2:def 1;
A2: dom (f*BagN1) = Bags 1 by FUNCT_2:def 1;
A3: o in NBag1.:(Support f) implies o in Support(f*BagN1)
proof
assume o in (NBag1).:(Support f); then
consider x be object such that
A4: x in dom (NBag1) & x in Support f & o = (NBag1).x by FUNCT_1:def 6;
A5: o in Bags 1 by A4,FUNCT_2:5;
(f*BagN1).o = ((f*BagN1)*(NBag1)).x by A4,FUNCT_2:15
.= f.x by Th37; then
(f*BagN1).o <> 0.R by A4,POLYNOM1:def 3;
hence thesis by A5, A2,POLYNOM1:def 3;
end;
o in Support(f*BagN1) implies o in NBag1.:(Support f)
proof
assume
A6: o in Support(f*BagN1); then
reconsider b = (BagN1).o as Element of NAT by FUNCT_2:5;
A7: dom f = NAT by FUNCT_2:def 1;
A8: NBag1.b = (id(Bags 1)).o by A6,FUNCT_2:15,Th11 .= o by A6, FUNCT_1:18;
f.b = (f*(BagN1)).o by A6,FUNCT_2:15; then
f.b <> 0.R by A6,POLYNOM1:def 3; then
b in Support f by A7,POLYNOM1:def 3;
hence thesis by A1,A8,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem Th40:
for B be Subset of NAT holds card(B) = card((NBag1).:B)
proof
let B be Subset of NAT;
reconsider F = (NBag1)|B as Function;
A1: rng F = (NBag1).:B by RELAT_1:115;
dom F = B by FUNCT_2:def 1;
hence thesis by CARD_1:5,A1,WELLORD2:def 4;
end;
theorem Th41:
for f be sequence of R holds card (Support f) = card Support(f*BagN1)
proof
let f be sequence of R;
card(Support f) = card(NBag1.:(Support f)) by Th40
.= card(Support(f*BagN1)) by Th39;
hence thesis;
end;
theorem Th42:
for f be Series of 1,R holds BagN1.:(Support f) = Support(f*NBag1)
proof
let f be Series of 1,R;
for o holds o in (BagN1).:(Support f) iff o in Support(f*NBag1)
proof
let o;
A1: dom (BagN1) = Bags 1 by FUNCT_2:def 1;
A2: dom (f*NBag1) = NAT by FUNCT_2:def 1;
A3: o in BagN1.:(Support f) implies o in Support(f*NBag1)
proof
assume o in (BagN1).:(Support f); then
consider x be object such that
A4: x in dom (BagN1) & x in Support f & o = (BagN1).x by FUNCT_1:def 6;
A5: o in NAT by A4,FUNCT_2:5;
(f*NBag1).o = ((f*NBag1)*(BagN1)).x by A4,FUNCT_2:15
.= f.x by Th38; then
(f*NBag1).o <> 0.R by A4,POLYNOM1:def 3;
hence thesis by A5,A2,POLYNOM1:def 3;
end;
o in Support(f*NBag1) implies o in BagN1.:(Support f)
proof
assume
A6: o in Support(f*NBag1); then
reconsider b = (NBag1).o as Element of Bags 1 by FUNCT_2:5;
A7: dom f = Bags 1 by FUNCT_2:def 1;
A8: BagN1.b = (id(NAT)).o by A6,FUNCT_2:15,Th10 .= o by A6,FUNCT_1:18;
f.b = (f*(NBag1)).o by A6,FUNCT_2:15; then
f.b <> 0.R by A6,POLYNOM1:def 3; then
b in Support f by A7,POLYNOM1:def 3;
hence thesis by A1,A8,FUNCT_1:def 6;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem Th43:
for B be Subset of Bags 1 holds card(B) = card((BagN1).:B)
proof
let B be Subset of Bags 1;
reconsider F = (BagN1)|B as Function;
A1: rng F = (BagN1).:B by RELAT_1:115;
dom F = B by FUNCT_2:def 1;
hence thesis by CARD_1:5, A1,WELLORD2:def 4;
end;
theorem Th44:
for f be Series of 1,R holds card (Support f) = card Support(f*NBag1)
proof
let f be Series of 1,R;
card(Support f) = card(BagN1.:(Support f)) by Th43
.= card(Support(f*NBag1)) by Th42;
hence thesis;
end;
Lm7:
for R holds
the carrier of Polynom-Ring(1,R) c= the carrier of Formal-Series(1,R)
proof
let R;
Polynom-Ring(1,R) is Subring of Formal-Series(1,R) by Th21;
hence thesis by C0SP1:def 3;
end;
definition
let R;
func BSPoly(R) -> Function of Polynom-Ring(1,R), Polynom-Ring R equals
(BSFSeri(R))|[#]Polynom-Ring(1,R);
coherence
proof
set PR1 = Polynom-Ring(1,R),
PR = Polynom-Ring R,
FS1 = Formal-Series(1,R),
FS = Formal-Series R;
the carrier of PR1 c= the carrier of FS1 by Lm7; then
[#]PR1 c= dom (BSFSeri(R)) by FUNCT_2:def 1; then
A1: dom((BSFSeri(R))|[#]PR1) = [#]PR1 by RELAT_1:62;
for o st o in the carrier of PR1 holds
((BSFSeri(R))|[#]Polynom-Ring(1,R)).o in the carrier of PR
proof
let o;
assume
A2: o in the carrier of PR1; then
A3: ((BSFSeri(R))|[#]Polynom-Ring(1,R)).o = (BSFSeri(R)).o by FUNCT_1:49;
A4: o is finite-Support Series of 1,R by A2,POLYNOM1:def 11; then
A5: o in the carrier of FS1 by Def3;
reconsider f = o as Element of FS1 by A4,Def3;
consider x1 being Series of 1,R such that
A6: x1 = o & (BSFSeri(R)).o = x1*(NBag1) by A5,Def4;
card (Support x1) = card Support(x1*NBag1) by Th44; then
Support(x1*NBag1) is finite by A4,A6; then
(BSFSeri(R)).o is Polynomial of R by A6, Th2;
hence thesis by A3,POLYNOM3:def 10;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
theorem Th45:
for R holds BSPoly(R) is one-to-one onto
proof
let R;
BSPoly(R) is onto
proof
for o holds o in [#]Polynom-Ring R implies o in rng (BSPoly(R))
proof
let o;
assume
A1: o in [#]Polynom-Ring R; then
A2: o is finite-Support sequence of R by POLYNOM3:def 10;
o in Formal-Series R by A2,POLYALG1:def 2; then
consider f1 being sequence of R such that
A3: f1 = o & (SBFSeri(R)).o = f1*(BagN1) by Def5;
f1 is finite-Support sequence of R by A3,A1,POLYNOM3:def 10; then
A4: Support f1 is finite by Th3;
card (Support f1) = card Support(f1*BagN1) by Th41; then
Support(f1*BagN1) is finite by A4; then
A5: f1*BagN1 is Polynomial of 1,R by POLYNOM1:def 5; then
A6: (SBFSeri(R)).o in Polynom-Ring(1,R) by A3,POLYNOM1:def 11;
set p = (SBFSeri(R)).o;
dom((BSFSeri(R))*(SBFSeri(R)))
= [#]Formal-Series R by FUNCT_2:def 1; then
A7: o in dom((BSFSeri(R))*(SBFSeri(R))) by A2,POLYALG1:def 2; then
o in dom SBFSeri(R) by FUNCT_2:123; then
o in dom((BSFSeri(R))") by Th32; then
A8: o in rng BSFSeri(R) by FUNCT_1:33;
p in Polynom-Ring(1,R) by A5,A3,POLYNOM1:def 11; then
A9: p in dom BSPoly(R) by FUNCT_2:def 1;
(BSPoly(R)).p = (BSFSeri(R)).p by A6,FUNCT_1:49
.= ((BSFSeri(R))*(SBFSeri(R))).o by A7,FUNCT_2:15
.= ((BSFSeri(R))*(BSFSeri(R))").o by Th32 .= o by A8,FUNCT_1:35;
hence thesis by A9,FUNCT_1:def 3;
end; then
[#]Polynom-Ring R c= rng(BSPoly(R));
hence thesis by XBOOLE_0:def 10;
end;
hence thesis;
end;
registration
let R;
cluster BSPoly(R) -> one-to-one onto;
coherence by Th45;
end;
theorem Th46:
for p,q be Element of Polynom-Ring(1,R),
f,g be Element of Formal-Series(1,R) st p = f & q = g holds p+q = f + g
proof
let p,q be Element of Polynom-Ring(1,R),
f,g be Element of Formal-Series(1,R);
assume
A1: p = f & q = g;
reconsider p0 = p,q0 =q as Polynomial of 1,R by POLYNOM1:def 11;
reconsider p1 = p0, q1 = q0 as Series of 1,R;
p+q = p0 + q0 by POLYNOM1:def 11 .= f + g by A1,Def3;
hence thesis;
end;
theorem Th47:
for p,q be Element of Polynom-Ring(1,R),
f,g be Element of Formal-Series(1,R) st p = f & q = g holds p*q = f * g
proof
let p,q be Element of Polynom-Ring(1,R),
f,g be Element of Formal-Series(1,R);
assume
A1: p = f & q = g;
reconsider p0 = p,q0 =q as Polynomial of 1,R by POLYNOM1:def 11;
reconsider p1 = p0, q1 = q0 as Series of 1,R;
p*q = p0 *' q0 by POLYNOM1:def 11 .= f * g by A1,Def3;
hence thesis;
end;
theorem Th48:
for f,g be Element of Polynom-Ring(1,R) holds
(BSPoly(R)).(f+g) = (BSPoly(R)).f + (BSPoly(R)).g
proof
let f,g be Element of Polynom-Ring(1,R);
set FS1 = Formal-Series(1,R),
FS = Formal-Series R;
reconsider PR = Polynom-Ring R as Subring of FS by Th35;
reconsider f0 = f, g0 = g as Element of FS1 by Lm7,TARSKI:def 3;
A1: (BSPoly(R)).f = (BSFSeri(R)).f by FUNCT_1:49;
A2: (BSPoly(R)).g = (BSFSeri(R)).g by FUNCT_1:49;
A3: (BSPoly(R)).(f+g) = (BSFSeri(R)).(f+g) by FUNCT_1:49;
reconsider s = (BSFSeri(R)).f0, t = (BSFSeri(R)).g0 as Element of FS;
reconsider p = (BSPoly(R)).f, q = (BSPoly(R)).g as Element of PR;
(BSPoly(R)).f + (BSPoly(R)).g = p + q .= s + t by A1,A2,Lm3
.= (BSFSeri(R)).(f0+g0) by Th27 .= (BSPoly(R)).(f+g) by Th46,A3;
hence thesis;
end;
theorem Th49:
for f,g be Element of Polynom-Ring(1,R)
holds (BSPoly(R)).(f*g) = (BSPoly(R)).f * (BSPoly(R)).g
proof
let f,g be Element of Polynom-Ring(1,R);
set FS1 = Formal-Series(1,R),
FS = Formal-Series R;
reconsider PR = Polynom-Ring R as Subring of FS by Th35;
reconsider f0 = f, g0 = g as Element of FS1 by Lm7,TARSKI:def 3;
A1: (BSPoly(R)).f = (BSFSeri(R)).f by FUNCT_1:49;
A2: (BSPoly(R)).g = (BSFSeri(R)).g by FUNCT_1:49;
A3: (BSPoly(R)).(f*g) = (BSFSeri(R)).(f*g) by FUNCT_1:49;
reconsider s = (BSFSeri(R)).f0, t = (BSFSeri(R)).g0 as Element of FS;
reconsider p = (BSPoly(R)).f, q = (BSPoly(R)).g as Element of PR;
(BSPoly(R)).f * (BSPoly(R)).g = p * q .= s * t by A1,A2,Lm3
.= (BSFSeri(R)).(f0*g0) by Th29 .= (BSPoly(R)).(f*g) by Th47,A3;
hence thesis;
end;
theorem Th50:
for R holds (BSPoly(R)).(1.Polynom-Ring(1,R)) = 1.(Polynom-Ring R)
proof
let R;
set FS = Formal-Series R;
reconsider PR = Polynom-Ring R as Subring of FS by Th35;
A1: 1.PR = 1_.(R) by POLYNOM3:def 10 .= 1.FS by POLYALG1:def 2;
1.Formal-Series(1,R) = 1_(1,R) by Def3
.= 1.Polynom-Ring(1,R) by POLYNOM1:def 11; then
(BSPoly(R)).(1.Polynom-Ring(1,R))
= (BSFSeri(R)).(1.Formal-Series(1,R)) by FUNCT_1:49
.= 1.Polynom-Ring R by A1,Th30;
hence thesis;
end;
registration
let R;
cluster BSPoly(R) -> additive multiplicative unity-preserving;
coherence by Th48,Th49,Th50;
end;
theorem
for R holds BSPoly(R) is RingIsomorphism &
Polynom-Ring R is (Polynom-Ring(1,R))-isomorphic
proof
let R;
BSPoly(R) is RingHomomorphism & BSPoly(R) is isomorphism;
hence thesis by RING_3:def 4;
end;
registration
let R;
cluster Polynom-Ring R -> (Polynom-Ring(1,R))-homomorphic
(Polynom-Ring(1,R))-monomorphic
(Polynom-Ring(1,R))-isomorphic;
coherence
proof
A1: BSPoly(R) is linear one-to-one;
hence Polynom-Ring R is (Polynom-Ring(1,R))-homomorphic;
thus
Polynom-Ring R is (Polynom-Ring(1,R))-monomorphic by A1,RING_3:def 3;
thus
Polynom-Ring R is (Polynom-Ring(1,R))-isomorphic by A1,RING_3:def 4;
end;
end;