Theorem mrsubcv

Description: The value of a substituted singleton. (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 )
Assertion	mrsubcv	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( S ` F ) ` <" X "> ) = if ( X e. A , ( F ` X ) , <" 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		simp3	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> X e. ( C u. V ) )
6	5	s1cld	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> <" X "> e. Word ( C u. V ) )
7		elun	|- ( X e. ( C u. V ) <-> ( X e. C \/ X e. V ) )
8		elfvex	|- ( X e. ( mCN ` T ) -> T e. _V )
9	8 1	eleq2s	|- ( X e. C -> T e. _V )
10		elfvex	|- ( X e. ( mVR ` T ) -> T e. _V )
11	10 2	eleq2s	|- ( X e. V -> T e. _V )
12	9 11	jaoi	|- ( ( X e. C \/ X e. V ) -> T e. _V )
13	7 12	sylbi	|- ( X e. ( C u. V ) -> T e. _V )
14	13	3ad2ant3	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> T e. _V )
15	1 2 3	mrexval	|- ( T e. _V -> R = Word ( C u. V ) )
16	14 15	syl	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> R = Word ( C u. V ) )
17	6 16	eleqtrrd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> <" X "> e. R )
18		eqid	|- ( freeMnd ` ( C u. V ) ) = ( freeMnd ` ( C u. V ) )
19	1 2 3 4 18	mrsubval	|- ( ( F : A --> R /\ A C_ V /\ <" X "> e. R ) -> ( ( S ` F ) ` <" X "> ) = ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) ) )
20	17 19	syld3an3	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( S ` F ) ` <" X "> ) = ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) ) )
21		simpl1	|- ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) -> F : A --> R )
22	21	ffvelcdmda	|- ( ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) /\ v e. A ) -> ( F ` v ) e. R )
23	16	ad2antrr	|- ( ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) /\ v e. A ) -> R = Word ( C u. V ) )
24	22 23	eleqtrd	|- ( ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) /\ v e. A ) -> ( F ` v ) e. Word ( C u. V ) )
25		simplr	|- ( ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) /\ -. v e. A ) -> v e. ( C u. V ) )
26	25	s1cld	|- ( ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) /\ -. v e. A ) -> <" v "> e. Word ( C u. V ) )
27	24 26	ifclda	|- ( ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) /\ v e. ( C u. V ) ) -> if ( v e. A , ( F ` v ) , <" v "> ) e. Word ( C u. V ) )
28	27	fmpttd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) : ( C u. V ) --> Word ( C u. V ) )
29		s1co	|- ( ( X e. ( C u. V ) /\ ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) : ( C u. V ) --> Word ( C u. V ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) = <" ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) "> )
30	5 28 29	syl2anc	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) = <" ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) "> )
31		eleq1	|- ( v = X -> ( v e. A <-> X e. A ) )
32		fveq2	|- ( v = X -> ( F ` v ) = ( F ` X ) )
33		s1eq	|- ( v = X -> <" v "> = <" X "> )
34	31 32 33	ifbieq12d	|- ( v = X -> if ( v e. A , ( F ` v ) , <" v "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
35		eqid	|- ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) = ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) )
36		fvex	|- ( F ` X ) e. _V
37		s1cli	|- <" X "> e. Word _V
38	37	elexi	|- <" X "> e. _V
39	36 38	ifex	|- if ( X e. A , ( F ` X ) , <" X "> ) e. _V
40	34 35 39	fvmpt	|- ( X e. ( C u. V ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) = if ( X e. A , ( F ` X ) , <" X "> ) )
41	40	3ad2ant3	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) = if ( X e. A , ( F ` X ) , <" X "> ) )
42	41	s1eqd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> <" ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) "> = <" if ( X e. A , ( F ` X ) , <" X "> ) "> )
43	30 42	eqtrd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) = <" if ( X e. A , ( F ` X ) , <" X "> ) "> )
44	43	oveq2d	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( freeMnd ` ( C u. V ) ) gsum ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. <" X "> ) ) = ( ( freeMnd ` ( C u. V ) ) gsum <" if ( X e. A , ( F ` X ) , <" X "> ) "> ) )
45	28 5	ffvelcdmd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) ` X ) e. Word ( C u. V ) )
46	41 45	eqeltrrd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> if ( X e. A , ( F ` X ) , <" X "> ) e. Word ( C u. V ) )
47	1	fvexi	|- C e. _V
48	2	fvexi	|- V e. _V
49	47 48	unex	|- ( C u. V ) e. _V
50		eqid	|- ( Base ` ( freeMnd ` ( C u. V ) ) ) = ( Base ` ( freeMnd ` ( C u. V ) ) )
51	18 50	frmdbas	|- ( ( C u. V ) e. _V -> ( Base ` ( freeMnd ` ( C u. V ) ) ) = Word ( C u. V ) )
52	49 51	ax-mp	|- ( Base ` ( freeMnd ` ( C u. V ) ) ) = Word ( C u. V )
53	52	eqcomi	|- Word ( C u. V ) = ( Base ` ( freeMnd ` ( C u. V ) ) )
54	53	gsumws1	|- ( if ( X e. A , ( F ` X ) , <" X "> ) e. Word ( C u. V ) -> ( ( freeMnd ` ( C u. V ) ) gsum <" if ( X e. A , ( F ` X ) , <" X "> ) "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
55	46 54	syl	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( freeMnd ` ( C u. V ) ) gsum <" if ( X e. A , ( F ` X ) , <" X "> ) "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
56	20 44 55	3eqtrd	|- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( S ` F ) ` <" X "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )