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		dffn2	|- ( F Fn X <-> F : X --> _V )
5	4	birani	|- ( ( F Fn X /\ Y e. X ) -> F : X --> _V )
6	5	feqmptd	|- ( ( F Fn X /\ Y e. X ) -> F = ( y e. X |-> ( F ` y ) ) )
7		fveq2	|- ( y = Y -> ( F ` y ) = ( F ` Y ) )
8	1 3 6 7	fmptco	|- ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( x e. I |-> ( F ` Y ) ) )
9		fconstmpt	|- ( I X. { ( F ` Y ) } ) = ( x e. I |-> ( F ` Y ) )
10	8 9	eqtr4di	|- ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( I X. { ( F ` Y ) } ) )