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

Metamath Proof Explorer

Theorem cncfmpt1f

Description: Composition of continuous functions. -cn-> analogue of cnmpt11f . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses cncfmpt1f.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
cncfmpt1f.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion cncfmpt1f ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cncfmpt1f.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
2 cncfmpt1f.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
3 cncff ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
4 2 3 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
5 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
6 5 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
7 4 6 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ℂ )
8 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
9 cncff ⊢ ( 𝐹 ∈ ( ℂ –cn→ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
10 1 9 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
11 10 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℂ ↦ ( 𝐹 ‘ 𝑦 ) ) )
12 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
13 7 8 11 12 fmptcof ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) )
14 2 1 cncfco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
15 13 14 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )