Theorem ofc1

Description: Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ofc1.1	|- ( ph -> A e. V )
2		ofc1.2	|- ( ph -> B e. W )
3		ofc1.3	|- ( ph -> F Fn A )
4		ofc1.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	6 3 1 1 7 9 4	ofval	|- ( ( ph /\ X e. A ) -> ( ( ( A X. { B } ) oF R F ) ` X ) = ( B R C ) )