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 ) , CC >. , <. ( +g ` ndx ) , + >. }
Assertion cnaddinv 
|- ( A e. CC -> ( ( invg ` G ) ` A ) = -u A )

Proof

Step Hyp Ref Expression
1 cnaddabl.g 
 |-  G = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
2 negid 
 |-  ( A e. CC -> ( A + -u A ) = 0 )
3 1 cnaddabl 
 |-  G e. Abel
4 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
5 3 4 ax-mp 
 |-  G e. Grp
6 id 
 |-  ( A e. CC -> A e. CC )
7 negcl 
 |-  ( A e. CC -> -u A e. CC )
8 cnex 
 |-  CC e. _V
9 1 grpbase 
 |-  ( CC e. _V -> CC = ( Base ` G ) )
10 8 9 ax-mp 
 |-  CC = ( Base ` G )
11 addex 
 |-  + e. _V
12 1 grpplusg 
 |-  ( + e. _V -> + = ( +g ` G ) )
13 11 12 ax-mp 
 |-  + = ( +g ` G )
14 1 cnaddid 
 |-  ( 0g ` G ) = 0
15 14 eqcomi 
 |-  0 = ( 0g ` G )
16 eqid 
 |-  ( invg ` G ) = ( invg ` G )
17 10 13 15 16 grpinvid1 
 |-  ( ( G e. Grp /\ A e. CC /\ -u A e. CC ) -> ( ( ( invg ` G ) ` A ) = -u A <-> ( A + -u A ) = 0 ) )
18 5 6 7 17 mp3an2i 
 |-  ( A e. CC -> ( ( ( invg ` G ) ` A ) = -u A <-> ( A + -u A ) = 0 ) )
19 2 18 mpbird 
 |-  ( A e. CC -> ( ( invg ` G ) ` A ) = -u A )