Theorem ofc2

Description: Right operation by a constant. (Contributed by NM, 7-Oct-2014)

	Ref	Expression
Hypotheses	ofc2.1	|- ( ph -> A e. V )
	ofc2.2	|- ( ph -> B e. W )
	ofc2.3	|- ( ph -> F Fn A )
	ofc2.4	|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
Assertion	ofc2	|- ( ( ph /\ X e. A ) -> ( ( F oF R ( A X. { B } ) ) ` X ) = ( C R B ) )

Proof

Step	Hyp	Ref	Expression
1		ofc2.1	|- ( ph -> A e. V )
2		ofc2.2	|- ( ph -> B e. W )
3		ofc2.3	|- ( ph -> F Fn A )
4		ofc2.4	|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
5		fnconstg	|- ( B e. W -> ( A X. { B } ) Fn A )
6	2 5	syl	|- ( ph -> ( A X. { B } ) Fn A )
7		inidm	|- ( A i^i A ) = A
8		fvconst2g	|- ( ( B e. W /\ X e. A ) -> ( ( A X. { B } ) ` X ) = B )
9	2 8	sylan	|- ( ( ph /\ X e. A ) -> ( ( A X. { B } ) ` X ) = B )
10	3 6 1 1 7 4 9	ofval	|- ( ( ph /\ X e. A ) -> ( ( F oF R ( A X. { B } ) ) ` X ) = ( C R B ) )