![]() |
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 21348 | . 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 7495 | 1 ⊢ Rel dom mPwSer |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 {crab 3405 Vcvv 3446 ⦋csb 3858 ∪ cun 3911 {csn 4591 {ctp 4595 〈cop 4597 class class class wbr 5110 ↦ cmpt 5193 × cxp 5636 ◡ccnv 5637 dom cdm 5638 ↾ cres 5640 “ cima 5641 Rel wrel 5643 ‘cfv 6501 (class class class)co 7362 ∈ cmpo 7364 ∘f cof 7620 ∘r cofr 7621 ↑m cmap 8772 Fincfn 8890 ≤ cle 11199 − cmin 11394 ℕcn 12162 ℕ0cn0 12422 ndxcnx 17076 Basecbs 17094 +gcplusg 17147 .rcmulr 17148 Scalarcsca 17150 ·𝑠 cvsca 17151 TopSetcts 17153 TopOpenctopn 17317 ∏tcpt 17334 Σg cgsu 17336 mPwSer cmps 21343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-xp 5644 df-rel 5645 df-dm 5648 df-oprab 7366 df-mpo 7367 df-psr 21348 |
This theorem is referenced by: psrbas 21383 psrelbas 21384 psrplusg 21386 psraddcl 21388 psrmulr 21389 psrmulcllem 21392 psrvscafval 21395 psrvscacl 21398 resspsrbas 21421 resspsradd 21422 resspsrmul 21423 mplval 21434 opsrle 21485 opsrbaslem 21487 opsrbaslemOLD 21488 psrbaspropd 21643 psropprmul 21646 |
Copyright terms: Public domain | W3C validator |