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 19125
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
StepHypRef Expression
1 cmps 19120 . 2 class mPwSer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3172 . . 3 class V
5 vd . . . 4 setvar 𝑑
6 vh . . . . . . . . 9 setvar
76cv 1473 . . . . . . . 8 class
87ccnv 5026 . . . . . . 7 class
9 cn 10869 . . . . . . 7 class
108, 9cima 5030 . . . . . 6 class ( “ ℕ)
11 cfn 7818 . . . . . 6 class Fin
1210, 11wcel 1976 . . . . 5 wff ( “ ℕ) ∈ Fin
13 cn0 11141 . . . . . 6 class 0
142cv 1473 . . . . . 6 class 𝑖
15 cmap 7721 . . . . . 6 class 𝑚
1613, 14, 15co 6526 . . . . 5 class (ℕ0𝑚 𝑖)
1712, 6, 16crab 2899 . . . 4 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
18 vb . . . . 5 setvar 𝑏
193cv 1473 . . . . . . 7 class 𝑟
20 cbs 15643 . . . . . . 7 class Base
2119, 20cfv 5789 . . . . . 6 class (Base‘𝑟)
225cv 1473 . . . . . 6 class 𝑑
2321, 22, 15co 6526 . . . . 5 class ((Base‘𝑟) ↑𝑚 𝑑)
24 cnx 15640 . . . . . . . . 9 class ndx
2524, 20cfv 5789 . . . . . . . 8 class (Base‘ndx)
2618cv 1473 . . . . . . . 8 class 𝑏
2725, 26cop 4130 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
28 cplusg 15716 . . . . . . . . 9 class +g
2924, 28cfv 5789 . . . . . . . 8 class (+g‘ndx)
3019, 28cfv 5789 . . . . . . . . . 10 class (+g𝑟)
3130cof 6770 . . . . . . . . 9 class 𝑓 (+g𝑟)
3226, 26cxp 5025 . . . . . . . . 9 class (𝑏 × 𝑏)
3331, 32cres 5029 . . . . . . . 8 class ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))
3429, 33cop 4130 . . . . . . 7 class ⟨(+g‘ndx), ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))⟩
35 cmulr 15717 . . . . . . . . 9 class .r
3624, 35cfv 5789 . . . . . . . 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 1473 . . . . . . . . . . . . . 14 class 𝑦
4339cv 1473 . . . . . . . . . . . . . 14 class 𝑘
44 cle 9931 . . . . . . . . . . . . . . 15 class
4544cofr 6771 . . . . . . . . . . . . . 14 class 𝑟
4642, 43, 45wbr 4577 . . . . . . . . . . . . 13 wff 𝑦𝑟𝑘
4746, 41, 22crab 2899 . . . . . . . . . . . 12 class {𝑦𝑑𝑦𝑟𝑘}
4840cv 1473 . . . . . . . . . . . . . 14 class 𝑥
4937cv 1473 . . . . . . . . . . . . . 14 class 𝑓
5048, 49cfv 5789 . . . . . . . . . . . . 13 class (𝑓𝑥)
51 cmin 10117 . . . . . . . . . . . . . . . 16 class
5251cof 6770 . . . . . . . . . . . . . . 15 class 𝑓
5343, 48, 52co 6526 . . . . . . . . . . . . . 14 class (𝑘𝑓𝑥)
5438cv 1473 . . . . . . . . . . . . . 14 class 𝑔
5553, 54cfv 5789 . . . . . . . . . . . . 13 class (𝑔‘(𝑘𝑓𝑥))
5619, 35cfv 5789 . . . . . . . . . . . . 13 class (.r𝑟)
5750, 55, 56co 6526 . . . . . . . . . . . 12 class ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))
5840, 47, 57cmpt 4637 . . . . . . . . . . 11 class (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥))))
59 cgsu 15872 . . . . . . . . . . 11 class Σg
6019, 58, 59co 6526 . . . . . . . . . 10 class (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))
6139, 22, 60cmpt 4637 . . . . . . . . 9 class (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥))))))
6237, 38, 26, 26, 61cmpt2 6528 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))
6336, 62cop 4130 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))⟩
6427, 34, 63ctp 4128 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))⟩}
65 csca 15719 . . . . . . . . 9 class Scalar
6624, 65cfv 5789 . . . . . . . 8 class (Scalar‘ndx)
6766, 19cop 4130 . . . . . . 7 class ⟨(Scalar‘ndx), 𝑟
68 cvsca 15720 . . . . . . . . 9 class ·𝑠
6924, 68cfv 5789 . . . . . . . 8 class ( ·𝑠 ‘ndx)
7048csn 4124 . . . . . . . . . . 11 class {𝑥}
7122, 70cxp 5025 . . . . . . . . . 10 class (𝑑 × {𝑥})
7256cof 6770 . . . . . . . . . 10 class 𝑓 (.r𝑟)
7371, 49, 72co 6526 . . . . . . . . 9 class ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓)
7440, 37, 21, 26, 73cmpt2 6528 . . . . . . . 8 class (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))
7569, 74cop 4130 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))⟩
76 cts 15722 . . . . . . . . 9 class TopSet
7724, 76cfv 5789 . . . . . . . 8 class (TopSet‘ndx)
78 ctopn 15853 . . . . . . . . . . . 12 class TopOpen
7919, 78cfv 5789 . . . . . . . . . . 11 class (TopOpen‘𝑟)
8079csn 4124 . . . . . . . . . 10 class {(TopOpen‘𝑟)}
8122, 80cxp 5025 . . . . . . . . 9 class (𝑑 × {(TopOpen‘𝑟)})
82 cpt 15870 . . . . . . . . 9 class t
8381, 82cfv 5789 . . . . . . . 8 class (∏t‘(𝑑 × {(TopOpen‘𝑟)}))
8477, 83cop 4130 . . . . . . 7 class ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩
8567, 75, 84ctp 4128 . . . . . 6 class {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}
8664, 85cun 3537 . . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
8718, 23, 86csb 3498 . . . 4 class ((Base‘𝑟) ↑𝑚 𝑑) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
885, 17, 87csb 3498 . . 3 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑((Base‘𝑟) ↑𝑚 𝑑) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑘𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦𝑑𝑦𝑟𝑘} ↦ ((𝑓𝑥)(.r𝑟)(𝑔‘(𝑘𝑓𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})
892, 3, 4, 4, 88cmpt2 6528 . 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‘𝑟)}))⟩}))
901, 89wceq 1474 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‘𝑟)}))⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  reldmpsr  19130  psrval  19131
  Copyright terms: Public domain W3C validator