Metamath Proof Explorer

Theorem fcoconst

Description: Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015)

Ref Expression
Assertion fcoconst 
|- ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( I X. { ( F ` Y ) } ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( F Fn X /\ Y e. X ) /\ x e. I ) -> Y e. X )
2 fconstmpt 
 |-  ( I X. { Y } ) = ( x e. I |-> Y )
3 2 a1i 
 |-  ( ( F Fn X /\ Y e. X ) -> ( I X. { Y } ) = ( x e. I |-> Y ) )
4 simpl 
 |-  ( ( F Fn X /\ Y e. X ) -> F Fn X )
5 dffn2 
 |-  ( F Fn X <-> F : X --> _V )
6 4 5 sylib 
 |-  ( ( F Fn X /\ Y e. X ) -> F : X --> _V )
7 6 feqmptd 
 |-  ( ( F Fn X /\ Y e. X ) -> F = ( y e. X |-> ( F ` y ) ) )
8 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
9 1 3 7 8 fmptco 
 |-  ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( x e. I |-> ( F ` Y ) ) )
10 fconstmpt 
 |-  ( I X. { ( F ` Y ) } ) = ( x e. I |-> ( F ` Y ) )
11 9 10 eqtr4di 
 |-  ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( I X. { ( F ` Y ) } ) )