Theorem ofcof

Description: Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018)

	Ref	Expression
Hypotheses	ofcof.1	|- ( ph -> F : A --> B )
	ofcof.2	|- ( ph -> A e. V )
	ofcof.3	|- ( ph -> C e. W )
Assertion	ofcof	|- ( ph -> ( F oFC R C ) = ( F oF R ( A X. { C } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofcof.1	|- ( ph -> F : A --> B )
2		ofcof.2	|- ( ph -> A e. V )
3		ofcof.3	|- ( ph -> C e. W )
4	1	ffnd	|- ( ph -> F Fn A )
5		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
6	4 2 3 5	ofcfval	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
7		fnconstg	|- ( C e. W -> ( A X. { C } ) Fn A )
8	3 7	syl	|- ( ph -> ( A X. { C } ) Fn A )
9		inidm	|- ( A i^i A ) = A
10		fvconst2g	|- ( ( C e. W /\ x e. A ) -> ( ( A X. { C } ) ` x ) = C )
11	3 10	sylan	|- ( ( ph /\ x e. A ) -> ( ( A X. { C } ) ` x ) = C )
12	4 8 2 2 9 5 11	offval	|- ( ph -> ( F oF R ( A X. { C } ) ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
13	6 12	eqtr4d	|- ( ph -> ( F oFC R C ) = ( F oF R ( A X. { C } ) ) )