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 ⊢ F = x ∈ A ⟼ − x
Assertion negcncf ⊢ A ⊆ ℂ → F : A ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 negcncf.1 ⊢ F = x ∈ A ⟼ − x
2 neg1cn ⊢ − 1 ∈ ℂ
3 ssel2 ⊢ A ⊆ ℂ ∧ x ∈ A → x ∈ ℂ
4 ovmpot ⊢ − 1 ∈ ℂ ∧ x ∈ ℂ → -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x = -1 ⁢ x
5 4 eqcomd ⊢ − 1 ∈ ℂ ∧ x ∈ ℂ → -1 ⁢ x = -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x
6 2 3 5 sylancr ⊢ A ⊆ ℂ ∧ x ∈ A → -1 ⁢ x = -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x
7 3 mulm1d ⊢ A ⊆ ℂ ∧ x ∈ A → -1 ⁢ x = − x
8 6 7 eqtr3d ⊢ A ⊆ ℂ ∧ x ∈ A → -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x = − x
9 8 mpteq2dva ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x = x ∈ A ⟼ − x
10 9 1 eqtr4di ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x = F
11 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
12 11 mpomulcn ⊢ a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
13 12 a1i ⊢ A ⊆ ℂ → a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
14 ssid ⊢ ℂ ⊆ ℂ
15 cncfmptc ⊢ − 1 ∈ ℂ ∧ A ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ A ⟼ − 1 : A ⟶cn ℂ
16 2 14 15 mp3an13 ⊢ A ⊆ ℂ → x ∈ A ⟼ − 1 : A ⟶cn ℂ
17 cncfmptid ⊢ A ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ A ⟼ x : A ⟶cn ℂ
18 14 17 mpan2 ⊢ A ⊆ ℂ → x ∈ A ⟼ x : A ⟶cn ℂ
19 11 13 16 18 cncfmpt2f ⊢ A ⊆ ℂ → x ∈ A ⟼ -1 a ∈ ℂ , b ∈ ℂ ⟼ a ⁢ b x : A ⟶cn ℂ
20 10 19 eqeltrrd ⊢ A ⊆ ℂ → F : A ⟶cn ℂ