Definition df-psr

Description: Define the algebra of power series over the index set i and with coefficients from the ring r . (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	df-psr	$$⊢\mathrm{mPwSer}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d⦌⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmps	$$class\mathrm{mPwSer}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vh	$$setvarh$$
5		cn0	$$class{\mathbb{N}}_0$$
6		cmap	$$class{\uparrow }_{𝑚}$$
7	1	cv	$$setvari$$
8	5 7 6	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
9	4	cv	$$setvarh$$
10	9	ccnv	$$class{h}^{-1}$$
11		cn	$$class\mathbb{N}$$
12	10 11	cima	$$class{h}^{-1}\left[\mathbb{N}\right]$$
13		cfn	$$class\mathrm{Fin}$$
14	12 13	wcel	$$wff{h}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
15	14 4 8	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
16		vd	$$setvard$$
17		cbs	$$class\mathrm{Base}$$
18	3	cv	$$setvarr$$
19	18 17	cfv	$$class{\mathrm{Base}}_r$$
20	16	cv	$$setvard$$
21	19 20 6	co	$$class\left({{\mathrm{Base}}_r}^d\right)$$
22		vb	$$setvarb$$
23		cnx	$$class\mathrm{ndx}$$
24	23 17	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
25	22	cv	$$setvarb$$
26	24 25	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
27		cplusg	$$class{+}_{𝑔}$$
28	23 27	cfv	$$class{+}_{\mathrm{ndx}}$$
29	18 27	cfv	$$class{+}_r$$
30	29	cof	$$class{\circ }_f{+}_r$$
31	25 25	cxp	$$class\left(b\times b\right)$$
32	30 31	cres	$$class\left({{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}\right)$$
33	28 32	cop	$$class⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩$$
34		cmulr	$$class{\cdot }_{𝑟}$$
35	23 34	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
36		vf	$$setvarf$$
37		vg	$$setvarg$$
38		vk	$$setvark$$
39		cgsu	$$class{\Sigma }_{𝑔}$$
40		vx	$$setvarx$$
41		vy	$$setvary$$
42	41	cv	$$setvary$$
43		cle	$$class\le$$
44	43	cofr	$$class{\circ }_r\le$$
45	38	cv	$$setvark$$
46	42 45 44	wbr	$$wffy{\le }_{f}k$$
47	46 41 20	crab	$$class\left\{y\in d|y{\le }_{f}k\right\}$$
48	36	cv	$$setvarf$$
49	40	cv	$$setvarx$$
50	49 48	cfv	$$classf\left(x\right)$$
51	18 34	cfv	$$class{\cdot }_r$$
52	37	cv	$$setvarg$$
53		cmin	$$class-$$
54	53	cof	$$class{\circ }_f-$$
55	45 49 54	co	$$class\left(k{-}_{f}x\right)$$
56	55 52	cfv	$$classg\left(k{-}_{f}x\right)$$
57	50 56 51	co	$$class\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)$$
58	40 47 57	cmpt	$$class\left(x\in \left\{y\in d|y{\le }_{f}k\right\}⟼f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)$$
59	18 58 39	co	$$class\left(\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r},\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)$$
60	38 20 59	cmpt	$$class\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)$$
61	36 37 25 25 60	cmpo	$$class\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)$$
62	35 61	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩$$
63	26 33 62	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}$$
64		csca	$$class\mathrm{Scalar}$$
65	23 64	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
66	65 18	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩$$
67		cvsca	$$class{\cdot }_{𝑠}$$
68	23 67	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
69	49	csn	$$class\left\{x\right\}$$
70	20 69	cxp	$$class\left(d\times \left\{x\right\}\right)$$
71	51	cof	$$class{\circ }_f{\cdot }_r$$
72	70 48 71	co	$$class\left(\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)$$
73	40 36 19 25 72	cmpo	$$class\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)$$
74	68 73	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩$$
75		cts	$$class\mathrm{TopSet}$$
76	23 75	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
77		cpt	$$class{\prod }_{𝑡}$$
78		ctopn	$$class\mathrm{TopOpen}$$
79	18 78	cfv	$$class\mathrm{TopOpen}\left(r\right)$$
80	79	csn	$$class\left\{\mathrm{TopOpen}\left(r\right)\right\}$$
81	20 80	cxp	$$class\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)$$
82	81 77	cfv	$$class{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)$$
83	76 82	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩$$
84	66 74 83	ctp	$$class\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}$$
85	63 84	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)$$
86	22 21 85	csb	$$class⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)$$
87	16 15 86	csb	$$class⦋\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d⦌⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)$$
88	1 3 2 2 87	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d⦌⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)\right)$$
89	0 88	wceq	$$wff\mathrm{mPwSer}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d⦌⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)\right)$$