fcoconst

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

		Ref	Expression
	Assertion	fcoconst	$⊢ (F Fn X \land Y \in X) \to F \circ (I \times \{Y\}) = I \times \{F (Y)\}$

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

Metamath Proof Explorer