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		addlid	\|- ( 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

Metamath Proof Explorer

Theorem cnaddablx

Proof