Theorem cnaddabl

Description: The complex numbers are an Abelian group under addition. This version of cnaddablx hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring . (Contributed by NM, 20-Oct-2012) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnaddabl.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
Assertion	cnaddabl	$$⊢G\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		cnaddabl.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3	1	grpbase	$$⊢ℂ\in \mathrm{V}\to ℂ={\mathrm{Base}}_G$$
4	2 3	ax-mp	$$⊢ℂ={\mathrm{Base}}_G$$
5		addex	$$⊢+\in \mathrm{V}$$
6	1	grpplusg	$$⊢+\in \mathrm{V}\to +={+}_G$$
7	5 6	ax-mp	$$⊢+={+}_G$$
8		addcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y\in ℂ$$
9		addass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x+y+z=x+y+z$$
10		0cn	$$⊢0\in ℂ$$
11		addlid	$$⊢x\in ℂ\to 0+x=x$$
12		negcl	$$⊢x\in ℂ\to -x\in ℂ$$
13		addcom	$$⊢\left(x\in ℂ\wedge -x\in ℂ\right)\to x+\left(-x\right)=-x+x$$
14	12 13	mpdan	$$⊢x\in ℂ\to x+\left(-x\right)=-x+x$$
15		negid	$$⊢x\in ℂ\to x+\left(-x\right)=0$$
16	14 15	eqtr3d	$$⊢x\in ℂ\to -x+x=0$$
17	4 7 8 9 10 11 12 16	isgrpi	$$⊢G\in \mathrm{Grp}$$
18		addcom	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y=y+x$$
19	17 4 7 18	isabli	$$⊢G\in \mathrm{Abel}$$