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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
Assertion	cnaddinv	$$⊢A\in ℂ\to {inv}_g\left(G\right)\left(A\right)=-A$$

Proof

Step	Hyp	Ref	Expression
1		cnaddabl.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
2		negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$
3	1	cnaddabl	$$⊢G\in \mathrm{Abel}$$
4		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
5	3 4	ax-mp	$$⊢G\in \mathrm{Grp}$$
6		id	$$⊢A\in ℂ\to A\in ℂ$$
7		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
8		cnex	$$⊢ℂ\in \mathrm{V}$$
9	1	grpbase	$$⊢ℂ\in \mathrm{V}\to ℂ={\mathrm{Base}}_G$$
10	8 9	ax-mp	$$⊢ℂ={\mathrm{Base}}_G$$
11		addex	$$⊢+\in \mathrm{V}$$
12	1	grpplusg	$$⊢+\in \mathrm{V}\to +={+}_G$$
13	11 12	ax-mp	$$⊢+={+}_G$$
14	1	cnaddid	$$⊢0_G=0$$
15	14	eqcomi	$$⊢0=0_G$$
16		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
17	10 13 15 16	grpinvid1	$$⊢\left(G\in \mathrm{Grp}\wedge A\in ℂ\wedge -A\in ℂ\right)\to \left({inv}_g\left(G\right)\left(A\right)=-A\leftrightarrow A+\left(-A\right)=0\right)$$
18	5 6 7 17	mp3an2i	$$⊢A\in ℂ\to \left({inv}_g\left(G\right)\left(A\right)=-A\leftrightarrow A+\left(-A\right)=0\right)$$
19	2 18	mpbird	$$⊢A\in ℂ\to {inv}_g\left(G\right)\left(A\right)=-A$$