Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-psr Structured version   Visualization version   GIF version

Definition df-psr 20598
 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 ↦ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ 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
StepHypRef Expression
1 cmps 20593 . 2 class mPwSer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3441 . . 3 class V
5 vd . . . 4 setvar 𝑑
6 vh . . . . . . . . 9 setvar
76cv 1537 . . . . . . . 8 class
87ccnv 5518 . . . . . . 7 class
9 cn 11627 . . . . . . 7 class
108, 9cima 5522 . . . . . 6 class ( “ ℕ)
11 cfn 8494 . . . . . 6 class Fin
1210, 11wcel 2111 . . . . 5 wff ( “ ℕ) ∈ Fin
13 cn0 11887 . . . . . 6 class 0
142cv 1537 . . . . . 6 class 𝑖
15 cmap 8391 . . . . . 6 class m
1613, 14, 15co 7135 . . . . 5 class (ℕ0m 𝑖)
1712, 6, 16crab 3110 . . . 4 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
18 vb . . . . 5 setvar 𝑏
193cv 1537 . . . . . . 7 class 𝑟
20 cbs 16477 . . . . . . 7 class Base
2119, 20cfv 6324 . . . . . 6 class (Base‘𝑟)
225cv 1537 . . . . . 6 class 𝑑
2321, 22, 15co 7135 . . . . 5 class ((Base‘𝑟) ↑m 𝑑)
24 cnx 16474 . . . . . . . . 9 class ndx
2524, 20cfv 6324 . . . . . . . 8 class (Base‘ndx)
2618cv 1537 . . . . . . . 8 class 𝑏
2725, 26cop 4531 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
28 cplusg 16559 . . . . . . . . 9 class +g
2924, 28cfv 6324 . . . . . . . 8 class (+g‘ndx)
3019, 28cfv 6324 . . . . . . . . . 10 class (+g𝑟)
3130cof 7388 . . . . . . . . 9 class f (+g𝑟)
3226, 26cxp 5517 . . . . . . . . 9 class (𝑏 × 𝑏)
3331, 32cres 5521 . . . . . . . 8 class ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))
3429, 33cop 4531 . . . . . . 7 class ⟨(+g‘ndx), ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))⟩
35 cmulr 16560 . . . . . . . . 9 class .r
3624, 35cfv 6324 . . . . . . . 8 class (.r‘ndx)
37 vf . . . . . . . . 9 setvar 𝑓
38 vg . . . . . . . . 9 setvar 𝑔
39 vk . . . . . . . . . 10 setvar 𝑘
40 vx . . . . . . . . . . . 12 setvar 𝑥
41 vy . . . . . . . . . . . . . . 15 setvar 𝑦
4241cv 1537 . . . . . . . . . . . . . 14 class 𝑦
4339cv 1537 . . . . . . . . . . . . . 14 class 𝑘
44 cle 10667 . . . . . . . . . . . . . . 15 class
4544cofr 7389 . . . . . . . . . . . . . 14 class r
4642, 43, 45wbr 5030 . . . . . . . . . . . . 13 wff 𝑦r𝑘
4746, 41, 22crab 3110 . . . . . . . . . . . 12 class {𝑦𝑑𝑦r𝑘}
4840cv 1537 . . . . . . . . . . . . . 14 class 𝑥
4937cv 1537 . . . . . . . . . . . . . 14 class 𝑓
5048, 49cfv 6324 . . . . . . . . . . . . 13 class (𝑓𝑥)
51 cmin 10861 . . . . . . . . . . . . . . . 16 class
5251cof 7388 . . . . . . . . . . . . . . 15 class f
5343, 48, 52co 7135 . . . . . . . . . . . . . 14 class (𝑘f𝑥)
5438cv 1537 . . . . . . . . . . . . . 14 class 𝑔
5553, 54cfv 6324 . . . . . . . . . . . . 13 class (𝑔‘(𝑘f𝑥))
5619, 35cfv 6324 . . . . . . . . . . . . 13 class (.r𝑟)
5750, 55, 56co 7135 . . . . . . . . . . . 12 class ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))
5840, 47, 57cmpt 5110 . . . . . . . . . . 11 class (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥))))
59 cgsu 16708 . . . . . . . . . . 11 class Σg
6019, 58, 59co 7135 . . . . . . . . . 10 class (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))
6139, 22, 60cmpt 5110 . . . . . . . . 9 class (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥))))))
6237, 38, 26, 26, 61cmpo 7137 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))
6336, 62cop 4531 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))⟩
6427, 34, 63ctp 4529 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))⟩}
65 csca 16562 . . . . . . . . 9 class Scalar
6624, 65cfv 6324 . . . . . . . 8 class (Scalar‘ndx)
6766, 19cop 4531 . . . . . . 7 class ⟨(Scalar‘ndx), 𝑟
68 cvsca 16563 . . . . . . . . 9 class ·𝑠
6924, 68cfv 6324 . . . . . . . 8 class ( ·𝑠 ‘ndx)
7048csn 4525 . . . . . . . . . . 11 class {𝑥}
7122, 70cxp 5517 . . . . . . . . . 10 class (𝑑 × {𝑥})
7256cof 7388 . . . . . . . . . 10 class f (.r𝑟)
7371, 49, 72co 7135 . . . . . . . . 9 class ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓)
7440, 37, 21, 26, 73cmpo 7137 . . . . . . . 8 class (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))
7569, 74cop 4531 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))⟩
76 cts 16565 . . . . . . . . 9 class TopSet
7724, 76cfv 6324 . . . . . . . 8 class (TopSet‘ndx)
78 ctopn 16689 . . . . . . . . . . . 12 class TopOpen
7919, 78cfv 6324 . . . . . . . . . . 11 class (TopOpen‘𝑟)
8079csn 4525 . . . . . . . . . 10 class {(TopOpen‘𝑟)}
8122, 80cxp 5517 . . . . . . . . 9 class (𝑑 × {(TopOpen‘𝑟)})
82 cpt 16706 . . . . . . . . 9 class t
8381, 82cfv 6324 . . . . . . . 8 class (∏t‘(𝑑 × {(TopOpen‘𝑟)}))
8477, 83cop 4531 . . . . . . 7 class ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩
8567, 75, 84ctp 4529 . . . . . 6 class {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}
8664, 85cun 3879 . . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
8718, 23, 86csb 3828 . . . 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‘𝑟)}))⟩})
885, 17, 87csb 3828 . . 3 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ 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‘𝑟)}))⟩})
892, 3, 4, 4, 88cmpo 7137 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ 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‘𝑟)}))⟩}))
901, 89wceq 1538 1 wff mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ 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‘𝑟)}))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  reldmpsr  20603  psrval  20604
 Copyright terms: Public domain W3C validator