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 21461
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 21456 . 2 class mPwSer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar π‘Ÿ
4 cvv 3474 . . 3 class V
5 vd . . . 4 setvar 𝑑
6 vh . . . . . . . . 9 setvar β„Ž
76cv 1540 . . . . . . . 8 class β„Ž
87ccnv 5675 . . . . . . 7 class β—‘β„Ž
9 cn 12211 . . . . . . 7 class β„•
108, 9cima 5679 . . . . . 6 class (β—‘β„Ž β€œ β„•)
11 cfn 8938 . . . . . 6 class Fin
1210, 11wcel 2106 . . . . 5 wff (β—‘β„Ž β€œ β„•) ∈ Fin
13 cn0 12471 . . . . . 6 class β„•0
142cv 1540 . . . . . 6 class 𝑖
15 cmap 8819 . . . . . 6 class ↑m
1613, 14, 15co 7408 . . . . 5 class (β„•0 ↑m 𝑖)
1712, 6, 16crab 3432 . . . 4 class {β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin}
18 vb . . . . 5 setvar 𝑏
193cv 1540 . . . . . . 7 class π‘Ÿ
20 cbs 17143 . . . . . . 7 class Base
2119, 20cfv 6543 . . . . . 6 class (Baseβ€˜π‘Ÿ)
225cv 1540 . . . . . 6 class 𝑑
2321, 22, 15co 7408 . . . . 5 class ((Baseβ€˜π‘Ÿ) ↑m 𝑑)
24 cnx 17125 . . . . . . . . 9 class ndx
2524, 20cfv 6543 . . . . . . . 8 class (Baseβ€˜ndx)
2618cv 1540 . . . . . . . 8 class 𝑏
2725, 26cop 4634 . . . . . . 7 class ⟨(Baseβ€˜ndx), π‘βŸ©
28 cplusg 17196 . . . . . . . . 9 class +g
2924, 28cfv 6543 . . . . . . . 8 class (+gβ€˜ndx)
3019, 28cfv 6543 . . . . . . . . . 10 class (+gβ€˜π‘Ÿ)
3130cof 7667 . . . . . . . . 9 class ∘f (+gβ€˜π‘Ÿ)
3226, 26cxp 5674 . . . . . . . . 9 class (𝑏 Γ— 𝑏)
3331, 32cres 5678 . . . . . . . 8 class ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))
3429, 33cop 4634 . . . . . . 7 class ⟨(+gβ€˜ndx), ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))⟩
35 cmulr 17197 . . . . . . . . 9 class .r
3624, 35cfv 6543 . . . . . . . 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 1540 . . . . . . . . . . . . . 14 class 𝑦
4339cv 1540 . . . . . . . . . . . . . 14 class π‘˜
44 cle 11248 . . . . . . . . . . . . . . 15 class ≀
4544cofr 7668 . . . . . . . . . . . . . 14 class ∘r ≀
4642, 43, 45wbr 5148 . . . . . . . . . . . . 13 wff 𝑦 ∘r ≀ π‘˜
4746, 41, 22crab 3432 . . . . . . . . . . . 12 class {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜}
4840cv 1540 . . . . . . . . . . . . . 14 class π‘₯
4937cv 1540 . . . . . . . . . . . . . 14 class 𝑓
5048, 49cfv 6543 . . . . . . . . . . . . 13 class (π‘“β€˜π‘₯)
51 cmin 11443 . . . . . . . . . . . . . . . 16 class βˆ’
5251cof 7667 . . . . . . . . . . . . . . 15 class ∘f βˆ’
5343, 48, 52co 7408 . . . . . . . . . . . . . 14 class (π‘˜ ∘f βˆ’ π‘₯)
5438cv 1540 . . . . . . . . . . . . . 14 class 𝑔
5553, 54cfv 6543 . . . . . . . . . . . . 13 class (π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))
5619, 35cfv 6543 . . . . . . . . . . . . 13 class (.rβ€˜π‘Ÿ)
5750, 55, 56co 7408 . . . . . . . . . . . 12 class ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))
5840, 47, 57cmpt 5231 . . . . . . . . . . 11 class (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))))
59 cgsu 17385 . . . . . . . . . . 11 class Ξ£g
6019, 58, 59co 7408 . . . . . . . . . 10 class (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))
6139, 22, 60cmpt 5231 . . . . . . . . 9 class (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯))))))
6237, 38, 26, 26, 61cmpo 7410 . . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))
6336, 62cop 4634 . . . . . . 7 class ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))⟩
6427, 34, 63ctp 4632 . . . . . 6 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), ( ∘f (+gβ€˜π‘Ÿ) β†Ύ (𝑏 Γ— 𝑏))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (π‘˜ ∈ 𝑑 ↦ (π‘Ÿ Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘“β€˜π‘₯)(.rβ€˜π‘Ÿ)(π‘”β€˜(π‘˜ ∘f βˆ’ π‘₯)))))))⟩}
65 csca 17199 . . . . . . . . 9 class Scalar
6624, 65cfv 6543 . . . . . . . 8 class (Scalarβ€˜ndx)
6766, 19cop 4634 . . . . . . 7 class ⟨(Scalarβ€˜ndx), π‘ŸβŸ©
68 cvsca 17200 . . . . . . . . 9 class ·𝑠
6924, 68cfv 6543 . . . . . . . 8 class ( ·𝑠 β€˜ndx)
7048csn 4628 . . . . . . . . . . 11 class {π‘₯}
7122, 70cxp 5674 . . . . . . . . . 10 class (𝑑 Γ— {π‘₯})
7256cof 7667 . . . . . . . . . 10 class ∘f (.rβ€˜π‘Ÿ)
7371, 49, 72co 7408 . . . . . . . . 9 class ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓)
7440, 37, 21, 26, 73cmpo 7410 . . . . . . . 8 class (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))
7569, 74cop 4634 . . . . . . 7 class ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))⟩
76 cts 17202 . . . . . . . . 9 class TopSet
7724, 76cfv 6543 . . . . . . . 8 class (TopSetβ€˜ndx)
78 ctopn 17366 . . . . . . . . . . . 12 class TopOpen
7919, 78cfv 6543 . . . . . . . . . . 11 class (TopOpenβ€˜π‘Ÿ)
8079csn 4628 . . . . . . . . . 10 class {(TopOpenβ€˜π‘Ÿ)}
8122, 80cxp 5674 . . . . . . . . 9 class (𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)})
82 cpt 17383 . . . . . . . . 9 class ∏t
8381, 82cfv 6543 . . . . . . . 8 class (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))
8477, 83cop 4634 . . . . . . 7 class ⟨(TopSetβ€˜ndx), (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))⟩
8567, 75, 84ctp 4632 . . . . . 6 class {⟨(Scalarβ€˜ndx), π‘ŸβŸ©, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑓 ∈ 𝑏 ↦ ((𝑑 Γ— {π‘₯}) ∘f (.rβ€˜π‘Ÿ)𝑓))⟩, ⟨(TopSetβ€˜ndx), (∏tβ€˜(𝑑 Γ— {(TopOpenβ€˜π‘Ÿ)}))⟩}
8664, 85cun 3946 . . . . 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 3893 . . . 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 3893 . . 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 7410 . 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 1541 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  21466  psrval  21467
  Copyright terms: Public domain W3C validator