Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 gg-negcncf.1 ⊢F=x∈A⟼−x
2 ssel2 ⊢A⊆ℂ∧x∈A→x∈ℂ
3 2 mulm1d ⊢A⊆ℂ∧x∈A→-1⁢x=−x
4 neg1cn ⊢−1∈ℂ
5 4 a1i ⊢A⊆ℂ∧x∈A→−1∈ℂ
6 5 2 jca ⊢A⊆ℂ∧x∈A→−1∈ℂ∧x∈ℂ
7 ovmul ⊢−1∈ℂ∧x∈ℂ→-1a∈ℂ,b∈ℂ⟼a⁢bx=-1⁢x
8 7 eqcomd ⊢−1∈ℂ∧x∈ℂ→-1⁢x=-1a∈ℂ,b∈ℂ⟼a⁢bx
9 6 8 syl ⊢A⊆ℂ∧x∈A→-1⁢x=-1a∈ℂ,b∈ℂ⟼a⁢bx
10 9 eqeq1d ⊢A⊆ℂ∧x∈A→-1⁢x=−x↔-1a∈ℂ,b∈ℂ⟼a⁢bx=−x
11 10 biimpd ⊢A⊆ℂ∧x∈A→-1⁢x=−x→-1a∈ℂ,b∈ℂ⟼a⁢bx=−x
12 3 11 mpd ⊢A⊆ℂ∧x∈A→-1a∈ℂ,b∈ℂ⟼a⁢bx=−x
13 12 mpteq2dva ⊢A⊆ℂ→x∈A⟼-1a∈ℂ,b∈ℂ⟼a⁢bx=x∈A⟼−x
14 13 1 eqtr4di ⊢A⊆ℂ→x∈A⟼-1a∈ℂ,b∈ℂ⟼a⁢bx=F
15 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
16 15 mpomulcn ⊢a∈ℂ,b∈ℂ⟼a⁢b∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
17 16 a1i ⊢A⊆ℂ→a∈ℂ,b∈ℂ⟼a⁢b∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 ssid ⊢ℂ⊆ℂ
19 cncfmptc ⊢−1∈ℂ∧A⊆ℂ∧ℂ⊆ℂ→x∈A⟼−1:A⟶cnℂ
20 4 18 19 mp3an13 ⊢A⊆ℂ→x∈A⟼−1:A⟶cnℂ
21 cncfmptid ⊢A⊆ℂ∧ℂ⊆ℂ→x∈A⟼x:A⟶cnℂ
22 18 21 mpan2 ⊢A⊆ℂ→x∈A⟼x:A⟶cnℂ
23 15 17 20 22 cncfmpt2f ⊢A⊆ℂ→x∈A⟼-1a∈ℂ,b∈ℂ⟼a⁢bx:A⟶cnℂ
24 14 23 eqeltrrd ⊢A⊆ℂ→F:A⟶cnℂ