Step | Hyp | Ref
| Expression |
1 | | moeq 3704 |
. . . . . . . . 9
⊢
∃*𝑧 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩ |
2 | 1 | mosubop 5512 |
. . . . . . . 8
⊢
∃*𝑧∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) |
3 | 2 | mosubop 5512 |
. . . . . . 7
⊢
∃*𝑧∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)) |
4 | | anass 470 |
. . . . . . . . . . 11
⊢ (((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
5 | 4 | 2exbii 1852 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) ↔ ∃𝑢∃𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
6 | | 19.42vv 1962 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
7 | 5, 6 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) ↔ (𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
8 | 7 | 2exbii 1852 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) ↔ ∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
9 | 8 | mobii 2543 |
. . . . . . 7
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) ↔ ∃*𝑧∃𝑤∃𝑣(𝑥 = ⟨𝑤, 𝑣⟩ ∧ ∃𝑢∃𝑓(𝑦 = ⟨𝑢, 𝑓⟩ ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))) |
10 | 3, 9 | mpbir 230 |
. . . . . 6
⊢
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩) |
11 | 10 | moani 2548 |
. . . . 5
⊢
∃*𝑧((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)) |
12 | 11 | funoprab 7530 |
. . . 4
⊢ Fun
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
13 | | df-add 11121 |
. . . . 5
⊢ + =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
14 | 13 | funeqi 6570 |
. . . 4
⊢ (Fun +
↔ Fun {⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}) |
15 | 12, 14 | mpbir 230 |
. . 3
⊢ Fun
+ |
16 | 13 | dmeqi 5905 |
. . . . 5
⊢ dom + =
dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
17 | | dmoprabss 7511 |
. . . . 5
⊢ dom
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} ⊆ (ℂ
× ℂ) |
18 | 16, 17 | eqsstri 4017 |
. . . 4
⊢ dom +
⊆ (ℂ × ℂ) |
19 | | 0ncn 11128 |
. . . . 5
⊢ ¬
∅ ∈ ℂ |
20 | | df-c 11116 |
. . . . . . 7
⊢ ℂ =
(R × R) |
21 | | oveq1 7416 |
. . . . . . . 8
⊢
(⟨𝑧, 𝑤⟩ = 𝑥 → (⟨𝑧, 𝑤⟩ + ⟨𝑣, 𝑢⟩) = (𝑥 + ⟨𝑣, 𝑢⟩)) |
22 | 21 | eleq1d 2819 |
. . . . . . 7
⊢
(⟨𝑧, 𝑤⟩ = 𝑥 → ((⟨𝑧, 𝑤⟩ + ⟨𝑣, 𝑢⟩) ∈ (R ×
R) ↔ (𝑥
+ ⟨𝑣, 𝑢⟩) ∈ (R
× R))) |
23 | | oveq2 7417 |
. . . . . . . 8
⊢
(⟨𝑣, 𝑢⟩ = 𝑦 → (𝑥 + ⟨𝑣, 𝑢⟩) = (𝑥 + 𝑦)) |
24 | 23 | eleq1d 2819 |
. . . . . . 7
⊢
(⟨𝑣, 𝑢⟩ = 𝑦 → ((𝑥 + ⟨𝑣, 𝑢⟩) ∈ (R ×
R) ↔ (𝑥
+ 𝑦) ∈
(R × R))) |
25 | | addcnsr 11130 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (⟨𝑧, 𝑤⟩ + ⟨𝑣, 𝑢⟩) = ⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩) |
26 | | addclsr 11078 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
+R 𝑣) ∈ R) |
27 | | addclsr 11078 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
+R 𝑢) ∈ R) |
28 | 26, 27 | anim12i 614 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
29 | 28 | an4s 659 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
30 | | opelxpi 5714 |
. . . . . . . . 9
⊢ (((𝑧 +R
𝑣) ∈ R
∧ (𝑤
+R 𝑢) ∈ R) → ⟨(𝑧 +R
𝑣), (𝑤 +R 𝑢)⟩ ∈ (R
× R)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩ ∈ (R
× R)) |
32 | 25, 31 | eqeltrd 2834 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (⟨𝑧, 𝑤⟩ + ⟨𝑣, 𝑢⟩) ∈ (R ×
R)) |
33 | 20, 22, 24, 32 | 2optocl 5772 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ (R ×
R)) |
34 | 33, 20 | eleqtrrdi 2845 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
35 | 19, 34 | oprssdm 7588 |
. . . 4
⊢ (ℂ
× ℂ) ⊆ dom + |
36 | 18, 35 | eqssi 3999 |
. . 3
⊢ dom + =
(ℂ × ℂ) |
37 | | df-fn 6547 |
. . 3
⊢ ( + Fn
(ℂ × ℂ) ↔ (Fun + ∧ dom + = (ℂ ×
ℂ))) |
38 | 15, 36, 37 | mpbir2an 710 |
. 2
⊢ + Fn
(ℂ × ℂ) |
39 | 34 | rgen2 3198 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (𝑥 + 𝑦) ∈
ℂ |
40 | | ffnov 7535 |
. 2
⊢ ( +
:(ℂ × ℂ)⟶ℂ ↔ ( + Fn (ℂ ×
ℂ) ∧ ∀𝑥
∈ ℂ ∀𝑦
∈ ℂ (𝑥 + 𝑦) ∈
ℂ)) |
41 | 38, 39, 40 | mpbir2an 710 |
1
⊢ +
:(ℂ × ℂ)⟶ℂ |