cnaddabl

Description: The complex numbers are an Abelian group under addition. This version of cnaddablx hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring . (Contributed by NM, 20-Oct-2012) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	cnaddabl.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ }
	Assertion	cnaddabl	⊢ 𝐺 ∈ Abel

Proof

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

Metamath Proof Explorer

Theorem cnaddabl

Proof