Step | Hyp | Ref
| Expression |
1 | | ssidd 3911 |
. . . . 5
⊢ (𝜑 → ℂ ⊆
ℂ) |
2 | | simpl 487 |
. . . . . . 7
⊢ (((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) → (𝐴 + 𝑥) = 0) |
3 | 2 | rgenw 3080 |
. . . . . 6
⊢
∀𝑥 ∈
ℂ (((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) → (𝐴 + 𝑥) = 0) |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℂ (((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) → (𝐴 + 𝑥) = 0)) |
5 | | addinvcom.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
6 | | sn-negex12 39880 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) |
8 | | 0cn 10656 |
. . . . . 6
⊢ 0 ∈
ℂ |
9 | | sn-subeu 39890 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → ∃!𝑥
∈ ℂ (𝐴 + 𝑥) = 0) |
10 | 5, 8, 9 | sylancl 590 |
. . . . 5
⊢ (𝜑 → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) |
11 | | riotass2 7131 |
. . . . 5
⊢
(((ℂ ⊆ ℂ ∧ ∀𝑥 ∈ ℂ (((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) → (𝐴 + 𝑥) = 0)) ∧ (∃𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) ∧ ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)) → (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) = (℩𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)) |
12 | 1, 4, 7, 10, 11 | syl22anc 838 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) = (℩𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)) |
13 | | addinvcom.1 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝐵) = 0) |
14 | | addinvcom.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
15 | | oveq2 7151 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐴 + 𝑥) = (𝐴 + 𝐵)) |
16 | 15 | eqeq1d 2761 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝐴 + 𝑥) = 0 ↔ (𝐴 + 𝐵) = 0)) |
17 | 16 | riota2 7126 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧
∃!𝑥 ∈ ℂ
(𝐴 + 𝑥) = 0) → ((𝐴 + 𝐵) = 0 ↔ (℩𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) = 𝐵)) |
18 | 14, 10, 17 | syl2anc 588 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵) = 0 ↔ (℩𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) = 𝐵)) |
19 | 13, 18 | mpbid 235 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) = 𝐵) |
20 | 12, 19 | eqtrd 2794 |
. . 3
⊢ (𝜑 → (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) = 𝐵) |
21 | | reurmo 3341 |
. . . . . 6
⊢
(∃!𝑥 ∈
ℂ (𝐴 + 𝑥) = 0 → ∃*𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) |
22 | 2 | rmoimi 3653 |
. . . . . 6
⊢
(∃*𝑥 ∈
ℂ (𝐴 + 𝑥) = 0 → ∃*𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) |
23 | 10, 21, 22 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ∃*𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) |
24 | | reu5 3338 |
. . . . 5
⊢
(∃!𝑥 ∈
ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) ↔ (∃𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) ∧ ∃*𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0))) |
25 | 7, 23, 24 | sylanbrc 587 |
. . . 4
⊢ (𝜑 → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) |
26 | | oveq1 7150 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 + 𝐴) = (𝐵 + 𝐴)) |
27 | 26 | eqeq1d 2761 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 + 𝐴) = 0 ↔ (𝐵 + 𝐴) = 0)) |
28 | 16, 27 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝐵 → (((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0) ↔ ((𝐴 + 𝐵) = 0 ∧ (𝐵 + 𝐴) = 0))) |
29 | 28 | riota2 7126 |
. . . 4
⊢ ((𝐵 ∈ ℂ ∧
∃!𝑥 ∈ ℂ
((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) → (((𝐴 + 𝐵) = 0 ∧ (𝐵 + 𝐴) = 0) ↔ (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) = 𝐵)) |
30 | 14, 25, 29 | syl2anc 588 |
. . 3
⊢ (𝜑 → (((𝐴 + 𝐵) = 0 ∧ (𝐵 + 𝐴) = 0) ↔ (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) = 0 ∧ (𝑥 + 𝐴) = 0)) = 𝐵)) |
31 | 20, 30 | mpbird 260 |
. 2
⊢ (𝜑 → ((𝐴 + 𝐵) = 0 ∧ (𝐵 + 𝐴) = 0)) |
32 | 31 | simprd 500 |
1
⊢ (𝜑 → (𝐵 + 𝐴) = 0) |