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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
Assertion	cnaddid	$$⊢0_G=0$$

Proof

Step	Hyp	Ref	Expression
1		cnaddabl.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
2		0cn	$$⊢0\in ℂ$$
3		cnex	$$⊢ℂ\in \mathrm{V}$$
4	1	grpbase	$$⊢ℂ\in \mathrm{V}\to ℂ={\mathrm{Base}}_G$$
5	3 4	ax-mp	$$⊢ℂ={\mathrm{Base}}_G$$
6		eqid	$$⊢0_G=0_G$$
7		addex	$$⊢+\in \mathrm{V}$$
8	1	grpplusg	$$⊢+\in \mathrm{V}\to +={+}_G$$
9	7 8	ax-mp	$$⊢+={+}_G$$
10		id	$$⊢0\in ℂ\to 0\in ℂ$$
11		addlid	$$⊢x\in ℂ\to 0+x=x$$
12	11	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to 0+x=x$$
13		addrid	$$⊢x\in ℂ\to x+0=x$$
14	13	adantl	$$⊢\left(0\in ℂ\wedge x\in ℂ\right)\to x+0=x$$
15	5 6 9 10 12 14	ismgmid2	$$⊢0\in ℂ\to 0=0_G$$
16	2 15	ax-mp	$$⊢0=0_G$$
17	16	eqcomi	$$⊢0_G=0$$