Theorem cnaddablx

Description: The complex numbers are an Abelian group under addition. This version of cnaddabl shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012)

	Ref	Expression
Hypothesis	cnaddablx.g	$$⊢G=\left\{⟨1,ℂ⟩,⟨2,+⟩\right\}$$
Assertion	cnaddablx	$$⊢G\in \mathrm{Abel}$$

Proof

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