Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . . . . 8
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → x ∈ ℝ) |
2 | 1 | recnd 6851 |
. . . . . . 7
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → x ∈ ℂ) |
3 | | ax-icn 6778 |
. . . . . . . . 9
⊢ i ∈ ℂ |
4 | 3 | a1i 9 |
. . . . . . . 8
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → i ∈ ℂ) |
5 | | simpr 103 |
. . . . . . . . 9
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → y ∈ ℝ) |
6 | 5 | recnd 6851 |
. . . . . . . 8
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → y ∈ ℂ) |
7 | 4, 6 | mulcld 6845 |
. . . . . . 7
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → (i · y) ∈ ℂ) |
8 | 2, 7 | addcld 6844 |
. . . . . 6
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → (x + (i · y)) ∈
ℂ) |
9 | 8 | rgen2a 2369 |
. . . . 5
⊢ ∀x ∈ ℝ ∀y ∈ ℝ (x +
(i · y)) ∈ ℂ |
10 | | cnref1o.1 |
. . . . . 6
⊢ 𝐹 = (x ∈ ℝ,
y ∈
ℝ ↦ (x + (i · y))) |
11 | 10 | fnmpt2 5770 |
. . . . 5
⊢ (∀x ∈ ℝ ∀y ∈ ℝ (x +
(i · y)) ∈ ℂ → 𝐹 Fn (ℝ ×
ℝ)) |
12 | 9, 11 | ax-mp 7 |
. . . 4
⊢ 𝐹 Fn (ℝ ×
ℝ) |
13 | | 1st2nd2 5743 |
. . . . . . . . 9
⊢ (z ∈ (ℝ
× ℝ) → z =
〈(1st ‘z),
(2nd ‘z)〉) |
14 | 13 | fveq2d 5125 |
. . . . . . . 8
⊢ (z ∈ (ℝ
× ℝ) → (𝐹‘z) = (𝐹‘〈(1st ‘z), (2nd ‘z)〉)) |
15 | | df-ov 5458 |
. . . . . . . 8
⊢
((1st ‘z)𝐹(2nd ‘z)) = (𝐹‘〈(1st ‘z), (2nd ‘z)〉) |
16 | 14, 15 | syl6eqr 2087 |
. . . . . . 7
⊢ (z ∈ (ℝ
× ℝ) → (𝐹‘z) = ((1st ‘z)𝐹(2nd ‘z))) |
17 | | xp1st 5734 |
. . . . . . . 8
⊢ (z ∈ (ℝ
× ℝ) → (1st ‘z) ∈
ℝ) |
18 | | xp2nd 5735 |
. . . . . . . 8
⊢ (z ∈ (ℝ
× ℝ) → (2nd ‘z) ∈
ℝ) |
19 | 17 | recnd 6851 |
. . . . . . . . 9
⊢ (z ∈ (ℝ
× ℝ) → (1st ‘z) ∈
ℂ) |
20 | 3 | a1i 9 |
. . . . . . . . . 10
⊢ (z ∈ (ℝ
× ℝ) → i ∈
ℂ) |
21 | 18 | recnd 6851 |
. . . . . . . . . 10
⊢ (z ∈ (ℝ
× ℝ) → (2nd ‘z) ∈
ℂ) |
22 | 20, 21 | mulcld 6845 |
. . . . . . . . 9
⊢ (z ∈ (ℝ
× ℝ) → (i · (2nd ‘z)) ∈
ℂ) |
23 | 19, 22 | addcld 6844 |
. . . . . . . 8
⊢ (z ∈ (ℝ
× ℝ) → ((1st ‘z) + (i · (2nd ‘z))) ∈
ℂ) |
24 | | oveq1 5462 |
. . . . . . . . 9
⊢ (x = (1st ‘z) → (x +
(i · y)) = ((1st
‘z) + (i · y))) |
25 | | oveq2 5463 |
. . . . . . . . . 10
⊢ (y = (2nd ‘z) → (i · y) = (i · (2nd ‘z))) |
26 | 25 | oveq2d 5471 |
. . . . . . . . 9
⊢ (y = (2nd ‘z) → ((1st ‘z) + (i · y)) = ((1st ‘z) + (i · (2nd ‘z)))) |
27 | 24, 26, 10 | ovmpt2g 5577 |
. . . . . . . 8
⊢
(((1st ‘z) ∈ ℝ ∧
(2nd ‘z) ∈ ℝ ∧
((1st ‘z) + (i ·
(2nd ‘z))) ∈ ℂ) → ((1st ‘z)𝐹(2nd ‘z)) = ((1st ‘z) + (i · (2nd ‘z)))) |
28 | 17, 18, 23, 27 | syl3anc 1134 |
. . . . . . 7
⊢ (z ∈ (ℝ
× ℝ) → ((1st ‘z)𝐹(2nd ‘z)) = ((1st ‘z) + (i · (2nd ‘z)))) |
29 | 16, 28 | eqtrd 2069 |
. . . . . 6
⊢ (z ∈ (ℝ
× ℝ) → (𝐹‘z) = ((1st ‘z) + (i · (2nd ‘z)))) |
30 | 29, 23 | eqeltrd 2111 |
. . . . 5
⊢ (z ∈ (ℝ
× ℝ) → (𝐹‘z) ∈
ℂ) |
31 | 30 | rgen 2368 |
. . . 4
⊢ ∀z ∈ (ℝ × ℝ)(𝐹‘z) ∈
ℂ |
32 | | ffnfv 5266 |
. . . 4
⊢ (𝐹:(ℝ ×
ℝ)⟶ℂ ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀z ∈ (ℝ
× ℝ)(𝐹‘z) ∈
ℂ)) |
33 | 12, 31, 32 | mpbir2an 848 |
. . 3
⊢ 𝐹:(ℝ ×
ℝ)⟶ℂ |
34 | 17, 18 | jca 290 |
. . . . . . 7
⊢ (z ∈ (ℝ
× ℝ) → ((1st ‘z) ∈ ℝ ∧ (2nd ‘z) ∈
ℝ)) |
35 | | xp1st 5734 |
. . . . . . . 8
⊢ (w ∈ (ℝ
× ℝ) → (1st ‘w) ∈
ℝ) |
36 | | xp2nd 5735 |
. . . . . . . 8
⊢ (w ∈ (ℝ
× ℝ) → (2nd ‘w) ∈
ℝ) |
37 | 35, 36 | jca 290 |
. . . . . . 7
⊢ (w ∈ (ℝ
× ℝ) → ((1st ‘w) ∈ ℝ ∧ (2nd ‘w) ∈
ℝ)) |
38 | | cru 7386 |
. . . . . . 7
⊢
((((1st ‘z) ∈ ℝ ∧
(2nd ‘z) ∈ ℝ) ∧
((1st ‘w) ∈ ℝ ∧
(2nd ‘w) ∈ ℝ)) → (((1st
‘z) + (i · (2nd
‘z))) = ((1st
‘w) + (i · (2nd
‘w))) ↔ ((1st
‘z) = (1st ‘w) ∧
(2nd ‘z) = (2nd
‘w)))) |
39 | 34, 37, 38 | syl2an 273 |
. . . . . 6
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) →
(((1st ‘z) + (i ·
(2nd ‘z))) =
((1st ‘w) + (i ·
(2nd ‘w))) ↔
((1st ‘z) =
(1st ‘w) ∧ (2nd ‘z) = (2nd ‘w)))) |
40 | | fveq2 5121 |
. . . . . . . . 9
⊢ (z = w →
(𝐹‘z) = (𝐹‘w)) |
41 | | fveq2 5121 |
. . . . . . . . . 10
⊢ (z = w →
(1st ‘z) = (1st
‘w)) |
42 | | fveq2 5121 |
. . . . . . . . . . 11
⊢ (z = w →
(2nd ‘z) = (2nd
‘w)) |
43 | 42 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (z = w → (i
· (2nd ‘z)) = (i
· (2nd ‘w))) |
44 | 41, 43 | oveq12d 5473 |
. . . . . . . . 9
⊢ (z = w →
((1st ‘z) + (i ·
(2nd ‘z))) =
((1st ‘w) + (i ·
(2nd ‘w)))) |
45 | 40, 44 | eqeq12d 2051 |
. . . . . . . 8
⊢ (z = w →
((𝐹‘z) = ((1st ‘z) + (i · (2nd ‘z))) ↔ (𝐹‘w) = ((1st ‘w) + (i · (2nd ‘w))))) |
46 | 45, 29 | vtoclga 2613 |
. . . . . . 7
⊢ (w ∈ (ℝ
× ℝ) → (𝐹‘w) = ((1st ‘w) + (i · (2nd ‘w)))) |
47 | 29, 46 | eqeqan12d 2052 |
. . . . . 6
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) → ((𝐹‘z) = (𝐹‘w) ↔ ((1st ‘z) + (i · (2nd ‘z))) = ((1st ‘w) + (i · (2nd ‘w))))) |
48 | | 1st2nd2 5743 |
. . . . . . . 8
⊢ (w ∈ (ℝ
× ℝ) → w =
〈(1st ‘w),
(2nd ‘w)〉) |
49 | 13, 48 | eqeqan12d 2052 |
. . . . . . 7
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) → (z = w ↔
〈(1st ‘z),
(2nd ‘z)〉 =
〈(1st ‘w),
(2nd ‘w)〉)) |
50 | | vex 2554 |
. . . . . . . . 9
⊢ z ∈
V |
51 | | 1stexg 5736 |
. . . . . . . . 9
⊢ (z ∈ V →
(1st ‘z) ∈ V) |
52 | 50, 51 | ax-mp 7 |
. . . . . . . 8
⊢
(1st ‘z) ∈ V |
53 | | 2ndexg 5737 |
. . . . . . . . 9
⊢ (z ∈ V →
(2nd ‘z) ∈ V) |
54 | 50, 53 | ax-mp 7 |
. . . . . . . 8
⊢
(2nd ‘z) ∈ V |
55 | 52, 54 | opth 3965 |
. . . . . . 7
⊢
(〈(1st ‘z),
(2nd ‘z)〉 =
〈(1st ‘w),
(2nd ‘w)〉 ↔
((1st ‘z) =
(1st ‘w) ∧ (2nd ‘z) = (2nd ‘w))) |
56 | 49, 55 | syl6bb 185 |
. . . . . 6
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) → (z = w ↔
((1st ‘z) =
(1st ‘w) ∧ (2nd ‘z) = (2nd ‘w)))) |
57 | 39, 47, 56 | 3bitr4d 209 |
. . . . 5
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) → ((𝐹‘z) = (𝐹‘w) ↔ z =
w)) |
58 | 57 | biimpd 132 |
. . . 4
⊢
((z ∈ (ℝ × ℝ) ∧ w ∈ (ℝ × ℝ)) → ((𝐹‘z) = (𝐹‘w) → z =
w)) |
59 | 58 | rgen2a 2369 |
. . 3
⊢ ∀z ∈ (ℝ × ℝ)∀w ∈ (ℝ × ℝ)((𝐹‘z) = (𝐹‘w) → z =
w) |
60 | | dff13 5350 |
. . 3
⊢ (𝐹:(ℝ ×
ℝ)–1-1→ℂ ↔
(𝐹:(ℝ ×
ℝ)⟶ℂ ∧ ∀z ∈ (ℝ × ℝ)∀w ∈ (ℝ × ℝ)((𝐹‘z) = (𝐹‘w) → z =
w))) |
61 | 33, 59, 60 | mpbir2an 848 |
. 2
⊢ 𝐹:(ℝ ×
ℝ)–1-1→ℂ |
62 | | cnre 6821 |
. . . . . 6
⊢ (w ∈ ℂ →
∃u ∈ ℝ ∃v ∈ ℝ w =
(u + (i · v))) |
63 | | simpl 102 |
. . . . . . . . 9
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → u ∈ ℝ) |
64 | | simpr 103 |
. . . . . . . . 9
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → v ∈ ℝ) |
65 | 63 | recnd 6851 |
. . . . . . . . . 10
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → u ∈ ℂ) |
66 | 3 | a1i 9 |
. . . . . . . . . . 11
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → i ∈ ℂ) |
67 | 64 | recnd 6851 |
. . . . . . . . . . 11
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → v ∈ ℂ) |
68 | 66, 67 | mulcld 6845 |
. . . . . . . . . 10
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → (i · v) ∈ ℂ) |
69 | 65, 68 | addcld 6844 |
. . . . . . . . 9
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → (u + (i · v)) ∈
ℂ) |
70 | | oveq1 5462 |
. . . . . . . . . 10
⊢ (x = u →
(x + (i · y)) = (u + (i
· y))) |
71 | | oveq2 5463 |
. . . . . . . . . . 11
⊢ (y = v → (i
· y) = (i · v)) |
72 | 71 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (y = v →
(u + (i · y)) = (u + (i
· v))) |
73 | 70, 72, 10 | ovmpt2g 5577 |
. . . . . . . . 9
⊢
((u ∈ ℝ ∧
v ∈
ℝ ∧ (u + (i · v)) ∈ ℂ)
→ (u𝐹v) =
(u + (i · v))) |
74 | 63, 64, 69, 73 | syl3anc 1134 |
. . . . . . . 8
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → (u𝐹v) =
(u + (i · v))) |
75 | 74 | eqeq2d 2048 |
. . . . . . 7
⊢
((u ∈ ℝ ∧
v ∈
ℝ) → (w = (u𝐹v)
↔ w = (u + (i · v)))) |
76 | 75 | 2rexbiia 2334 |
. . . . . 6
⊢ (∃u ∈ ℝ ∃v ∈ ℝ w =
(u𝐹v)
↔ ∃u ∈ ℝ ∃v ∈ ℝ w =
(u + (i · v))) |
77 | 62, 76 | sylibr 137 |
. . . . 5
⊢ (w ∈ ℂ →
∃u ∈ ℝ ∃v ∈ ℝ w =
(u𝐹v)) |
78 | | fveq2 5121 |
. . . . . . . 8
⊢ (z = 〈u,
v〉 → (𝐹‘z) = (𝐹‘〈u, v〉)) |
79 | | df-ov 5458 |
. . . . . . . 8
⊢ (u𝐹v) =
(𝐹‘〈u, v〉) |
80 | 78, 79 | syl6eqr 2087 |
. . . . . . 7
⊢ (z = 〈u,
v〉 → (𝐹‘z) = (u𝐹v)) |
81 | 80 | eqeq2d 2048 |
. . . . . 6
⊢ (z = 〈u,
v〉 → (w = (𝐹‘z) ↔ w =
(u𝐹v))) |
82 | 81 | rexxp 4423 |
. . . . 5
⊢ (∃z ∈ (ℝ × ℝ)w = (𝐹‘z) ↔ ∃u ∈ ℝ ∃v ∈ ℝ w =
(u𝐹v)) |
83 | 77, 82 | sylibr 137 |
. . . 4
⊢ (w ∈ ℂ →
∃z ∈ (ℝ × ℝ)w = (𝐹‘z)) |
84 | 83 | rgen 2368 |
. . 3
⊢ ∀w ∈ ℂ ∃z ∈ (ℝ × ℝ)w = (𝐹‘z) |
85 | | dffo3 5257 |
. . 3
⊢ (𝐹:(ℝ ×
ℝ)–onto→ℂ ↔
(𝐹:(ℝ ×
ℝ)⟶ℂ ∧ ∀w ∈ ℂ ∃z ∈ (ℝ × ℝ)w = (𝐹‘z))) |
86 | 33, 84, 85 | mpbir2an 848 |
. 2
⊢ 𝐹:(ℝ ×
ℝ)–onto→ℂ |
87 | | df-f1o 4852 |
. 2
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ ↔ (𝐹:(ℝ × ℝ)–1-1→ℂ ∧ 𝐹:(ℝ × ℝ)–onto→ℂ)) |
88 | 61, 86, 87 | mpbir2an 848 |
1
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ |