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	⊢ 𝐺 = { ⟨ 1 , ℤ ⟩ , ⟨ 2 , + ⟩ }
	Assertion	zaddablx	⊢ 𝐺 ∈ Abel

Proof

Step	Hyp	Ref	Expression
1		zaddablx.g	⊢ 𝐺 = { ⟨ 1 , ℤ ⟩ , ⟨ 2 , + ⟩ }
2		zex	⊢ ℤ ∈ V
3		addex	⊢ + ∈ V
4		zaddcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
5		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
6		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
7		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
8		addass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9	5 6 7 8	syl3an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
10		0z	⊢ 0 ∈ ℤ
11	5	addlidd	⊢ ( 𝑥 ∈ ℤ → ( 0 + 𝑥 ) = 𝑥 )
12		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
13		zcn	⊢ ( - 𝑥 ∈ ℤ → - 𝑥 ∈ ℂ )
14		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ - 𝑥 ∈ ℂ ) → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
15	5 13 14	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ - 𝑥 ∈ ℤ ) → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
16	12 15	mpdan	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
17	5	negidd	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 + - 𝑥 ) = 0 )
18	16 17	eqtr3d	⊢ ( 𝑥 ∈ ℤ → ( - 𝑥 + 𝑥 ) = 0 )
19	2 3 1 4 9 10 11 12 18	isgrpix	⊢ 𝐺 ∈ Grp
20	2 3 1	grpbasex	⊢ ℤ = ( Base ‘ 𝐺 )
21	2 3 1	grpplusgx	⊢ + = ( +_g ‘ 𝐺 )
22		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
23	5 6 22	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
24	19 20 21 23	isabli	⊢ 𝐺 ∈ Abel

Metamath Proof Explorer

Theorem zaddablx

Proof