Theorem constcof

Description: Composition with a constant function. See also fcoconst . (Contributed by Thierry Arnoux, 11-Jan-2026)

	Ref	Expression
Hypotheses	constcof.1	$$⊢\phi \to F:X⟶I$$
	constcof.2	$$⊢\phi \to Y\in V$$
Assertion	constcof	$$⊢\phi \to \left(I\times \left\{Y\right\}\right)\circ F=X\times \left\{Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		constcof.1	$$⊢\phi \to F:X⟶I$$
2		constcof.2	$$⊢\phi \to Y\in V$$
3		fnconstg	$$⊢Y\in V\to \left(I\times \left\{Y\right\}\right)FnI$$
4	2 3	syl	$$⊢\phi \to \left(I\times \left\{Y\right\}\right)FnI$$
5		fnfco	$$⊢\left(\left(I\times \left\{Y\right\}\right)FnI\wedge F:X⟶I\right)\to \left(\left(I\times \left\{Y\right\}\right)\circ F\right)FnX$$
6	4 1 5	syl2anc	$$⊢\phi \to \left(\left(I\times \left\{Y\right\}\right)\circ F\right)FnX$$
7	1	adantr	$$⊢\left(\phi \wedge x\in X\right)\to F:X⟶I$$
8		simpr	$$⊢\left(\phi \wedge x\in X\right)\to x\in X$$
9	7 8	fvco3d	$$⊢\left(\phi \wedge x\in X\right)\to \left(\left(I\times \left\{Y\right\}\right)\circ F\right)\left(x\right)=\left(I\times \left\{Y\right\}\right)\left(F\left(x\right)\right)$$
10	2	adantr	$$⊢\left(\phi \wedge x\in X\right)\to Y\in V$$
11	1	ffvelcdmda	$$⊢\left(\phi \wedge x\in X\right)\to F\left(x\right)\in I$$
12		fvconst2g	$$⊢\left(Y\in V\wedge F\left(x\right)\in I\right)\to \left(I\times \left\{Y\right\}\right)\left(F\left(x\right)\right)=Y$$
13	10 11 12	syl2anc	$$⊢\left(\phi \wedge x\in X\right)\to \left(I\times \left\{Y\right\}\right)\left(F\left(x\right)\right)=Y$$
14	9 13	eqtrd	$$⊢\left(\phi \wedge x\in X\right)\to \left(\left(I\times \left\{Y\right\}\right)\circ F\right)\left(x\right)=Y$$
15	6 14	fconst7v	$$⊢\phi \to \left(I\times \left\{Y\right\}\right)\circ F=X\times \left\{Y\right\}$$