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		ovmul	⊢ ( ( - 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→ ℂ ) )