Theorem zaddablx

Description: The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011)

	Ref	Expression
Hypothesis	zaddablx.g	|- G = { <. 1 , ZZ >. , <. 2 , + >. }
Assertion	zaddablx	|- G e. Abel

Proof

Step	Hyp	Ref	Expression
1		zaddablx.g	|- G = { <. 1 , ZZ >. , <. 2 , + >. }
2		zex	|- ZZ e. _V
3		addex	|- + e. _V
4		zaddcl	|- ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
5		zcn	|- ( x e. ZZ -> x e. CC )
6		zcn	|- ( y e. ZZ -> y e. CC )
7		zcn	|- ( z e. ZZ -> z e. CC )
8		addass	|- ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
9	5 6 7 8	syl3an	|- ( ( x e. ZZ /\ y e. ZZ /\ z e. ZZ ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
10		0z	|- 0 e. ZZ
11	5	addid2d	|- ( x e. ZZ -> ( 0 + x ) = x )
12		znegcl	|- ( x e. ZZ -> -u x e. ZZ )
13		zcn	|- ( -u x e. ZZ -> -u x e. CC )
14		addcom	|- ( ( x e. CC /\ -u x e. CC ) -> ( x + -u x ) = ( -u x + x ) )
15	5 13 14	syl2an	|- ( ( x e. ZZ /\ -u x e. ZZ ) -> ( x + -u x ) = ( -u x + x ) )
16	12 15	mpdan	|- ( x e. ZZ -> ( x + -u x ) = ( -u x + x ) )
17	5	negidd	|- ( x e. ZZ -> ( x + -u x ) = 0 )
18	16 17	eqtr3d	|- ( x e. ZZ -> ( -u x + x ) = 0 )
19	2 3 1 4 9 10 11 12 18	isgrpix	|- G e. Grp
20	2 3 1	grpbasex	|- ZZ = ( Base ` G )
21	2 3 1	grpplusgx	|- + = ( +g ` G )
22		addcom	|- ( ( x e. CC /\ y e. CC ) -> ( x + y ) = ( y + x ) )
23	5 6 22	syl2an	|- ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) = ( y + x ) )
24	19 20 21 23	isabli	|- G e. Abel