Metamath Proof Explorer

Theorem negcncf

Description: The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis negcncf.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 )
Assertion negcncf ( 𝐴 ⊆ ℂ → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 negcncf.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 )
2 neg1cn ⊢ - 1 ∈ ℂ
3 ssel2 ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
4 ovmpot ⊢ ( ( - 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) = ( - 1 · 𝑥 ) )
5 4 eqcomd ⊢ ( ( - 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 1 · 𝑥 ) = ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) )
6 2 3 5 sylancr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · 𝑥 ) = ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) )
7 3 mulm1d ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · 𝑥 ) = - 𝑥 )
8 6 7 eqtr3d ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) = - 𝑥 )
9 8 mpteq2dva ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 ) )
10 9 1 eqtr4di ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) ) = 𝐹 )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 11 mpomulcn ⊢ ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
13 12 a1i ⊢ ( 𝐴 ⊆ ℂ → ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
14 ssid ⊢ ℂ ⊆ ℂ
15 cncfmptc ⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ - 1 ) ∈ ( 𝐴 –cn→ ℂ ) )
16 2 14 15 mp3an13 ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ - 1 ) ∈ ( 𝐴 –cn→ ℂ ) )
17 cncfmptid ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
18 14 17 mpan2 ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
19 11 13 16 18 cncfmpt2f ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ ( - 1 ( 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ↦ ( 𝑎 · 𝑏 ) ) 𝑥 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
20 10 19 eqeltrrd ⊢ ( 𝐴 ⊆ ℂ → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )