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		dffn2	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 ⟶ V )
5	4	birani	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ V )
6	5	feqmptd	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 𝐹 = ( 𝑦 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑦 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
8	1 3 6 7	fmptco	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑌 ) ) )
9		fconstmpt	⊢ ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑌 ) )
10	8 9	eqtr4di	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) )