Theorem cnaddid

Description: The group identity element of complex number addition is zero. See also cnfld0 . (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	cnaddid	|- ( 0g ` G ) = 0

Proof

Step	Hyp	Ref	Expression
1		cnaddabl.g	|- G = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
2		0cn	|- 0 e. CC
3		cnex	|- CC e. _V
4	1	grpbase	|- ( CC e. _V -> CC = ( Base ` G ) )
5	3 4	ax-mp	|- CC = ( Base ` G )
6		eqid	|- ( 0g ` G ) = ( 0g ` G )
7		addex	|- + e. _V
8	1	grpplusg	|- ( + e. _V -> + = ( +g ` G ) )
9	7 8	ax-mp	|- + = ( +g ` G )
10		id	|- ( 0 e. CC -> 0 e. CC )
11		addid2	|- ( x e. CC -> ( 0 + x ) = x )
12	11	adantl	|- ( ( 0 e. CC /\ x e. CC ) -> ( 0 + x ) = x )
13		addid1	|- ( x e. CC -> ( x + 0 ) = x )
14	13	adantl	|- ( ( 0 e. CC /\ x e. CC ) -> ( x + 0 ) = x )
15	5 6 9 10 12 14	ismgmid2	|- ( 0 e. CC -> 0 = ( 0g ` G ) )
16	2 15	ax-mp	|- 0 = ( 0g ` G )
17	16	eqcomi	|- ( 0g ` G ) = 0