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 = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
Assertion	cnaddabl	|- G e. Abel

Proof

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