MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmpsr Structured version   Visualization version   GIF version

Theorem reldmpsr 21686
Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
reldmpsr Rel dom mPwSer

Proof of Theorem reldmpsr
Dummy variables β„Ž 𝑖 π‘Ÿ 𝑦 𝑏 𝑑 𝑓 𝑔 π‘˜ π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef 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β€˜π‘Ÿ)}))⟩}))
21reldmmpo 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