![]() |
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 19862 | . 2 ⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪ {〈(Scalar‘ndx), 𝑟〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉})) | |
2 | 1 | reldmmpo 7099 | 1 ⊢ Rel dom mPwSer |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 {crab 3085 Vcvv 3408 ⦋csb 3779 ∪ cun 3820 {csn 4435 {ctp 4439 〈cop 4441 class class class wbr 4925 ↦ cmpt 5004 × cxp 5401 ◡ccnv 5402 dom cdm 5403 ↾ cres 5405 “ cima 5406 Rel wrel 5408 ‘cfv 6185 (class class class)co 6974 ∈ cmpo 6976 ∘𝑓 cof 7223 ∘𝑟 cofr 7224 ↑𝑚 cmap 8204 Fincfn 8304 ≤ cle 10473 − cmin 10668 ℕcn 11437 ℕ0cn0 11705 ndxcnx 16334 Basecbs 16337 +gcplusg 16419 .rcmulr 16420 Scalarcsca 16422 ·𝑠 cvsca 16423 TopSetcts 16425 TopOpenctopn 16549 ∏tcpt 16566 Σg cgsu 16568 mPwSer cmps 19857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-rab 3090 df-v 3410 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4926 df-opab 4988 df-xp 5409 df-rel 5410 df-dm 5413 df-oprab 6978 df-mpo 6979 df-psr 19862 |
This theorem is referenced by: psrbas 19884 psrelbas 19885 psrplusg 19887 psraddcl 19889 psrmulr 19890 psrmulcllem 19893 psrvscafval 19896 psrvscacl 19899 resspsrbas 19921 resspsradd 19922 resspsrmul 19923 mplval 19934 opsrle 19981 opsrbaslem 19983 psrbaspropd 20121 psropprmul 20124 |
Copyright terms: Public domain | W3C validator |