Metamath Proof Explorer

Theorem gg-divcn

Description: Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses mpomulcn.j ⊢J=TopOpen⁡ℂfld
gg-divcn.k ⊢K=J↾𝑡ℂ∖0
Assertion gg-divcn ⊢÷∈J×tKCnJ

Proof

Step Hyp Ref Expression
1 mpomulcn.j ⊢J=TopOpen⁡ℂfld
2 gg-divcn.k ⊢K=J↾𝑡ℂ∖0
3 df-div ⊢÷=x∈ℂ,y∈ℂ∖0⟼ιz∈ℂ|y⁢z=x
4 eldifsn ⊢y∈ℂ∖0↔y∈ℂ∧y≠0
5 divval ⊢x∈ℂ∧y∈ℂ∧y≠0→xy=ιz∈ℂ|y⁢z=x
6 divrec ⊢x∈ℂ∧y∈ℂ∧y≠0→xy=x⁢1y
7 5 6 eqtr3d ⊢x∈ℂ∧y∈ℂ∧y≠0→ιz∈ℂ|y⁢z=x=x⁢1y
8 7 3expb ⊢x∈ℂ∧y∈ℂ∧y≠0→ιz∈ℂ|y⁢z=x=x⁢1y
9 4 8 sylan2b ⊢x∈ℂ∧y∈ℂ∖0→ιz∈ℂ|y⁢z=x=x⁢1y
10 9 mpoeq3ia ⊢x∈ℂ,y∈ℂ∖0⟼ιz∈ℂ|y⁢z=x=x∈ℂ,y∈ℂ∖0⟼x⁢1y
11 3 10 eqtri ⊢÷=x∈ℂ,y∈ℂ∖0⟼x⁢1y
12 1 cnfldtopon ⊢J∈TopOn⁡ℂ
13 12 a1i ⊢⊤→J∈TopOn⁡ℂ
14 difss ⊢ℂ∖0⊆ℂ
15 resttopon ⊢J∈TopOn⁡ℂ∧ℂ∖0⊆ℂ→J↾𝑡ℂ∖0∈TopOn⁡ℂ∖0
16 13 14 15 sylancl ⊢⊤→J↾𝑡ℂ∖0∈TopOn⁡ℂ∖0
17 2 16 eqeltrid ⊢⊤→K∈TopOn⁡ℂ∖0
18 13 17 cnmpt1st ⊢⊤→x∈ℂ,y∈ℂ∖0⟼x∈J×tKCnJ
19 13 17 cnmpt2nd ⊢⊤→x∈ℂ,y∈ℂ∖0⟼y∈J×tKCnK
20 eqid ⊢z∈ℂ∖0⟼1z=z∈ℂ∖0⟼1z
21 eldifsn ⊢z∈ℂ∖0↔z∈ℂ∧z≠0
22 reccl ⊢z∈ℂ∧z≠0→1z∈ℂ
23 21 22 sylbi ⊢z∈ℂ∖0→1z∈ℂ
24 20 23 fmpti ⊢z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ
25 eqid ⊢if1≤x⁢w1x⁢w⁢x2=if1≤x⁢w1x⁢w⁢x2
26 25 reccn2 ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
27 ovres ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y=xabs∘−y
28 eldifi ⊢x∈ℂ∖0→x∈ℂ
29 eldifi ⊢y∈ℂ∖0→y∈ℂ
30 eqid ⊢abs∘−=abs∘−
31 30 cnmetdval ⊢x∈ℂ∧y∈ℂ→xabs∘−y=x−y
32 abssub ⊢x∈ℂ∧y∈ℂ→x−y=y−x
33 31 32 eqtrd ⊢x∈ℂ∧y∈ℂ→xabs∘−y=y−x
34 28 29 33 syl2an ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−y=y−x
35 27 34 eqtrd ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y=y−x
36 35 breq1d ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y<a↔y−x<a
37 oveq2 ⊢z=x→1z=1x
38 ovex ⊢1x∈V
39 37 20 38 fvmpt ⊢x∈ℂ∖0→z∈ℂ∖0⟼1z⁡x=1x
40 oveq2 ⊢z=y→1z=1y
41 ovex ⊢1y∈V
42 40 20 41 fvmpt ⊢y∈ℂ∖0→z∈ℂ∖0⟼1z⁡y=1y
43 39 42 oveqan12d ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y=1xabs∘−1y
44 eldifsn ⊢x∈ℂ∖0↔x∈ℂ∧x≠0
45 reccl ⊢x∈ℂ∧x≠0→1x∈ℂ
46 44 45 sylbi ⊢x∈ℂ∖0→1x∈ℂ
47 reccl ⊢y∈ℂ∧y≠0→1y∈ℂ
48 4 47 sylbi ⊢y∈ℂ∖0→1y∈ℂ
49 30 cnmetdval ⊢1x∈ℂ∧1y∈ℂ→1xabs∘−1y=1x−1y
50 abssub ⊢1x∈ℂ∧1y∈ℂ→1x−1y=1y−1x
51 49 50 eqtrd ⊢1x∈ℂ∧1y∈ℂ→1xabs∘−1y=1y−1x
52 46 48 51 syl2an ⊢x∈ℂ∖0∧y∈ℂ∖0→1xabs∘−1y=1y−1x
53 43 52 eqtrd ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y=1y−1x
54 53 breq1d ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔1y−1x<w
55 36 54 imbi12d ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔y−x<a→1y−1x<w
56 55 ralbidva ⊢x∈ℂ∖0→∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∀y∈ℂ∖0y−x<a→1y−1x<w
57 56 rexbidv ⊢x∈ℂ∖0→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
58 57 adantr ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
59 26 58 mpbird ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
60 59 rgen2 ⊢∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
61 cnxmet ⊢abs∘−∈∞Met⁡ℂ
62 xmetres2 ⊢abs∘−∈∞Met⁡ℂ∧ℂ∖0⊆ℂ→abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0
63 61 14 62 mp2an ⊢abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0
64 eqid ⊢abs∘−↾ℂ∖0×ℂ∖0=abs∘−↾ℂ∖0×ℂ∖0
65 1 cnfldtopn ⊢J=MetOpen⁡abs∘−
66 eqid ⊢MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
67 64 65 66 metrest ⊢abs∘−∈∞Met⁡ℂ∧ℂ∖0⊆ℂ→J↾𝑡ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
68 61 14 67 mp2an ⊢J↾𝑡ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
69 2 68 eqtri ⊢K=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
70 69 65 metcn ⊢abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0∧abs∘−∈∞Met⁡ℂ→z∈ℂ∖0⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
71 63 61 70 mp2an ⊢z∈ℂ∖0⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
72 24 60 71 mpbir2an ⊢z∈ℂ∖0⟼1z∈KCnJ
73 72 a1i ⊢⊤→z∈ℂ∖0⟼1z∈KCnJ
74 13 17 19 17 73 40 cnmpt21 ⊢⊤→x∈ℂ,y∈ℂ∖0⟼1y∈J×tKCnJ
75 1 mpomulcn ⊢u∈ℂ,v∈ℂ⟼u⁢v∈J×tJCnJ
76 75 a1i ⊢⊤→u∈ℂ,v∈ℂ⟼u⁢v∈J×tJCnJ
77 oveq12 ⊢u=x∧v=1y→u⁢v=x⁢1y
78 13 17 18 74 13 13 76 77 cnmpt22 ⊢⊤→x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
79 78 mptru ⊢x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
80 11 79 eqeltri ⊢÷∈J×tKCnJ