Theorem fcoconst

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

	Ref	Expression
Assertion	fcoconst	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑌 ∈ 𝑋 )
2		fconstmpt	⊢ ( 𝐼 × { 𝑌 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑌 )
3	2	a1i	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐼 × { 𝑌 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑌 ) )
4		simpl	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
5		dffn2	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 ⟶ V )
6	4 5	sylib	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ V )
7	6	feqmptd	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 𝐹 = ( 𝑦 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑦 ) ) )
8		fveq2	⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
9	1 3 7 8	fmptco	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑌 ) ) )
10		fconstmpt	⊢ ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑌 ) )
11	9 10	eqtr4di	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) )