Theorem ofcc

Description: Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ofcc.1	|- ( ph -> A e. V )
2		ofcc.2	|- ( ph -> B e. W )
3		ofcc.3	|- ( ph -> C e. X )
4		fnconstg	|- ( B e. W -> ( A X. { B } ) Fn A )
5	2 4	syl	|- ( ph -> ( A X. { B } ) Fn A )
6		fvconst2g	|- ( ( B e. W /\ x e. A ) -> ( ( A X. { B } ) ` x ) = B )
7	2 6	sylan	|- ( ( ph /\ x e. A ) -> ( ( A X. { B } ) ` x ) = B )
8	5 1 3 7	ofcfval	|- ( ph -> ( ( A X. { B } ) oFC R C ) = ( x e. A |-> ( B R C ) ) )
9		fconstmpt	|- ( A X. { ( B R C ) } ) = ( x e. A |-> ( B R C ) )
10	8 9	eqtr4di	|- ( ph -> ( ( A X. { B } ) oFC R C ) = ( A X. { ( B R C ) } ) )