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 ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
Assertion cnaddinv ( 𝐴 ∈ ℂ → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) = - 𝐴 )

Proof

Step Hyp Ref Expression
1 cnaddabl.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
2 negid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )
3 1 cnaddabl ⊢ 𝐺 ∈ Abel
4 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
5 3 4 ax-mp ⊢ 𝐺 ∈ Grp
6 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
7 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
8 cnex ⊢ ℂ ∈ V
9 1 grpbase ⊢ ( ℂ ∈ V → ℂ = ( Base ‘ 𝐺 ) )
10 8 9 ax-mp ⊢ ℂ = ( Base ‘ 𝐺 )
11 addex ⊢ + ∈ V
12 1 grpplusg ⊢ ( + ∈ V → + = ( +g ‘ 𝐺 ) )
13 11 12 ax-mp ⊢ + = ( +g ‘ 𝐺 )
14 1 cnaddid ⊢ ( 0g ‘ 𝐺 ) = 0
15 14 eqcomi ⊢ 0 = ( 0g ‘ 𝐺 )
16 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
17 10 13 15 16 grpinvid1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) = - 𝐴 ↔ ( 𝐴 + - 𝐴 ) = 0 ) )
18 5 6 7 17 mp3an2i ⊢ ( 𝐴 ∈ ℂ → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) = - 𝐴 ↔ ( 𝐴 + - 𝐴 ) = 0 ) )
19 2 18 mpbird ⊢ ( 𝐴 ∈ ℂ → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) = - 𝐴 )