Theorem mrsubval

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	mrsubval	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\to S\left(F\right)\left(X\right)={\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ X\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	1 2 3 4 5	mrsubfval	$$⊢\left(F:A⟶R\wedge A\subseteq V\right)\to S\left(F\right)=\left(e\in R⟼{\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ e\right)\right)$$
7	6	3adant3	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\to S\left(F\right)=\left(e\in R⟼{\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ e\right)\right)$$
8		simpr	$$⊢\left(\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\wedge e=X\right)\to e=X$$
9	8	coeq2d	$$⊢\left(\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\wedge e=X\right)\to \left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ e=\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ X$$
10	9	oveq2d	$$⊢\left(\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\wedge e=X\right)\to {\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,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 A,F\left(v\right),⟨“v”⟩\right)\right)\circ X\right)$$
11		simp3	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\to X\in R$$
12		ovexd	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\to {\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ X\right)\in \mathrm{V}$$
13	7 10 11 12	fvmptd	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in R\right)\to S\left(F\right)\left(X\right)={\sum }_G\left(\left(v\in \left(C\cup V\right)⟼if\left(v\in A,F\left(v\right),⟨“v”⟩\right)\right)\circ X\right)$$