Theorem ofcval

Description: Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	|- ( ph -> F Fn A )
	ofcfval.2	|- ( ph -> A e. V )
	ofcfval.3	|- ( ph -> C e. W )
	ofcval.6	|- ( ( ph /\ X e. A ) -> ( F ` X ) = B )
Assertion	ofcval	|- ( ( ph /\ X e. A ) -> ( ( F oFC R C ) ` X ) = ( B R C ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	|- ( ph -> F Fn A )
2		ofcfval.2	|- ( ph -> A e. V )
3		ofcfval.3	|- ( ph -> C e. W )
4		ofcval.6	|- ( ( ph /\ X e. A ) -> ( F ` X ) = B )
5		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
6	1 2 3 5	ofcfval	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
7	6	adantr	|- ( ( ph /\ X e. A ) -> ( F oFC R C ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
8		simpr	|- ( ( ( ph /\ X e. A ) /\ x = X ) -> x = X )
9	8	fveq2d	|- ( ( ( ph /\ X e. A ) /\ x = X ) -> ( F ` x ) = ( F ` X ) )
10	9	oveq1d	|- ( ( ( ph /\ X e. A ) /\ x = X ) -> ( ( F ` x ) R C ) = ( ( F ` X ) R C ) )
11		simpr	|- ( ( ph /\ X e. A ) -> X e. A )
12		ovexd	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) R C ) e. _V )
13	7 10 11 12	fvmptd	|- ( ( ph /\ X e. A ) -> ( ( F oFC R C ) ` X ) = ( ( F ` X ) R C ) )
14	4	oveq1d	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) R C ) = ( B R C ) )
15	13 14	eqtrd	|- ( ( ph /\ X e. A ) -> ( ( F oFC R C ) ` X ) = ( B R C ) )