| Step | Hyp | Ref
| Expression |
| 1 | | df-div 11921 |
. . 3
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) |
| 2 | | eldifsn 4786 |
. . . . 5
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
| 3 | | divval 11924 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) |
| 4 | | divrec 11938 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (𝑥 · (1 / 𝑦))) |
| 5 | 3, 4 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
| 6 | 5 | 3expb 1121 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
| 7 | 2, 6 | sylan2b 594 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
| 8 | 7 | mpoeq3ia 7511 |
. . 3
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦))) |
| 9 | 1, 8 | eqtri 2765 |
. 2
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) |
| 10 | | mpomulcn.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 11 | 10 | cnfldtopon 24803 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐽 ∈
(TopOn‘ℂ)) |
| 13 | | divcn.k |
. . . . 5
⊢ 𝐾 = (𝐽 ↾t (ℂ ∖
{0})) |
| 14 | | difss 4136 |
. . . . . 6
⊢ (ℂ
∖ {0}) ⊆ ℂ |
| 15 | | resttopon 23169 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾t (ℂ ∖ {0}))
∈ (TopOn‘(ℂ ∖ {0}))) |
| 16 | 12, 14, 15 | sylancl 586 |
. . . . 5
⊢ (⊤
→ (𝐽
↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖
{0}))) |
| 17 | 13, 16 | eqeltrid 2845 |
. . . 4
⊢ (⊤
→ 𝐾 ∈
(TopOn‘(ℂ ∖ {0}))) |
| 18 | 12, 17 | cnmpt1st 23676 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑥) ∈
((𝐽 ×t
𝐾) Cn 𝐽)) |
| 19 | 12, 17 | cnmpt2nd 23677 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑦) ∈
((𝐽 ×t
𝐾) Cn 𝐾)) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) |
| 21 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
| 22 | | eldifsni 4790 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
| 23 | 21, 22 | reccld 12036 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (1 / 𝑧) ∈
ℂ) |
| 24 | 20, 23 | fmpti 7132 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)):(ℂ
∖ {0})⟶ℂ |
| 25 | | eqid 2737 |
. . . . . . . . . 10
⊢ (if(1
≤ ((abs‘𝑥)
· 𝑤), 1,
((abs‘𝑥) ·
𝑤)) ·
((abs‘𝑥) / 2)) =
(if(1 ≤ ((abs‘𝑥)
· 𝑤), 1,
((abs‘𝑥) ·
𝑤)) ·
((abs‘𝑥) /
2)) |
| 26 | 25 | reccn2 15633 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈
ℝ+) → ∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤)) |
| 27 | | ovres 7599 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) = (𝑥(abs ∘ − )𝑦)) |
| 28 | | eldifi 4131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ∈
ℂ) |
| 29 | | eldifi 4131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 31 | 30 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑥 − 𝑦))) |
| 32 | | abssub 15365 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 − 𝑦)) = (abs‘(𝑦 − 𝑥))) |
| 33 | 31, 32 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑦 − 𝑥))) |
| 34 | 28, 29, 33 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥(abs
∘ − )𝑦) =
(abs‘(𝑦 − 𝑥))) |
| 35 | 27, 34 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) = (abs‘(𝑦 − 𝑥))) |
| 36 | 35 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → ((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 ↔ (abs‘(𝑦 − 𝑥)) < 𝑎)) |
| 37 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (1 / 𝑧) = (1 / 𝑥)) |
| 38 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑥) ∈
V |
| 39 | 37, 20, 38 | fvmpt 7016 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑥) = (1 / 𝑥)) |
| 40 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (1 / 𝑧) = (1 / 𝑦)) |
| 41 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑦) ∈
V |
| 42 | 40, 20, 41 | fvmpt 7016 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑦) = (1 / 𝑦)) |
| 43 | 39, 42 | oveqan12d 7450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑦)) = ((1 / 𝑥)(abs ∘ − )(1 / 𝑦))) |
| 44 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ≠
0) |
| 45 | 28, 44 | reccld 12036 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (1 / 𝑥) ∈
ℂ) |
| 46 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
| 47 | 29, 46 | reccld 12036 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
| 48 | 30 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑦)) =
(abs‘((1 / 𝑥) −
(1 / 𝑦)))) |
| 49 | | abssub 15365 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
(abs‘((1 / 𝑥) −
(1 / 𝑦))) = (abs‘((1
/ 𝑦) − (1 / 𝑥)))) |
| 50 | 48, 49 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑦)) =
(abs‘((1 / 𝑦) −
(1 / 𝑥)))) |
| 51 | 45, 47, 50 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑦)) = (abs‘((1 / 𝑦) − (1 / 𝑥)))) |
| 52 | 43, 51 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑦)) = (abs‘((1 / 𝑦) − (1 / 𝑥)))) |
| 53 | 52 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → ((((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑦)) < 𝑤 ↔ (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤)) |
| 54 | 36, 53 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) ↔ ((abs‘(𝑦 − 𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤))) |
| 55 | 54 | ralbidva 3176 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (∀𝑦 ∈
(ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) ↔ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤))) |
| 56 | 55 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (∃𝑎 ∈
ℝ+ ∀𝑦 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) ↔ ∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤))) |
| 57 | 56 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈
ℝ+) → (∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((𝑥((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) ↔ ∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤))) |
| 58 | 26, 57 | mpbird 257 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈
ℝ+) → ∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((𝑥((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤)) |
| 59 | 58 | rgen2 3199 |
. . . . . . 7
⊢
∀𝑥 ∈
(ℂ ∖ {0})∀𝑤 ∈ ℝ+ ∃𝑎 ∈ ℝ+
∀𝑦 ∈ (ℂ
∖ {0})((𝑥((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) |
| 60 | | cnxmet 24793 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 61 | | xmetres2 24371 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → ((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖
{0}))) |
| 62 | 60, 14, 61 | mp2an 692 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) ∈ (∞Met‘(ℂ ∖ {0})) |
| 63 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) = ((abs ∘ − ) ↾ ((ℂ ∖ {0}) ×
(ℂ ∖ {0}))) |
| 64 | 10 | cnfldtopn 24802 |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 65 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0})))) = (MetOpen‘((abs ∘ − )
↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
| 66 | 63, 64, 65 | metrest 24537 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → (𝐽
↾t (ℂ ∖ {0})) = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))))) |
| 67 | 60, 14, 66 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐽 ↾t (ℂ
∖ {0})) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))) |
| 68 | 13, 67 | eqtri 2765 |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
| 69 | 68, 64 | metcn 24556 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) ∈ (∞Met‘(ℂ ∖ {0})) ∧ (abs ∘
− ) ∈ (∞Met‘ℂ)) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧)) ∈ (𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧)):(ℂ ∖
{0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑤 ∈ ℝ+
∃𝑎 ∈
ℝ+ ∀𝑦 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤)))) |
| 70 | 62, 60, 69 | mp2an 692 |
. . . . . . 7
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧)):(ℂ ∖
{0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑤 ∈ ℝ+
∃𝑎 ∈
ℝ+ ∀𝑦 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤))) |
| 71 | 24, 59, 70 | mpbir2an 711 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) |
| 72 | 71 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽)) |
| 73 | 12, 17, 19, 17, 72, 40 | cnmpt21 23679 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (1 / 𝑦))
∈ ((𝐽
×t 𝐾) Cn
𝐽)) |
| 74 | 10 | mpomulcn 24891 |
. . . . 5
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
| 75 | 74 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
| 76 | | oveq12 7440 |
. . . 4
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (1 / 𝑦)) → (𝑢 · 𝑣) = (𝑥 · (1 / 𝑦))) |
| 77 | 12, 17, 18, 73, 12, 12, 75, 76 | cnmpt22 23682 |
. . 3
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (𝑥 · (1
/ 𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
| 78 | 77 | mptru 1547 |
. 2
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽) |
| 79 | 9, 78 | eqeltri 2837 |
1
⊢ / ∈
((𝐽 ×t
𝐾) Cn 𝐽) |