This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )