Metamath Proof Explorer


Theorem msubffval

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubffval.v V = mVR T
msubffval.r R = mREx T
msubffval.s S = mSubst T
msubffval.e E = mEx T
msubffval.o O = mRSubst T
Assertion msubffval T W S = f R 𝑝𝑚 V e E 1 st e O f 2 nd e

Proof

Step Hyp Ref Expression
1 msubffval.v V = mVR T
2 msubffval.r R = mREx T
3 msubffval.s S = mSubst T
4 msubffval.e E = mEx T
5 msubffval.o O = mRSubst T
6 elex T W T V
7 fveq2 t = T mREx t = mREx T
8 7 2 eqtr4di t = T mREx t = R
9 fveq2 t = T mVR t = mVR T
10 9 1 eqtr4di t = T mVR t = V
11 8 10 oveq12d t = T mREx t 𝑝𝑚 mVR t = R 𝑝𝑚 V
12 fveq2 t = T mEx t = mEx T
13 12 4 eqtr4di t = T mEx t = E
14 fveq2 t = T mRSubst t = mRSubst T
15 14 5 eqtr4di t = T mRSubst t = O
16 15 fveq1d t = T mRSubst t f = O f
17 16 fveq1d t = T mRSubst t f 2 nd e = O f 2 nd e
18 17 opeq2d t = T 1 st e mRSubst t f 2 nd e = 1 st e O f 2 nd e
19 13 18 mpteq12dv t = T e mEx t 1 st e mRSubst t f 2 nd e = e E 1 st e O f 2 nd e
20 11 19 mpteq12dv t = T f mREx t 𝑝𝑚 mVR t e mEx t 1 st e mRSubst t f 2 nd e = f R 𝑝𝑚 V e E 1 st e O f 2 nd e
21 df-msub mSubst = t V f mREx t 𝑝𝑚 mVR t e mEx t 1 st e mRSubst t f 2 nd e
22 ovex R 𝑝𝑚 V V
23 22 mptex f R 𝑝𝑚 V e E 1 st e O f 2 nd e V
24 20 21 23 fvmpt T V mSubst T = f R 𝑝𝑚 V e E 1 st e O f 2 nd e
25 3 24 syl5eq T V S = f R 𝑝𝑚 V e E 1 st e O f 2 nd e
26 6 25 syl T W S = f R 𝑝𝑚 V e E 1 st e O f 2 nd e