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

Theorem reldmprds 17398
Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
Assertion
Ref Expression
reldmprds Rel dom Xs

Proof of Theorem reldmprds
Dummy variables π‘Ž 𝑐 𝑑 𝑒 𝑓 𝑔 β„Ž 𝑠 π‘Ÿ π‘₯ 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-prds 17397 . 2 Xs = (𝑠 ∈ V, π‘Ÿ ∈ V ↦ ⦋Xπ‘₯ ∈ dom π‘Ÿ(Baseβ€˜(π‘Ÿβ€˜π‘₯)) / π‘£β¦Œβ¦‹(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ Xπ‘₯ ∈ dom π‘Ÿ((π‘“β€˜π‘₯)(Hom β€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))) / β„Žβ¦Œ(({⟨(Baseβ€˜ndx), π‘£βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (π‘₯ ∈ dom π‘Ÿ ↦ ((π‘“β€˜π‘₯)(+gβ€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (π‘₯ ∈ dom π‘Ÿ ↦ ((π‘“β€˜π‘₯)(.rβ€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))))⟩} βˆͺ {⟨(Scalarβ€˜ndx), π‘ βŸ©, ⟨( ·𝑠 β€˜ndx), (𝑓 ∈ (Baseβ€˜π‘ ), 𝑔 ∈ 𝑣 ↦ (π‘₯ ∈ dom π‘Ÿ ↦ (𝑓( ·𝑠 β€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))))⟩, ⟨(Β·π‘–β€˜ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Ξ£g (π‘₯ ∈ dom π‘Ÿ ↦ ((π‘“β€˜π‘₯)(Β·π‘–β€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯)))))⟩}) βˆͺ ({⟨(TopSetβ€˜ndx), (∏tβ€˜(TopOpen ∘ π‘Ÿ))⟩, ⟨(leβ€˜ndx), {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑣 ∧ βˆ€π‘₯ ∈ dom π‘Ÿ(π‘“β€˜π‘₯)(leβ€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))}⟩, ⟨(distβ€˜ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (π‘₯ ∈ dom π‘Ÿ ↦ ((π‘“β€˜π‘₯)(distβ€˜(π‘Ÿβ€˜π‘₯))(π‘”β€˜π‘₯))) βˆͺ {0}), ℝ*, < ))⟩} βˆͺ {⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘Ž ∈ (𝑣 Γ— 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd β€˜π‘Ž)β„Žπ‘), 𝑒 ∈ (β„Žβ€˜π‘Ž) ↦ (π‘₯ ∈ dom π‘Ÿ ↦ ((π‘‘β€˜π‘₯)(⟨((1st β€˜π‘Ž)β€˜π‘₯), ((2nd β€˜π‘Ž)β€˜π‘₯)⟩(compβ€˜(π‘Ÿβ€˜π‘₯))(π‘β€˜π‘₯))(π‘’β€˜π‘₯)))))⟩})))
21reldmmpo 7545 1 Rel dom Xs
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 394  βˆ€wral 3059  Vcvv 3472  β¦‹csb 3892   βˆͺ cun 3945   βŠ† wss 3947  {csn 4627  {cpr 4629  {ctp 4631  βŸ¨cop 4633   class class class wbr 5147  {copab 5209   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675  ran crn 5676   ∘ ccom 5679  Rel wrel 5680  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  1st c1st 7975  2nd c2nd 7976  Xcixp 8893  supcsup 9437  0cc0 11112  β„*cxr 11251   < clt 11252  ndxcnx 17130  Basecbs 17148  +gcplusg 17201  .rcmulr 17202  Scalarcsca 17204   ·𝑠 cvsca 17205  Β·π‘–cip 17206  TopSetcts 17207  lecple 17208  distcds 17210  Hom chom 17212  compcco 17213  TopOpenctopn 17371  βˆtcpt 17388   Ξ£g cgsu 17390  Xscprds 17395
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-prds 17397
This theorem is referenced by:  dsmmval  21508  dsmmval2  21510  dsmmbas2  21511  dsmmfi  21512
  Copyright terms: Public domain W3C validator