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 )