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 21462
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
StepHypRef Expression
1 cmps 21457 . 2 class mPwSer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar π‘Ÿ
4 cvv 3475 . . 3 class V
5 vd . . . 4 setvar 𝑑
6 vh . . . . . . . . 9 setvar β„Ž
76cv 1541 . . . . . . . 8 class β„Ž
87ccnv 5676 . . . . . . 7 class β—‘β„Ž
9 cn 12212 . . . . . . 7 class β„•
108, 9cima 5680 . . . . . 6 class (β—‘β„Ž β€œ β„•)
11 cfn 8939 . . . . . 6 class Fin
1210, 11wcel 2107 . . . . 5 wff (β—‘β„Ž β€œ β„•) ∈ Fin
13 cn0 12472 . . . . . 6 class β„•0
142cv 1541 . . . . . 6 class 𝑖
15 cmap 8820 . . . . . 6 class ↑m
1613, 14, 15co 7409 . . . . 5 class (β„•0 ↑m 𝑖)
1712, 6, 16crab 3433 . . . 4 class {β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin}
18 vb . . . . 5 setvar 𝑏
193cv 1541 . . . . . . 7 class π‘Ÿ
20 cbs 17144 . . . . . . 7 class Base
2119, 20cfv 6544 . . . . . 6 class (Baseβ€˜π‘Ÿ)
225cv 1541 . . . . . 6 class 𝑑
2321, 22, 15co 7409 . . . . 5 class ((Baseβ€˜π‘Ÿ) ↑m 𝑑)
24 cnx 17126 . . . . . . . . 9 class ndx
2524, 20cfv 6544 . . . . . . . 8 class (Baseβ€˜ndx)
2618cv 1541 . . . . . . . 8 class 𝑏
2725, 26cop 4635 . . . . . . 7 class ⟨(Baseβ€˜ndx), π‘βŸ©
28 cplusg 17197 . . . . . . . . 9 class +g
2924, 28cfv 6544 . . . . . . . 8 class (+gβ€˜ndx)
3019, 28cfv 6544 . . . . . . . . . 10 class (+gβ€˜π‘Ÿ)
3130cof 7668 . . . . . . . . 9 class ∘f (+gβ€˜π‘Ÿ)
3226, 26cxp 5675 . . . . . . . . 9 class (𝑏 Γ— 𝑏)
3331, 32cres 5679 . . . . . . . 8 class ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))
3429, 33cop 4635 . . . . . . 7 class ⟨(+gβ€˜ndx), ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))⟩
35 cmulr 17198 . . . . . . . . 9 class .r
3624, 35cfv 6544 . . . . . . . 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 1541 . . . . . . . . . . . . . 14 class 𝑦
4339cv 1541 . . . . . . . . . . . . . 14 class π‘˜
44 cle 11249 . . . . . . . . . . . . . . 15 class ≀
4544cofr 7669 . . . . . . . . . . . . . 14 class ∘r ≀
4642, 43, 45wbr 5149 . . . . . . . . . . . . 13 wff 𝑦 ∘r ≀ π‘˜
4746, 41, 22crab 3433 . . . . . . . . . . . 12 class {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜}
4840cv 1541 . . . . . . . . . . . . . 14 class π‘₯
4937cv 1541 . . . . . . . . . . . . . 14 class 𝑓
5048, 49cfv 6544 . . . . . . . . . . . . 13 class (π‘“β€˜π‘₯)
51 cmin 11444 . . . . . . . . . . . . . . . 16 class βˆ’
5251cof 7668 . . . . . . . . . . . . . . 15 class ∘f βˆ’
5343, 48, 52co 7409 . . . . . . . . . . . . . 14 class (π‘˜ ∘f βˆ’ π‘₯)
5438cv 1541 . . . . . . . . . . . . . 14 class 𝑔
5553, 54cfv 6544 . . . . . . . . . . . . 13 class (π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))
5619, 35cfv 6544 . . . . . . . . . . . . 13 class (.rβ€˜π‘Ÿ)
5750, 55, 56co 7409 . . . . . . . . . . . 12 class ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))
5840, 47, 57cmpt 5232 . . . . . . . . . . 11 class (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))))
59 cgsu 17386 . . . . . . . . . . 11 class Ξ£g
6019, 58, 59co 7409 . . . . . . . . . 10 class (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))
6139, 22, 60cmpt 5232 . . . . . . . . 9 class (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))))))
6237, 38, 26, 26, 61cmpo 7411 . . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))
6336, 62cop 4635 . . . . . . 7 class ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))⟩
6427, 34, 63ctp 4633 . . . . . 6 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))⟩}
65 csca 17200 . . . . . . . . 9 class Scalar
6624, 65cfv 6544 . . . . . . . 8 class (Scalarβ€˜ndx)
6766, 19cop 4635 . . . . . . 7 class ⟨(Scalarβ€˜ndx), π‘ŸβŸ©
68 cvsca 17201 . . . . . . . . 9 class ·𝑠
6924, 68cfv 6544 . . . . . . . 8 class ( ·𝑠 β€˜ndx)
7048csn 4629 . . . . . . . . . . 11 class {π‘₯}
7122, 70cxp 5675 . . . . . . . . . 10 class (𝑑 Γ— {π‘₯})
7256cof 7668 . . . . . . . . . 10 class ∘f (.rβ€˜π‘Ÿ)
7371, 49, 72co 7409 . . . . . . . . 9 class ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓)
7440, 37, 21, 26, 73cmpo 7411 . . . . . . . 8 class (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))
7569, 74cop 4635 . . . . . . 7 class ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))⟩
76 cts 17203 . . . . . . . . 9 class TopSet
7724, 76cfv 6544 . . . . . . . 8 class (TopSetβ€˜ndx)
78 ctopn 17367 . . . . . . . . . . . 12 class TopOpen
7919, 78cfv 6544 . . . . . . . . . . 11 class (TopOpenβ€˜π‘Ÿ)
8079csn 4629 . . . . . . . . . 10 class {(TopOpenβ€˜π‘Ÿ)}
8122, 80cxp 5675 . . . . . . . . 9 class (𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)})
82 cpt 17384 . . . . . . . . 9 class ∏t
8381, 82cfv 6544 . . . . . . . 8 class (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))
8477, 83cop 4635 . . . . . . 7 class ⟨(TopSetβ€˜ndx), (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))⟩
8567, 75, 84ctp 4633 . . . . . 6 class {⟨(Scalarβ€˜ndx), π‘ŸβŸ©, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))⟩, ⟨(TopSetβ€˜ndx), (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))⟩}
8664, 85cun 3947 . . . . 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 3894 . . . 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 3894 . . 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β€˜π‘Ÿ)}))⟩})
892, 3, 4, 4, 88cmpo 7411 . 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β€˜π‘Ÿ)}))⟩}))
901, 89wceq 1542 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β€˜π‘Ÿ)}))⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  reldmpsr  21467  psrval  21468
  Copyright terms: Public domain W3C validator