This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addinvcom

Description: A number commutes with its additive inverse. Compare remulinvcom . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses addinvcom.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
addinvcom.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
addinvcom.1 ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = 0 )
Assertion addinvcom ( 𝜑 → ( 𝐵 + 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 addinvcom.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 addinvcom.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 addinvcom.1 ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = 0 )
4 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
5 simpl ⊢ ( ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) → ( 𝐴 + 𝑥 ) = 0 )
6 5 rgenw ⊢ ∀ 𝑥 ∈ ℂ ( ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) → ( 𝐴 + 𝑥 ) = 0 )
7 6 a1i ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) → ( 𝐴 + 𝑥 ) = 0 ) )
8 sn-negex12 ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) )
9 1 8 syl ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) )
10 0cn ⊢ 0 ∈ ℂ
11 sn-subeu ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
12 1 10 11 sylancl ⊢ ( 𝜑 → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
13 riotass2 ⊢ ( ( ( ℂ ⊆ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) → ( 𝐴 + 𝑥 ) = 0 ) ) ∧ ( ∃ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ∧ ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) ) → ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) = ( ℩ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) )
14 4 7 9 12 13 syl22anc ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) = ( ℩ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) )
15 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 + 𝑥 ) = ( 𝐴 + 𝐵 ) )
16 15 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 + 𝑥 ) = 0 ↔ ( 𝐴 + 𝐵 ) = 0 ) )
17 16 riota2 ⊢ ( ( 𝐵 ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ ( ℩ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) = 𝐵 ) )
18 2 12 17 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 0 ↔ ( ℩ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) = 𝐵 ) )
19 3 18 mpbid ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) = 𝐵 )
20 14 19 eqtrd ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) = 𝐵 )
21 reurmo ⊢ ( ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 → ∃* 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
22 5 rmoimi ⊢ ( ∃* 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 → ∃* 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) )
23 12 21 22 3syl ⊢ ( 𝜑 → ∃* 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) )
24 reu5 ⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ↔ ( ∃ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ∧ ∃* 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) )
25 9 23 24 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) )
26 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 + 𝐴 ) = ( 𝐵 + 𝐴 ) )
27 26 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 + 𝐴 ) = 0 ↔ ( 𝐵 + 𝐴 ) = 0 ) )
28 16 27 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ↔ ( ( 𝐴 + 𝐵 ) = 0 ∧ ( 𝐵 + 𝐴 ) = 0 ) ) )
29 28 riota2 ⊢ ( ( 𝐵 ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( ( ( 𝐴 + 𝐵 ) = 0 ∧ ( 𝐵 + 𝐴 ) = 0 ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) = 𝐵 ) )
30 2 25 29 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) = 0 ∧ ( 𝐵 + 𝐴 ) = 0 ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝐴 ) = 0 ) ) = 𝐵 ) )
31 20 30 mpbird ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 0 ∧ ( 𝐵 + 𝐴 ) = 0 ) )
32 31 simprd ⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = 0 )