Step | Hyp | Ref
| Expression |
1 | | df-div 11903 |
. . 3
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) |
2 | | eldifsn 4791 |
. . . . 5
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
3 | | divval 11905 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) |
4 | | divrec 11919 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (𝑥 · (1 / 𝑦))) |
5 | 3, 4 | eqtr3d 2770 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
6 | 5 | 3expb 1118 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
7 | 2, 6 | sylan2b 593 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
8 | 7 | mpoeq3ia 7498 |
. . 3
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦))) |
9 | 1, 8 | eqtri 2756 |
. 2
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) |
10 | | mpomulcn.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
11 | 10 | cnfldtopon 24712 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐽 ∈
(TopOn‘ℂ)) |
13 | | divcn.k |
. . . . 5
⊢ 𝐾 = (𝐽 ↾t (ℂ ∖
{0})) |
14 | | difss 4130 |
. . . . . 6
⊢ (ℂ
∖ {0}) ⊆ ℂ |
15 | | resttopon 23078 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾t (ℂ ∖ {0}))
∈ (TopOn‘(ℂ ∖ {0}))) |
16 | 12, 14, 15 | sylancl 585 |
. . . . 5
⊢ (⊤
→ (𝐽
↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖
{0}))) |
17 | 13, 16 | eqeltrid 2833 |
. . . 4
⊢ (⊤
→ 𝐾 ∈
(TopOn‘(ℂ ∖ {0}))) |
18 | 12, 17 | cnmpt1st 23585 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑥) ∈
((𝐽 ×t
𝐾) Cn 𝐽)) |
19 | 12, 17 | cnmpt2nd 23586 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑦) ∈
((𝐽 ×t
𝐾) Cn 𝐾)) |
20 | | eqid 2728 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) |
21 | | eldifi 4125 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
22 | | eldifsni 4794 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
23 | 21, 22 | reccld 12014 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (1 / 𝑧) ∈
ℂ) |
24 | 20, 23 | fmpti 7122 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)):(ℂ
∖ {0})⟶ℂ |
25 | | eqid 2728 |
. . . . . . . . . 10
⊢ (if(1
≤ ((abs‘𝑥)
· 𝑤), 1,
((abs‘𝑥) ·
𝑤)) ·
((abs‘𝑥) / 2)) =
(if(1 ≤ ((abs‘𝑥)
· 𝑤), 1,
((abs‘𝑥) ·
𝑤)) ·
((abs‘𝑥) /
2)) |
26 | 25 | reccn2 15574 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈
ℝ+) → ∃𝑎 ∈ ℝ+ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤)) |
27 | | ovres 7587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) = (𝑥(abs ∘ − )𝑦)) |
28 | | eldifi 4125 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ∈
ℂ) |
29 | | eldifi 4125 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
30 | | eqid 2728 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
31 | 30 | cnmetdval 24700 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑥 − 𝑦))) |
32 | | abssub 15306 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 − 𝑦)) = (abs‘(𝑦 − 𝑥))) |
33 | 31, 32 | eqtrd 2768 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑦 − 𝑥))) |
34 | 28, 29, 33 | syl2an 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥(abs
∘ − )𝑦) =
(abs‘(𝑦 − 𝑥))) |
35 | 27, 34 | eqtrd 2768 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) = (abs‘(𝑦 − 𝑥))) |
36 | 35 | breq1d 5158 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → ((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 ↔ (abs‘(𝑦 − 𝑥)) < 𝑎)) |
37 | | oveq2 7428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (1 / 𝑧) = (1 / 𝑥)) |
38 | | ovex 7453 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑥) ∈
V |
39 | 37, 20, 38 | fvmpt 7005 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑥) = (1 / 𝑥)) |
40 | | oveq2 7428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (1 / 𝑧) = (1 / 𝑦)) |
41 | | ovex 7453 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑦) ∈
V |
42 | 40, 20, 41 | fvmpt 7005 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑦) = (1 / 𝑦)) |
43 | 39, 42 | oveqan12d 7439 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑦)) = ((1 / 𝑥)(abs ∘ − )(1 / 𝑦))) |
44 | | eldifsni 4794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ≠
0) |
45 | 28, 44 | reccld 12014 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (1 / 𝑥) ∈
ℂ) |
46 | | eldifsni 4794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
47 | 29, 46 | reccld 12014 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
48 | 30 | cnmetdval 24700 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑦)) =
(abs‘((1 / 𝑥) −
(1 / 𝑦)))) |
49 | | abssub 15306 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
(abs‘((1 / 𝑥) −
(1 / 𝑦))) = (abs‘((1
/ 𝑦) − (1 / 𝑥)))) |
50 | 48, 49 | eqtrd 2768 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑦) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑦)) =
(abs‘((1 / 𝑦) −
(1 / 𝑥)))) |
51 | 45, 47, 50 | syl2an 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑦)) = (abs‘((1 / 𝑦) − (1 / 𝑥)))) |
52 | 43, 51 | eqtrd 2768 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑦)) = (abs‘((1 / 𝑦) − (1 / 𝑥)))) |
53 | 52 | breq1d 5158 |
. . . . . . . . . . . . 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 3172 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (∀𝑦 ∈
(ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) ↔ ∀𝑦 ∈ (ℂ ∖
{0})((abs‘(𝑦 −
𝑥)) < 𝑎 → (abs‘((1 / 𝑦) − (1 / 𝑥))) < 𝑤))) |
56 | 55 | rexbidv 3175 |
. . . . . . . . . 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 3194 |
. . . . . . 7
⊢
∀𝑥 ∈
(ℂ ∖ {0})∀𝑤 ∈ ℝ+ ∃𝑎 ∈ ℝ+
∀𝑦 ∈ (ℂ
∖ {0})((𝑥((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤) |
60 | | cnxmet 24702 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
61 | | xmetres2 24280 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → ((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖
{0}))) |
62 | 60, 14, 61 | mp2an 691 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) ∈ (∞Met‘(ℂ ∖ {0})) |
63 | | eqid 2728 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) = ((abs ∘ − ) ↾ ((ℂ ∖ {0}) ×
(ℂ ∖ {0}))) |
64 | 10 | cnfldtopn 24711 |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
65 | | eqid 2728 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0})))) = (MetOpen‘((abs ∘ − )
↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
66 | 63, 64, 65 | metrest 24446 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → (𝐽
↾t (ℂ ∖ {0})) = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))))) |
67 | 60, 14, 66 | mp2an 691 |
. . . . . . . . . 10
⊢ (𝐽 ↾t (ℂ
∖ {0})) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))) |
68 | 13, 67 | eqtri 2756 |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
69 | 68, 64 | metcn 24465 |
. . . . . . . 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 691 |
. . . . . . 7
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧)):(ℂ ∖
{0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑤 ∈ ℝ+
∃𝑎 ∈
ℝ+ ∀𝑦 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑦) < 𝑎 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑦)) < 𝑤))) |
71 | 24, 59, 70 | mpbir2an 710 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) |
72 | 71 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽)) |
73 | 12, 17, 19, 17, 72, 40 | cnmpt21 23588 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (1 / 𝑦))
∈ ((𝐽
×t 𝐾) Cn
𝐽)) |
74 | 10 | mpomulcn 24798 |
. . . . 5
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
75 | 74 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
76 | | oveq12 7429 |
. . . 4
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (1 / 𝑦)) → (𝑢 · 𝑣) = (𝑥 · (1 / 𝑦))) |
77 | 12, 17, 18, 73, 12, 12, 75, 76 | cnmpt22 23591 |
. . 3
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (𝑥 · (1
/ 𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
78 | 77 | mptru 1541 |
. 2
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽) |
79 | 9, 78 | eqeltri 2825 |
1
⊢ / ∈
((𝐽 ×t
𝐾) Cn 𝐽) |