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, ℤ⟩, ⟨2 +⟩\}$
	Assertion	zaddablx	$⊢ G \in Abel$

Proof

Step	Hyp	Ref	Expression
1		zaddablx.g	$⊢ G = \{⟨1, ℤ⟩, ⟨2 +⟩\}$
2		zex	$⊢ ℤ \in V$
3		addex	$⊢ + \in V$
4		zaddcl	$⊢ (x \in ℤ \land y \in ℤ) \to x + y \in ℤ$
5		zcn	$⊢ x \in ℤ \to x \in ℂ$
6		zcn	$⊢ y \in ℤ \to y \in ℂ$
7		zcn	$⊢ z \in ℤ \to z \in ℂ$
8		addass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x + y + z = x + y + z$
9	5 6 7 8	syl3an	$⊢ (x \in ℤ \land y \in ℤ \land z \in ℤ) \to x + y + z = x + y + z$
10		0z	$⊢ 0 \in ℤ$
11	5	addid2d	$⊢ x \in ℤ \to 0 + x = x$
12		znegcl	$⊢ x \in ℤ \to - x \in ℤ$
13		zcn	$⊢ - x \in ℤ \to - x \in ℂ$
14		addcom	$⊢ (x \in ℂ \land - x \in ℂ) \to x + (- x) = - x + x$
15	5 13 14	syl2an	$⊢ (x \in ℤ \land - x \in ℤ) \to x + (- x) = - x + x$
16	12 15	mpdan	$⊢ x \in ℤ \to x + (- x) = - x + x$
17	5	negidd	$⊢ x \in ℤ \to x + (- x) = 0$
18	16 17	eqtr3d	$⊢ x \in ℤ \to - x + x = 0$
19	2 3 1 4 9 10 11 12 18	isgrpix	$⊢ G \in Grp$
20	2 3 1	grpbasex	$⊢ ℤ = {Base}_{G}$
21	2 3 1	grpplusgx	$⊢ + = +_{G}$
22		addcom	$⊢ (x \in ℂ \land y \in ℂ) \to x + y = y + x$
23	5 6 22	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to x + y = y + x$
24	19 20 21 23	isabli	$⊢ G \in Abel$

Metamath Proof Explorer

Theorem zaddablx

Proof