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

Metamath Proof Explorer

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