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		dffn2	$$⊢FFnX\leftrightarrow F:X⟶\mathrm{V}$$
5	4	birani	$$⊢\left(FFnX\wedge Y\in X\right)\to F:X⟶\mathrm{V}$$
6	5	feqmptd	$$⊢\left(FFnX\wedge Y\in X\right)\to F=\left(y\in X⟼F\left(y\right)\right)$$
7		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
8	1 3 6 7	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)$$
9		fconstmpt	$$⊢I\times \left\{F\left(Y\right)\right\}=\left(x\in I⟼F\left(Y\right)\right)$$
10	8 9	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\}$$