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

Definition df-psr 20868
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 20863 . 2 class mPwSer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3408 . . 3 class V
5 vd . . . 4 setvar 𝑑
6 vh . . . . . . . . 9 setvar
76cv 1542 . . . . . . . 8 class
87ccnv 5550 . . . . . . 7 class
9 cn 11830 . . . . . . 7 class
108, 9cima 5554 . . . . . 6 class ( “ ℕ)
11 cfn 8626 . . . . . 6 class Fin
1210, 11wcel 2110 . . . . 5 wff ( “ ℕ) ∈ Fin
13 cn0 12090 . . . . . 6 class 0
142cv 1542 . . . . . 6 class 𝑖
15 cmap 8508 . . . . . 6 class m
1613, 14, 15co 7213 . . . . 5 class (ℕ0m 𝑖)
1712, 6, 16crab 3065 . . . 4 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
18 vb . . . . 5 setvar 𝑏
193cv 1542 . . . . . . 7 class 𝑟
20 cbs 16760 . . . . . . 7 class Base
2119, 20cfv 6380 . . . . . 6 class (Base‘𝑟)
225cv 1542 . . . . . 6 class 𝑑
2321, 22, 15co 7213 . . . . 5 class ((Base‘𝑟) ↑m 𝑑)
24 cnx 16744 . . . . . . . . 9 class ndx
2524, 20cfv 6380 . . . . . . . 8 class (Base‘ndx)
2618cv 1542 . . . . . . . 8 class 𝑏
2725, 26cop 4547 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
28 cplusg 16802 . . . . . . . . 9 class +g
2924, 28cfv 6380 . . . . . . . 8 class (+g‘ndx)
3019, 28cfv 6380 . . . . . . . . . 10 class (+g𝑟)
3130cof 7467 . . . . . . . . 9 class f (+g𝑟)
3226, 26cxp 5549 . . . . . . . . 9 class (𝑏 × 𝑏)
3331, 32cres 5553 . . . . . . . 8 class ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))
3429, 33cop 4547 . . . . . . 7 class ⟨(+g‘ndx), ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))⟩
35 cmulr 16803 . . . . . . . . 9 class .r
3624, 35cfv 6380 . . . . . . . 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 1542 . . . . . . . . . . . . . 14 class 𝑦
4339cv 1542 . . . . . . . . . . . . . 14 class 𝑘
44 cle 10868 . . . . . . . . . . . . . . 15 class
4544cofr 7468 . . . . . . . . . . . . . 14 class r
4642, 43, 45wbr 5053 . . . . . . . . . . . . 13 wff 𝑦r𝑘
4746, 41, 22crab 3065 . . . . . . . . . . . 12 class {𝑦𝑑𝑦r𝑘}
4840cv 1542 . . . . . . . . . . . . . 14 class 𝑥
4937cv 1542 . . . . . . . . . . . . . 14 class 𝑓
5048, 49cfv 6380 . . . . . . . . . . . . 13 class (𝑓𝑥)
51 cmin 11062 . . . . . . . . . . . . . . . 16 class
5251cof 7467 . . . . . . . . . . . . . . 15 class f
5343, 48, 52co 7213 . . . . . . . . . . . . . 14 class (𝑘f𝑥)
5438cv 1542 . . . . . . . . . . . . . 14 class 𝑔
5553, 54cfv 6380 . . . . . . . . . . . . 13 class (𝑔‘(𝑘f𝑥))
5619, 35cfv 6380 . . . . . . . . . . . . 13 class (.r𝑟)
5750, 55, 56co 7213 . . . . . . . . . . . 12 class ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))
5840, 47, 57cmpt 5135 . . . . . . . . . . 11 class (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥))))
59 cgsu 16945 . . . . . . . . . . 11 class Σg
6019, 58, 59co 7213 . . . . . . . . . 10 class (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))
6139, 22, 60cmpt 5135 . . . . . . . . 9 class (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥))))))
6237, 38, 26, 26, 61cmpo 7215 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))
6336, 62cop 4547 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))⟩
6427, 34, 63ctp 4545 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦r𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘f𝑥)))))))⟩}
65 csca 16805 . . . . . . . . 9 class Scalar
6624, 65cfv 6380 . . . . . . . 8 class (Scalar‘ndx)
6766, 19cop 4547 . . . . . . 7 class ⟨(Scalar‘ndx), 𝑟
68 cvsca 16806 . . . . . . . . 9 class ·𝑠
6924, 68cfv 6380 . . . . . . . 8 class ( ·𝑠 ‘ndx)
7048csn 4541 . . . . . . . . . . 11 class {𝑥}
7122, 70cxp 5549 . . . . . . . . . 10 class (𝑑 × {𝑥})
7256cof 7467 . . . . . . . . . 10 class f (.r𝑟)
7371, 49, 72co 7213 . . . . . . . . 9 class ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓)
7440, 37, 21, 26, 73cmpo 7215 . . . . . . . 8 class (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))
7569, 74cop 4547 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))⟩
76 cts 16808 . . . . . . . . 9 class TopSet
7724, 76cfv 6380 . . . . . . . 8 class (TopSet‘ndx)
78 ctopn 16926 . . . . . . . . . . . 12 class TopOpen
7919, 78cfv 6380 . . . . . . . . . . 11 class (TopOpen‘𝑟)
8079csn 4541 . . . . . . . . . 10 class {(TopOpen‘𝑟)}
8122, 80cxp 5549 . . . . . . . . 9 class (𝑑 × {(TopOpen‘𝑟)})
82 cpt 16943 . . . . . . . . 9 class t
8381, 82cfv 6380 . . . . . . . 8 class (∏t‘(𝑑 × {(TopOpen‘𝑟)}))
8477, 83cop 4547 . . . . . . 7 class ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩
8567, 75, 84ctp 4545 . . . . . 6 class {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}
8664, 85cun 3864 . . . . 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 3811 . . . 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 3811 . . 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 7215 . 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 1543 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  20873  psrval  20874
  Copyright terms: Public domain W3C validator