![]() |
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 21681 | . 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 7545 | 1 β’ Rel dom mPwSer |
Colors of variables: wff setvar class |
Syntax hints: β wcel 2104 {crab 3430 Vcvv 3472 β¦csb 3892 βͺ cun 3945 {csn 4627 {ctp 4631 β¨cop 4633 class class class wbr 5147 β¦ cmpt 5230 Γ cxp 5673 β‘ccnv 5674 dom cdm 5675 βΎ cres 5677 β cima 5678 Rel wrel 5680 βcfv 6542 (class class class)co 7411 β cmpo 7413 βf cof 7670 βr cofr 7671 βm cmap 8822 Fincfn 8941 β€ cle 11253 β cmin 11448 βcn 12216 β0cn0 12476 ndxcnx 17130 Basecbs 17148 +gcplusg 17201 .rcmulr 17202 Scalarcsca 17204 Β·π cvsca 17205 TopSetcts 17207 TopOpenctopn 17371 βtcpt 17388 Ξ£g cgsu 17390 mPwSer cmps 21676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-xp 5681 df-rel 5682 df-dm 5685 df-oprab 7415 df-mpo 7416 df-psr 21681 |
This theorem is referenced by: psrbas 21716 psrelbas 21717 psrplusg 21719 psraddcl 21721 psrmulr 21722 psrmulcllem 21725 psrvscafval 21728 psrvscacl 21731 resspsrbas 21754 resspsradd 21755 resspsrmul 21756 mplval 21767 opsrle 21821 opsrbaslem 21823 opsrbaslemOLD 21824 psrbaspropd 21977 psropprmul 21980 |
Copyright terms: Public domain | W3C validator |