|   | 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 21930 | . 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 7568 | 1 ⊢ Rel dom mPwSer | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2107 {crab 3435 Vcvv 3479 ⦋csb 3898 ∪ cun 3948 {csn 4625 {ctp 4629 〈cop 4631 class class class wbr 5142 ↦ cmpt 5224 × cxp 5682 ◡ccnv 5683 dom cdm 5684 ↾ cres 5686 “ cima 5687 Rel wrel 5689 ‘cfv 6560 (class class class)co 7432 ∈ cmpo 7434 ∘f cof 7696 ∘r cofr 7697 ↑m cmap 8867 Fincfn 8986 ≤ cle 11297 − cmin 11493 ℕcn 12267 ℕ0cn0 12528 ndxcnx 17231 Basecbs 17248 +gcplusg 17298 .rcmulr 17299 Scalarcsca 17301 ·𝑠 cvsca 17302 TopSetcts 17304 TopOpenctopn 17467 ∏tcpt 17484 Σg cgsu 17486 mPwSer cmps 21925 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 df-opab 5205 df-xp 5690 df-rel 5691 df-dm 5694 df-oprab 7436 df-mpo 7437 df-psr 21930 | 
| This theorem is referenced by: psrbas 21954 psrelbas 21955 psrplusg 21957 psraddcl 21959 psraddclOLD 21960 psrmulr 21963 psrmulcllem 21966 psrvscafval 21969 psrvscacl 21972 resspsrbas 21995 resspsradd 21996 resspsrmul 21997 mplval 22010 opsrle 22066 opsrbaslem 22068 opsrbaslemOLD 22069 psdval 22164 psdcl 22166 psdadd 22168 psdvsca 22169 psdmul 22171 psdpw 22175 psrbaspropd 22237 psropprmul 22240 mhmcopsr 42564 | 
| Copyright terms: Public domain | W3C validator |