Theorem fcoconst

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

	Ref	Expression
Assertion	fcoconst	$$⊢\left(FFnX\wedge Y\in X\right)\to F\circ \left(I\times \left\{Y\right\}\right)=I\times \left\{F\left(Y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simplr	$$⊢\left(\left(FFnX\wedge Y\in X\right)\wedge x\in I\right)\to Y\in X$$
2		fconstmpt	$$⊢I\times \left\{Y\right\}=\left(x\in I⟼Y\right)$$
3	2	a1i	$$⊢\left(FFnX\wedge Y\in X\right)\to I\times \left\{Y\right\}=\left(x\in I⟼Y\right)$$
4		simpl	$$⊢\left(FFnX\wedge Y\in X\right)\to FFnX$$
5		dffn2	$$⊢FFnX\leftrightarrow F:X⟶\mathrm{V}$$
6	4 5	sylib	$$⊢\left(FFnX\wedge Y\in X\right)\to F:X⟶\mathrm{V}$$
7	6	feqmptd	$$⊢\left(FFnX\wedge Y\in X\right)\to F=\left(y\in X⟼F\left(y\right)\right)$$
8		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
9	1 3 7 8	fmptco	$$⊢\left(FFnX\wedge Y\in X\right)\to F\circ \left(I\times \left\{Y\right\}\right)=\left(x\in I⟼F\left(Y\right)\right)$$
10		fconstmpt	$$⊢I\times \left\{F\left(Y\right)\right\}=\left(x\in I⟼F\left(Y\right)\right)$$
11	9 10	eqtr4di	$$⊢\left(FFnX\wedge Y\in X\right)\to F\circ \left(I\times \left\{Y\right\}\right)=I\times \left\{F\left(Y\right)\right\}$$