# Metamath Proof Explorer

## Theorem mrsubffval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c ${⊢}{C}=\mathrm{mCN}\left({T}\right)$
mrsubffval.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
mrsubffval.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
mrsubffval.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
mrsubffval.g ${⊢}{G}=\mathrm{freeMnd}\left({C}\cup {V}\right)$
Assertion mrsubffval ${⊢}{T}\in {W}\to {S}=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 mrsubffval.c ${⊢}{C}=\mathrm{mCN}\left({T}\right)$
2 mrsubffval.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
3 mrsubffval.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
4 mrsubffval.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
5 mrsubffval.g ${⊢}{G}=\mathrm{freeMnd}\left({C}\cup {V}\right)$
6 elex ${⊢}{T}\in {W}\to {T}\in \mathrm{V}$
7 fveq2 ${⊢}{t}={T}\to \mathrm{mREx}\left({t}\right)=\mathrm{mREx}\left({T}\right)$
8 7 3 syl6eqr ${⊢}{t}={T}\to \mathrm{mREx}\left({t}\right)={R}$
9 fveq2 ${⊢}{t}={T}\to \mathrm{mVR}\left({t}\right)=\mathrm{mVR}\left({T}\right)$
10 9 2 syl6eqr ${⊢}{t}={T}\to \mathrm{mVR}\left({t}\right)={V}$
11 8 10 oveq12d ${⊢}{t}={T}\to \mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)={R}{↑}_{𝑝𝑚}{V}$
12 fveq2 ${⊢}{t}={T}\to \mathrm{mCN}\left({t}\right)=\mathrm{mCN}\left({T}\right)$
13 12 1 syl6eqr ${⊢}{t}={T}\to \mathrm{mCN}\left({t}\right)={C}$
14 13 10 uneq12d ${⊢}{t}={T}\to \mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)={C}\cup {V}$
15 14 fveq2d ${⊢}{t}={T}\to \mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)=\mathrm{freeMnd}\left({C}\cup {V}\right)$
16 15 5 syl6eqr ${⊢}{t}={T}\to \mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)={G}$
17 14 mpteq1d ${⊢}{t}={T}\to \left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)=\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)$
18 17 coeq1d ${⊢}{t}={T}\to \left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}=\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}$
19 16 18 oveq12d ${⊢}{t}={T}\to {\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)={\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)$
20 8 19 mpteq12dv ${⊢}{t}={T}\to \left({e}\in \mathrm{mREx}\left({t}\right)⟼{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)=\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)$
21 11 20 mpteq12dv ${⊢}{t}={T}\to \left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mREx}\left({t}\right)⟼{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)$
22 df-mrsub ${⊢}\mathrm{mRSubst}=\left({t}\in \mathrm{V}⟼\left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mREx}\left({t}\right)⟼{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({t}\right)\cup \mathrm{mVR}\left({t}\right)\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)\right)$
23 ovex ${⊢}{R}{↑}_{𝑝𝑚}{V}\in \mathrm{V}$
24 23 mptex ${⊢}\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)\in \mathrm{V}$
25 21 22 24 fvmpt ${⊢}{T}\in \mathrm{V}\to \mathrm{mRSubst}\left({T}\right)=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)$
26 6 25 syl ${⊢}{T}\in {W}\to \mathrm{mRSubst}\left({T}\right)=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)$
27 4 26 syl5eq ${⊢}{T}\in {W}\to {S}=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)⟼\left({e}\in {R}⟼{\sum }_{{G}}\left(\left({v}\in \left({C}\cup {V}\right)⟼if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ {e}\right)\right)\right)$