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 = { <. 1 , CC >. , <. 2 , + >. }
Assertion	cnaddablx	|- G e. Abel

Proof

Step	Hyp	Ref	Expression
1		cnaddablx.g	|- G = { <. 1 , CC >. , <. 2 , + >. }
2		cnex	|- CC e. _V
3		addex	|- + e. _V
4		addcl	|- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
5		addass	|- ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
6		0cn	|- 0 e. CC
7		addid2	|- ( x e. CC -> ( 0 + x ) = x )
8		negcl	|- ( x e. CC -> -u x e. CC )
9		addcom	|- ( ( x e. CC /\ -u x e. CC ) -> ( x + -u x ) = ( -u x + x ) )
10	8 9	mpdan	|- ( x e. CC -> ( x + -u x ) = ( -u x + x ) )
11		negid	|- ( x e. CC -> ( x + -u x ) = 0 )
12	10 11	eqtr3d	|- ( x e. CC -> ( -u x + x ) = 0 )
13	2 3 1 4 5 6 7 8 12	isgrpix	|- G e. Grp
14	2 3 1	grpbasex	|- CC = ( Base ` G )
15	2 3 1	grpplusgx	|- + = ( +g ` G )
16		addcom	|- ( ( x e. CC /\ y e. CC ) -> ( x + y ) = ( y + x ) )
17	13 14 15 16	isabli	|- G e. Abel