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

Metamath Proof Explorer

Theorem zaddablx

Proof