Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  msubffval Structured version   Visualization version   GIF version

Theorem msubffval 33203
Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
msubffval.v 𝑉 = (mVR‘𝑇)
msubffval.r 𝑅 = (mREx‘𝑇)
msubffval.s 𝑆 = (mSubst‘𝑇)
msubffval.e 𝐸 = (mEx‘𝑇)
msubffval.o 𝑂 = (mRSubst‘𝑇)
Assertion
Ref Expression
msubffval (𝑇𝑊𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)))
Distinct variable groups:   𝑒,𝑓,𝐸   𝑒,𝑂,𝑓   𝑅,𝑒,𝑓   𝑇,𝑒,𝑓   𝑒,𝑉,𝑓
Allowed substitution hints:   𝑆(𝑒,𝑓)   𝑊(𝑒,𝑓)

Proof of Theorem msubffval
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 elex 3431 . 2 (𝑇𝑊𝑇 ∈ V)
2 msubffval.s . . 3 𝑆 = (mSubst‘𝑇)
3 fveq2 6722 . . . . . . 7 (𝑡 = 𝑇 → (mREx‘𝑡) = (mREx‘𝑇))
4 msubffval.r . . . . . . 7 𝑅 = (mREx‘𝑇)
53, 4eqtr4di 2796 . . . . . 6 (𝑡 = 𝑇 → (mREx‘𝑡) = 𝑅)
6 fveq2 6722 . . . . . . 7 (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
7 msubffval.v . . . . . . 7 𝑉 = (mVR‘𝑇)
86, 7eqtr4di 2796 . . . . . 6 (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
95, 8oveq12d 7236 . . . . 5 (𝑡 = 𝑇 → ((mREx‘𝑡) ↑pm (mVR‘𝑡)) = (𝑅pm 𝑉))
10 fveq2 6722 . . . . . . 7 (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
11 msubffval.e . . . . . . 7 𝐸 = (mEx‘𝑇)
1210, 11eqtr4di 2796 . . . . . 6 (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
13 fveq2 6722 . . . . . . . . . 10 (𝑡 = 𝑇 → (mRSubst‘𝑡) = (mRSubst‘𝑇))
14 msubffval.o . . . . . . . . . 10 𝑂 = (mRSubst‘𝑇)
1513, 14eqtr4di 2796 . . . . . . . . 9 (𝑡 = 𝑇 → (mRSubst‘𝑡) = 𝑂)
1615fveq1d 6724 . . . . . . . 8 (𝑡 = 𝑇 → ((mRSubst‘𝑡)‘𝑓) = (𝑂𝑓))
1716fveq1d 6724 . . . . . . 7 (𝑡 = 𝑇 → (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒)) = ((𝑂𝑓)‘(2nd𝑒)))
1817opeq2d 4796 . . . . . 6 (𝑡 = 𝑇 → ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩ = ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)
1912, 18mpteq12dv 5145 . . . . 5 (𝑡 = 𝑇 → (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩) = (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩))
209, 19mpteq12dv 5145 . . . 4 (𝑡 = 𝑇 → (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩)) = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)))
21 df-msub 33171 . . . 4 mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩)))
22 ovex 7251 . . . . 5 (𝑅pm 𝑉) ∈ V
2322mptex 7044 . . . 4 (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)) ∈ V
2420, 21, 23fvmpt 6823 . . 3 (𝑇 ∈ V → (mSubst‘𝑇) = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)))
252, 24syl5eq 2790 . 2 (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)))
261, 25syl 17 1 (𝑇𝑊𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝐸 ↦ ⟨(1st𝑒), ((𝑂𝑓)‘(2nd𝑒))⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2110  Vcvv 3413  cop 4552  cmpt 5140  cfv 6385  (class class class)co 7218  1st c1st 7764  2nd c2nd 7765  pm cpm 8514  mVRcmvar 33141  mRExcmrex 33146  mExcmex 33147  mRSubstcmrsub 33150  mSubstcmsub 33151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pr 5327
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-ov 7221  df-msub 33171
This theorem is referenced by:  msubfval  33204  elmsubrn  33208  msubrn  33209  msubff  33210
  Copyright terms: Public domain W3C validator