This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝐼 × { 𝑌 } ) ) = ( 𝐼 × { ( 𝐹 ‘ 𝑌 ) } ) )