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

Metamath Proof Explorer

Theorem cnaddinv

Description: Value of the group inverse of complex number addition. See also cnfldneg . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 26-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g ⊢ G = Base ndx ℂ + ndx +
Assertion cnaddinv ⊢ A ∈ ℂ → inv g ⁡ G ⁡ A = − A

Proof

Step Hyp Ref Expression
1 cnaddabl.g ⊢ G = Base ndx ℂ + ndx +
2 negid ⊢ A ∈ ℂ → A + − A = 0
3 1 cnaddabl ⊢ G ∈ Abel
4 ablgrp ⊢ G ∈ Abel → G ∈ Grp
5 3 4 ax-mp ⊢ G ∈ Grp
6 id ⊢ A ∈ ℂ → A ∈ ℂ
7 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
8 cnex ⊢ ℂ ∈ V
9 1 grpbase ⊢ ℂ ∈ V → ℂ = Base G
10 8 9 ax-mp ⊢ ℂ = Base G
11 addex ⊢ + ∈ V
12 1 grpplusg ⊢ + ∈ V → + = + G
13 11 12 ax-mp ⊢ + = + G
14 1 cnaddid ⊢ 0 G = 0
15 14 eqcomi ⊢ 0 = 0 G
16 eqid ⊢ inv g ⁡ G = inv g ⁡ G
17 10 13 15 16 grpinvid1 ⊢ G ∈ Grp ∧ A ∈ ℂ ∧ − A ∈ ℂ → inv g ⁡ G ⁡ A = − A ↔ A + − A = 0
18 5 6 7 17 mp3an2i ⊢ A ∈ ℂ → inv g ⁡ G ⁡ A = − A ↔ A + − A = 0
19 2 18 mpbird ⊢ A ∈ ℂ → inv g ⁡ G ⁡ A = − A