![]() |
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 21682 | . 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 7546 | 1 β’ Rel dom mPwSer |
Colors of variables: wff setvar class |
Syntax hints: β wcel 2105 {crab 3431 Vcvv 3473 β¦csb 3893 βͺ cun 3946 {csn 4628 {ctp 4632 β¨cop 4634 class class class wbr 5148 β¦ cmpt 5231 Γ cxp 5674 β‘ccnv 5675 dom cdm 5676 βΎ cres 5678 β cima 5679 Rel wrel 5681 βcfv 6543 (class class class)co 7412 β cmpo 7414 βf cof 7671 βr cofr 7672 βm cmap 8823 Fincfn 8942 β€ cle 11254 β cmin 11449 βcn 12217 β0cn0 12477 ndxcnx 17131 Basecbs 17149 +gcplusg 17202 .rcmulr 17203 Scalarcsca 17205 Β·π cvsca 17206 TopSetcts 17208 TopOpenctopn 17372 βtcpt 17389 Ξ£g cgsu 17391 mPwSer cmps 21677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-dm 5686 df-oprab 7416 df-mpo 7417 df-psr 21682 |
This theorem is referenced by: psrbas 21717 psrelbas 21718 psrplusg 21720 psraddcl 21722 psrmulr 21723 psrmulcllem 21726 psrvscafval 21729 psrvscacl 21732 resspsrbas 21755 resspsradd 21756 resspsrmul 21757 mplval 21768 opsrle 21822 opsrbaslem 21824 opsrbaslemOLD 21825 psrbaspropd 21978 psropprmul 21981 |
Copyright terms: Public domain | W3C validator |