![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldmpsr | Structured version Visualization version GIF version |
Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
Ref | Expression |
---|---|
reldmpsr | ⊢ Rel dom mPwSer |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-psr 21902 | . 2 ⊢ 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‘𝑟)}))〉})) | |
2 | 1 | reldmmpo 7552 | 1 ⊢ Rel dom mPwSer |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 {crab 3419 Vcvv 3462 ⦋csb 3891 ∪ cun 3944 {csn 4623 {ctp 4627 〈cop 4629 class class class wbr 5145 ↦ cmpt 5228 × cxp 5672 ◡ccnv 5673 dom cdm 5674 ↾ cres 5676 “ cima 5677 Rel wrel 5679 ‘cfv 6546 (class class class)co 7416 ∈ cmpo 7418 ∘f cof 7680 ∘r cofr 7681 ↑m cmap 8847 Fincfn 8966 ≤ cle 11290 − cmin 11485 ℕcn 12258 ℕ0cn0 12518 ndxcnx 17190 Basecbs 17208 +gcplusg 17261 .rcmulr 17262 Scalarcsca 17264 ·𝑠 cvsca 17265 TopSetcts 17267 TopOpenctopn 17431 ∏tcpt 17448 Σg cgsu 17450 mPwSer cmps 21897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5296 ax-nul 5303 ax-pr 5425 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-ss 3963 df-nul 4323 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-br 5146 df-opab 5208 df-xp 5680 df-rel 5681 df-dm 5684 df-oprab 7420 df-mpo 7421 df-psr 21902 |
This theorem is referenced by: psrbas 21938 psrelbas 21939 psrplusg 21941 psraddcl 21943 psraddclOLD 21944 psrmulr 21947 psrmulcllem 21950 psrvscafval 21953 psrvscacl 21956 resspsrbas 21979 resspsradd 21980 resspsrmul 21981 mplval 21994 opsrle 22050 opsrbaslem 22052 opsrbaslemOLD 22053 psrbaspropd 22220 psropprmul 22223 mhmcopsr 42239 |
Copyright terms: Public domain | W3C validator |