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

Theorem reldmevls 21653
Description: Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Assertion
Ref Expression
reldmevls Rel dom evalSub

Proof of Theorem reldmevls
Dummy variables 𝑏 𝑓 𝑔 𝑖 π‘Ÿ 𝑠 𝑀 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-evls 21641 . 2 evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Baseβ€˜π‘ ) / π‘β¦Œ(π‘Ÿ ∈ (SubRingβ€˜π‘ ) ↦ ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))))
21reldmmpo 7545 1 Rel dom evalSub
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 396   = wceq 1541  Vcvv 3474  β¦‹csb 3893  {csn 4628   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676   ∘ ccom 5680  Rel wrel 5681  β€˜cfv 6543  β„©crio 7366  (class class class)co 7411   ↑m cmap 8822  Basecbs 17146   β†Ύs cress 17175   ↑s cpws 17394  CRingccrg 20059   RingHom crh 20252  SubRingcsubrg 20319  algSccascl 21413   mVar cmvr 21464   mPoly cmpl 21465   evalSub ces 21639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rab 3433  df-v 3476  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 7415  df-mpo 7416  df-evls 21641
This theorem is referenced by:  mpfrcl  21654  evlval  21664
  Copyright terms: Public domain W3C validator