| Step | Hyp | Ref
| Expression |
| 1 | | moeq 3713 |
. . . . . . . . 9
⊢
∃*𝑧 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉 |
| 2 | 1 | mosubop 5516 |
. . . . . . . 8
⊢
∃*𝑧∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) |
| 3 | 2 | mosubop 5516 |
. . . . . . 7
⊢
∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉)) |
| 4 | | anass 468 |
. . . . . . . . . . 11
⊢ (((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 5 | 4 | 2exbii 1849 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) ↔ ∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 6 | | 19.42vv 1957 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = 〈𝑤, 𝑣〉 ∧ (𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉)) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 7 | 5, 6 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) ↔ (𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 8 | 7 | 2exbii 1849 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) ↔ ∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 9 | 8 | mobii 2548 |
. . . . . . 7
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) ↔ ∃*𝑧∃𝑤∃𝑣(𝑥 = 〈𝑤, 𝑣〉 ∧ ∃𝑢∃𝑓(𝑦 = 〈𝑢, 𝑓〉 ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))) |
| 10 | 3, 9 | mpbir 231 |
. . . . . 6
⊢
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉) |
| 11 | 10 | moani 2553 |
. . . . 5
⊢
∃*𝑧((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉)) |
| 12 | 11 | funoprab 7555 |
. . . 4
⊢ Fun
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} |
| 13 | | df-add 11166 |
. . . . 5
⊢ + =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} |
| 14 | 13 | funeqi 6587 |
. . . 4
⊢ (Fun +
↔ Fun {〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))}) |
| 15 | 12, 14 | mpbir 231 |
. . 3
⊢ Fun
+ |
| 16 | 13 | dmeqi 5915 |
. . . . 5
⊢ dom + =
dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} |
| 17 | | dmoprabss 7537 |
. . . . 5
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} ⊆ (ℂ
× ℂ) |
| 18 | 16, 17 | eqsstri 4030 |
. . . 4
⊢ dom +
⊆ (ℂ × ℂ) |
| 19 | | 0ncn 11173 |
. . . . 5
⊢ ¬
∅ ∈ ℂ |
| 20 | | df-c 11161 |
. . . . . . 7
⊢ ℂ =
(R × R) |
| 21 | | oveq1 7438 |
. . . . . . . 8
⊢
(〈𝑧, 𝑤〉 = 𝑥 → (〈𝑧, 𝑤〉 + 〈𝑣, 𝑢〉) = (𝑥 + 〈𝑣, 𝑢〉)) |
| 22 | 21 | eleq1d 2826 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 𝑥 → ((〈𝑧, 𝑤〉 + 〈𝑣, 𝑢〉) ∈ (R ×
R) ↔ (𝑥
+ 〈𝑣, 𝑢〉) ∈ (R
× R))) |
| 23 | | oveq2 7439 |
. . . . . . . 8
⊢
(〈𝑣, 𝑢〉 = 𝑦 → (𝑥 + 〈𝑣, 𝑢〉) = (𝑥 + 𝑦)) |
| 24 | 23 | eleq1d 2826 |
. . . . . . 7
⊢
(〈𝑣, 𝑢〉 = 𝑦 → ((𝑥 + 〈𝑣, 𝑢〉) ∈ (R ×
R) ↔ (𝑥
+ 𝑦) ∈
(R × R))) |
| 25 | | addcnsr 11175 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (〈𝑧, 𝑤〉 + 〈𝑣, 𝑢〉) = 〈(𝑧 +R 𝑣), (𝑤 +R 𝑢)〉) |
| 26 | | addclsr 11123 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
+R 𝑣) ∈ R) |
| 27 | | addclsr 11123 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
+R 𝑢) ∈ R) |
| 28 | 26, 27 | anim12i 613 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
| 29 | 28 | an4s 660 |
. . . . . . . . 9
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
| 30 | | opelxpi 5722 |
. . . . . . . . 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 2841 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (〈𝑧, 𝑤〉 + 〈𝑣, 𝑢〉) ∈ (R ×
R)) |
| 33 | 20, 22, 24, 32 | 2optocl 5781 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ (R ×
R)) |
| 34 | 33, 20 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
| 35 | 19, 34 | oprssdm 7614 |
. . . 4
⊢ (ℂ
× ℂ) ⊆ dom + |
| 36 | 18, 35 | eqssi 4000 |
. . 3
⊢ dom + =
(ℂ × ℂ) |
| 37 | | df-fn 6564 |
. . 3
⊢ ( + Fn
(ℂ × ℂ) ↔ (Fun + ∧ dom + = (ℂ ×
ℂ))) |
| 38 | 15, 36, 37 | mpbir2an 711 |
. 2
⊢ + Fn
(ℂ × ℂ) |
| 39 | 34 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (𝑥 + 𝑦) ∈
ℂ |
| 40 | | ffnov 7559 |
. 2
⊢ ( +
:(ℂ × ℂ)⟶ℂ ↔ ( + Fn (ℂ ×
ℂ) ∧ ∀𝑥
∈ ℂ ∀𝑦
∈ ℂ (𝑥 + 𝑦) ∈
ℂ)) |
| 41 | 38, 39, 40 | mpbir2an 711 |
1
⊢ +
:(ℂ × ℂ)⟶ℂ |