Definition df-psr 15049

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

Assertion

Ref	Expression
df-psr	⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))

Distinct variable group:   𝑏,𝑑,𝑓,𝑔,ℎ,𝑖,𝑘,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-psr

Step	Hyp	Ref	Expression
1		cmps 15047	. 2 class mPwSer
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 2821	. . 3 class V
5		vd	. . . 4 setvar 𝑑
6		vh	. . . . . . . . 9 setvar ℎ
7	6	cv 1401	. . . . . . . 8 class ℎ
8	7	ccnv 4773	. . . . . . 7 class ◡ℎ
9		cn 9305	. . . . . . 7 class ℕ
10	8, 9	cima 4777	. . . . . 6 class (◡ℎ “ ℕ)
11		cfn 7022	. . . . . 6 class Fin
12	10, 11	wcel 2209	. . . . 5 wff (◡ℎ “ ℕ) ∈ Fin
13		cn0 9565	. . . . . 6 class ℕ0
14	2	cv 1401	. . . . . 6 class 𝑖
15		cmap 6922	. . . . . 6 class ↑𝑚
16	13, 14, 15	co 6085	. . . . 5 class (ℕ0 ↑𝑚 𝑖)
17	12, 6, 16	crab 2532	. . . 4 class {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
18		vb	. . . . 5 setvar 𝑏
19	3	cv 1401	. . . . . . 7 class 𝑟
20		cbs 13354	. . . . . . 7 class Base
21	19, 20	cfv 5377	. . . . . 6 class (Base‘𝑟)
22	5	cv 1401	. . . . . 6 class 𝑑
23	21, 22, 15	co 6085	. . . . 5 class ((Base‘𝑟) ↑𝑚 𝑑)
24		cnx 13351	. . . . . . . . 9 class ndx
25	24, 20	cfv 5377	. . . . . . . 8 class (Base‘ndx)
26	18	cv 1401	. . . . . . . 8 class 𝑏
27	25, 26	cop 3712	. . . . . . 7 class ⟨(Base‘ndx), 𝑏⟩
28		cplusg 13433	. . . . . . . . 9 class +g
29	24, 28	cfv 5377	. . . . . . . 8 class (+g‘ndx)
30	19, 28	cfv 5377	. . . . . . . . . 10 class (+g‘𝑟)
31	30	cof 6300	. . . . . . . . 9 class ∘𝑓 (+g‘𝑟)
32	26, 26	cxp 4772	. . . . . . . . 9 class (𝑏 × 𝑏)
33	31, 32	cres 4776	. . . . . . . 8 class ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))
34	29, 33	cop 3712	. . . . . . 7 class ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩
35		cmulr 13434	. . . . . . . . 9 class .r
36	24, 35	cfv 5377	. . . . . . . 8 class (.r‘ndx)
37		vf	. . . . . . . . 9 setvar 𝑓
38		vg	. . . . . . . . 9 setvar 𝑔
39		vk	. . . . . . . . . 10 setvar 𝑘
40		vx	. . . . . . . . . . . 12 setvar 𝑥
41		vy	. . . . . . . . . . . . . . 15 setvar 𝑦
42	41	cv 1401	. . . . . . . . . . . . . 14 class 𝑦
43	39	cv 1401	. . . . . . . . . . . . . 14 class 𝑘
44		cle 8361	. . . . . . . . . . . . . . 15 class ≤
45	44	cofr 6301	. . . . . . . . . . . . . 14 class ∘𝑟 ≤
46	42, 43, 45	wbr 4130	. . . . . . . . . . . . 13 wff 𝑦 ∘𝑟 ≤ 𝑘
47	46, 41, 22	crab 2532	. . . . . . . . . . . 12 class {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘}
48	40	cv 1401	. . . . . . . . . . . . . 14 class 𝑥
49	37	cv 1401	. . . . . . . . . . . . . 14 class 𝑓
50	48, 49	cfv 5377	. . . . . . . . . . . . 13 class (𝑓‘𝑥)
51		cmin 8497	. . . . . . . . . . . . . . . 16 class −
52	51	cof 6300	. . . . . . . . . . . . . . 15 class ∘𝑓 −
53	43, 48, 52	co 6085	. . . . . . . . . . . . . 14 class (𝑘 ∘𝑓 − 𝑥)
54	38	cv 1401	. . . . . . . . . . . . . 14 class 𝑔
55	53, 54	cfv 5377	. . . . . . . . . . . . 13 class (𝑔‘(𝑘 ∘𝑓 − 𝑥))
56	19, 35	cfv 5377	. . . . . . . . . . . . 13 class (.r‘𝑟)
57	50, 55, 56	co 6085	. . . . . . . . . . . 12 class ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))
58	40, 47, 57	cmpt 4192	. . . . . . . . . . 11 class (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))
59		cgsu 14152	. . . . . . . . . . 11 class Σg
60	19, 58, 59	co 6085	. . . . . . . . . 10 class (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))
61	39, 22, 60	cmpt 4192	. . . . . . . . 9 class (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))
62	37, 38, 26, 26, 61	cmpo 6087	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))
63	36, 62	cop 3712	. . . . . . 7 class ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩
64	27, 34, 63	ctp 3711	. . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩}
65		csca 13436	. . . . . . . . 9 class Scalar
66	24, 65	cfv 5377	. . . . . . . 8 class (Scalar‘ndx)
67	66, 19	cop 3712	. . . . . . 7 class ⟨(Scalar‘ndx), 𝑟⟩
68		cvsca 13437	. . . . . . . . 9 class ·𝑠
69	24, 68	cfv 5377	. . . . . . . 8 class ( ·𝑠 ‘ndx)
70	48	csn 3709	. . . . . . . . . . 11 class {𝑥}
71	22, 70	cxp 4772	. . . . . . . . . 10 class (𝑑 × {𝑥})
72	56	cof 6300	. . . . . . . . . 10 class ∘𝑓 (.r‘𝑟)
73	71, 49, 72	co 6085	. . . . . . . . 9 class ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓)
74	40, 37, 21, 26, 73	cmpo 6087	. . . . . . . 8 class (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))
75	69, 74	cop 3712	. . . . . . 7 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩
76		cts 13439	. . . . . . . . 9 class TopSet
77	24, 76	cfv 5377	. . . . . . . 8 class (TopSet‘ndx)
78		ctopn 13596	. . . . . . . . . . . 12 class TopOpen
79	19, 78	cfv 5377	. . . . . . . . . . 11 class (TopOpen‘𝑟)
80	79	csn 3709	. . . . . . . . . 10 class {(TopOpen‘𝑟)}
81	22, 80	cxp 4772	. . . . . . . . 9 class (𝑑 × {(TopOpen‘𝑟)})
82		cpt 13611	. . . . . . . . 9 class ∏t
83	81, 82	cfv 5377	. . . . . . . 8 class (∏t‘(𝑑 × {(TopOpen‘𝑟)}))
84	77, 83	cop 3712	. . . . . . 7 class ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩
85	67, 75, 84	ctp 3711	. . . . . 6 class {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}
86	64, 85	cun 3218	. . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
87	18, 23, 86	csb 3147	. . . 4 class ⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
88	5, 17, 87	csb 3147	. . 3 class ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
89	2, 3, 4, 4, 88	cmpo 6087	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
90	1, 89	wceq 1402	1 wff mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))

This definition is used by:  reldmpsr  15051  psrval  15052  fnpsr  15053