Theorem ofcfval4

Description: The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval4.1	|- ( ph -> F : A --> B )
	ofcfval4.2	|- ( ph -> A e. V )
	ofcfval4.3	|- ( ph -> C e. W )
Assertion	ofcfval4	|- ( ph -> ( F oFC R C ) = ( ( x e. B |-> ( x R C ) ) o. F ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval4.1	|- ( ph -> F : A --> B )
2		ofcfval4.2	|- ( ph -> A e. V )
3		ofcfval4.3	|- ( ph -> C e. W )
4	1	fdmd	|- ( ph -> dom F = A )
5	4	mpteq1d	|- ( ph -> ( y e. dom F |-> ( ( F ` y ) R C ) ) = ( y e. A |-> ( ( F ` y ) R C ) ) )
6	1 2	fexd	|- ( ph -> F e. _V )
7		ofcfval3	|- ( ( F e. _V /\ C e. W ) -> ( F oFC R C ) = ( y e. dom F |-> ( ( F ` y ) R C ) ) )
8	6 3 7	syl2anc	|- ( ph -> ( F oFC R C ) = ( y e. dom F |-> ( ( F ` y ) R C ) ) )
9	1	ffvelrnda	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. B )
10	1	feqmptd	|- ( ph -> F = ( y e. A |-> ( F ` y ) ) )
11		eqidd	|- ( ph -> ( x e. B |-> ( x R C ) ) = ( x e. B |-> ( x R C ) ) )
12		oveq1	|- ( x = ( F ` y ) -> ( x R C ) = ( ( F ` y ) R C ) )
13	9 10 11 12	fmptco	|- ( ph -> ( ( x e. B |-> ( x R C ) ) o. F ) = ( y e. A |-> ( ( F ` y ) R C ) ) )
14	5 8 13	3eqtr4d	|- ( ph -> ( F oFC R C ) = ( ( x e. B |-> ( x R C ) ) o. F ) )