Definition df-psr 21121

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 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))

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

Detailed syntax breakdown of Definition df-psr

Step	Hyp	Ref	Expression
1		cmps 21116	. 2 class mPwSer
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3433	. . 3 class V
5		vd	. . . 4 setvar 𝑑
6		vh	. . . . . . . . 9 setvar ℎ
7	6	cv 1538	. . . . . . . 8 class ℎ
8	7	ccnv 5589	. . . . . . 7 class ◡ℎ
9		cn 11982	. . . . . . 7 class ℕ
10	8, 9	cima 5593	. . . . . 6 class (◡ℎ “ ℕ)
11		cfn 8742	. . . . . 6 class Fin
12	10, 11	wcel 2107	. . . . 5 wff (◡ℎ “ ℕ) ∈ Fin
13		cn0 12242	. . . . . 6 class ℕ0
14	2	cv 1538	. . . . . 6 class 𝑖
15		cmap 8624	. . . . . 6 class ↑m
16	13, 14, 15	co 7284	. . . . 5 class (ℕ0 ↑m 𝑖)
17	12, 6, 16	crab 3069	. . . 4 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
18		vb	. . . . 5 setvar 𝑏
19	3	cv 1538	. . . . . . 7 class 𝑟
20		cbs 16921	. . . . . . 7 class Base
21	19, 20	cfv 6437	. . . . . 6 class (Base‘𝑟)
22	5	cv 1538	. . . . . 6 class 𝑑
23	21, 22, 15	co 7284	. . . . 5 class ((Base‘𝑟) ↑m 𝑑)
24		cnx 16903	. . . . . . . . 9 class ndx
25	24, 20	cfv 6437	. . . . . . . 8 class (Base‘ndx)
26	18	cv 1538	. . . . . . . 8 class 𝑏
27	25, 26	cop 4568	. . . . . . 7 class ⟨(Base‘ndx), 𝑏⟩
28		cplusg 16971	. . . . . . . . 9 class +g
29	24, 28	cfv 6437	. . . . . . . 8 class (+g‘ndx)
30	19, 28	cfv 6437	. . . . . . . . . 10 class (+g‘𝑟)
31	30	cof 7540	. . . . . . . . 9 class ∘f (+g‘𝑟)
32	26, 26	cxp 5588	. . . . . . . . 9 class (𝑏 × 𝑏)
33	31, 32	cres 5592	. . . . . . . 8 class ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))
34	29, 33	cop 4568	. . . . . . 7 class ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩
35		cmulr 16972	. . . . . . . . 9 class .r
36	24, 35	cfv 6437	. . . . . . . 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 1538	. . . . . . . . . . . . . 14 class 𝑦
43	39	cv 1538	. . . . . . . . . . . . . 14 class 𝑘
44		cle 11019	. . . . . . . . . . . . . . 15 class ≤
45	44	cofr 7541	. . . . . . . . . . . . . 14 class ∘r ≤
46	42, 43, 45	wbr 5075	. . . . . . . . . . . . 13 wff 𝑦 ∘r ≤ 𝑘
47	46, 41, 22	crab 3069	. . . . . . . . . . . 12 class {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘}
48	40	cv 1538	. . . . . . . . . . . . . 14 class 𝑥
49	37	cv 1538	. . . . . . . . . . . . . 14 class 𝑓
50	48, 49	cfv 6437	. . . . . . . . . . . . 13 class (𝑓‘𝑥)
51		cmin 11214	. . . . . . . . . . . . . . . 16 class −
52	51	cof 7540	. . . . . . . . . . . . . . 15 class ∘f −
53	43, 48, 52	co 7284	. . . . . . . . . . . . . 14 class (𝑘 ∘f − 𝑥)
54	38	cv 1538	. . . . . . . . . . . . . 14 class 𝑔
55	53, 54	cfv 6437	. . . . . . . . . . . . 13 class (𝑔‘(𝑘 ∘f − 𝑥))
56	19, 35	cfv 6437	. . . . . . . . . . . . 13 class (.r‘𝑟)
57	50, 55, 56	co 7284	. . . . . . . . . . . 12 class ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))
58	40, 47, 57	cmpt 5158	. . . . . . . . . . 11 class (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))
59		cgsu 17160	. . . . . . . . . . 11 class Σg
60	19, 58, 59	co 7284	. . . . . . . . . 10 class (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))
61	39, 22, 60	cmpt 5158	. . . . . . . . 9 class (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))))
62	37, 38, 26, 26, 61	cmpo 7286	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))
63	36, 62	cop 4568	. . . . . . 7 class ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩
64	27, 34, 63	ctp 4566	. . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩}
65		csca 16974	. . . . . . . . 9 class Scalar
66	24, 65	cfv 6437	. . . . . . . 8 class (Scalar‘ndx)
67	66, 19	cop 4568	. . . . . . 7 class ⟨(Scalar‘ndx), 𝑟⟩
68		cvsca 16975	. . . . . . . . 9 class ·𝑠
69	24, 68	cfv 6437	. . . . . . . 8 class ( ·𝑠 ‘ndx)
70	48	csn 4562	. . . . . . . . . . 11 class {𝑥}
71	22, 70	cxp 5588	. . . . . . . . . 10 class (𝑑 × {𝑥})
72	56	cof 7540	. . . . . . . . . 10 class ∘f (.r‘𝑟)
73	71, 49, 72	co 7284	. . . . . . . . 9 class ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)
74	40, 37, 21, 26, 73	cmpo 7286	. . . . . . . 8 class (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))
75	69, 74	cop 4568	. . . . . . 7 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩
76		cts 16977	. . . . . . . . 9 class TopSet
77	24, 76	cfv 6437	. . . . . . . 8 class (TopSet‘ndx)
78		ctopn 17141	. . . . . . . . . . . 12 class TopOpen
79	19, 78	cfv 6437	. . . . . . . . . . 11 class (TopOpen‘𝑟)
80	79	csn 4562	. . . . . . . . . 10 class {(TopOpen‘𝑟)}
81	22, 80	cxp 5588	. . . . . . . . 9 class (𝑑 × {(TopOpen‘𝑟)})
82		cpt 17158	. . . . . . . . 9 class ∏t
83	81, 82	cfv 6437	. . . . . . . 8 class (∏t‘(𝑑 × {(TopOpen‘𝑟)}))
84	77, 83	cop 4568	. . . . . . 7 class ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩
85	67, 75, 84	ctp 4566	. . . . . 6 class {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}
86	64, 85	cun 3886	. . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
87	18, 23, 86	csb 3833	. . . 4 class ⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
88	5, 17, 87	csb 3833	. . 3 class ⦋{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
89	2, 3, 4, 4, 88	cmpo 7286	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
90	1, 89	wceq 1539	1 wff mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))

This definition is referenced by:  reldmpsr  21126  psrval  21127