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 = ( mCN ` T )
	mrsubffval.v	|- V = ( mVR ` T )
	mrsubffval.r	|- R = ( mREx ` T )
	mrsubffval.s	|- S = ( mRSubst ` T )
	mrsubffval.g	|- G = ( freeMnd ` ( C u. V ) )
Assertion	mrsubval	|- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> ( ( S ` F ) ` X ) = ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) ) )

Proof

Step	Hyp	Ref	Expression
1		mrsubffval.c	|- C = ( mCN ` T )
2		mrsubffval.v	|- V = ( mVR ` T )
3		mrsubffval.r	|- R = ( mREx ` T )
4		mrsubffval.s	|- S = ( mRSubst ` T )
5		mrsubffval.g	|- G = ( freeMnd ` ( C u. V ) )
6	1 2 3 4 5	mrsubfval	|- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
7	6	3adant3	|- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> ( S ` F ) = ( e e. R |-> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
8		simpr	|- ( ( ( F : A --> R /\ A C_ V /\ X e. R ) /\ e = X ) -> e = X )
9	8	coeq2d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. R ) /\ e = X ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) = ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) )
10	9	oveq2d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. R ) /\ e = X ) -> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) = ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) ) )
11		simp3	|- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> X e. R )
12		ovexd	|- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) ) e. _V )
13	7 10 11 12	fvmptd	|- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> ( ( S ` F ) ` X ) = ( G gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) ) )