cnaddablx

Description: The complex numbers are an Abelian group under addition. This version of cnaddabl shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012)

		Ref	Expression
	Hypothesis	cnaddablx.g	⊢ 𝐺 = { ⟨ 1 , ℂ ⟩ , ⟨ 2 , + ⟩ }
	Assertion	cnaddablx	⊢ 𝐺 ∈ Abel

Proof

Step	Hyp	Ref	Expression
1		cnaddablx.g	⊢ 𝐺 = { ⟨ 1 , ℂ ⟩ , ⟨ 2 , + ⟩ }
2		cnex	⊢ ℂ ∈ V
3		addex	⊢ + ∈ V
4		addcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
5		addass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
6		0cn	⊢ 0 ∈ ℂ
7		addlid	⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
8		negcl	⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
9		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ - 𝑥 ∈ ℂ ) → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
10	8 9	mpdan	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
11		negid	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = 0 )
12	10 11	eqtr3d	⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = 0 )
13	2 3 1 4 5 6 7 8 12	isgrpix	⊢ 𝐺 ∈ Grp
14	2 3 1	grpbasex	⊢ ℂ = ( Base ‘ 𝐺 )
15	2 3 1	grpplusgx	⊢ + = ( +_g ‘ 𝐺 )
16		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
17	13 14 15 16	isabli	⊢ 𝐺 ∈ Abel

Metamath Proof Explorer

Theorem cnaddablx

Proof