Metamath Proof Explorer


Theorem cncfmpt2f

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

Ref Expression
Hypotheses cncfmpt2f.1 𝐽 = ( TopOpen ‘ ℂfld )
cncfmpt2f.2 ( 𝜑𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
cncfmpt2f.3 ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) )
cncfmpt2f.4 ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( 𝑋cn→ ℂ ) )
Assertion cncfmpt2f ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cncfmpt2f.1 𝐽 = ( TopOpen ‘ ℂfld )
2 cncfmpt2f.2 ( 𝜑𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
3 cncfmpt2f.3 ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) )
4 cncfmpt2f.4 ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( 𝑋cn→ ℂ ) )
5 1 cnfldtopon 𝐽 ∈ ( TopOn ‘ ℂ )
6 cncfrss ( ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) → 𝑋 ⊆ ℂ )
7 3 6 syl ( 𝜑𝑋 ⊆ ℂ )
8 resttopon ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐽t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
9 5 7 8 sylancr ( 𝜑 → ( 𝐽t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
10 ssid ℂ ⊆ ℂ
11 eqid ( 𝐽t 𝑋 ) = ( 𝐽t 𝑋 )
12 5 toponrestid 𝐽 = ( 𝐽t ℂ )
13 1 11 12 cncfcn ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋cn→ ℂ ) = ( ( 𝐽t 𝑋 ) Cn 𝐽 ) )
14 7 10 13 sylancl ( 𝜑 → ( 𝑋cn→ ℂ ) = ( ( 𝐽t 𝑋 ) Cn 𝐽 ) )
15 3 14 eleqtrd ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( ( 𝐽t 𝑋 ) Cn 𝐽 ) )
16 4 14 eleqtrd ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( ( 𝐽t 𝑋 ) Cn 𝐽 ) )
17 9 15 16 2 cnmpt12f ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽t 𝑋 ) Cn 𝐽 ) )
18 17 14 eleqtrrd ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋cn→ ℂ ) )