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

Metamath Proof Explorer

Theorem constcof

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

Ref Expression
Hypotheses constcof.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝐼 )
constcof.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion constcof ( 𝜑 → ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) = ( 𝑋 × { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 constcof.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝐼 )
2 constcof.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
3 fnconstg ⊢ ( 𝑌 ∈ 𝑉 → ( 𝐼 × { 𝑌 } ) Fn 𝐼 )
4 2 3 syl ⊢ ( 𝜑 → ( 𝐼 × { 𝑌 } ) Fn 𝐼 )
5 fnfco ⊢ ( ( ( 𝐼 × { 𝑌 } ) Fn 𝐼 ∧ 𝐹 : 𝑋 ⟶ 𝐼 ) → ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) Fn 𝑋 )
6 4 1 5 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) Fn 𝑋 )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝐼 )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9 7 8 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝐼 × { 𝑌 } ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ∈ 𝑉 )
11 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 )
12 fvconst2g ⊢ ( ( 𝑌 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 ) → ( ( 𝐼 × { 𝑌 } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑌 )
13 10 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐼 × { 𝑌 } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑌 )
14 9 13 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) ‘ 𝑥 ) = 𝑌 )
15 6 14 fconst7v ⊢ ( 𝜑 → ( ( 𝐼 × { 𝑌 } ) ∘ 𝐹 ) = ( 𝑋 × { 𝑌 } ) )