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

Metamath Proof Explorer

Theorem cnaddabl

Proof