Theorem cnaddid

Description: The group identity element of complex number addition is zero. See also cnfld0 . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 26-Aug-2021) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cnaddabl.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
2		0cn	⊢ 0 ∈ ℂ
3		cnex	⊢ ℂ ∈ V
4	1	grpbase	⊢ ( ℂ ∈ V → ℂ = ( Base ‘ 𝐺 ) )
5	3 4	ax-mp	⊢ ℂ = ( Base ‘ 𝐺 )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7		addex	⊢ + ∈ V
8	1	grpplusg	⊢ ( + ∈ V → + = ( +g ‘ 𝐺 ) )
9	7 8	ax-mp	⊢ + = ( +g ‘ 𝐺 )
10		id	⊢ ( 0 ∈ ℂ → 0 ∈ ℂ )
11		addlid	⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
12	11	adantl	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝑥 ) = 𝑥 )
13		addrid	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + 0 ) = 𝑥 )
14	13	adantl	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 + 0 ) = 𝑥 )
15	5 6 9 10 12 14	ismgmid2	⊢ ( 0 ∈ ℂ → 0 = ( 0g ‘ 𝐺 ) )
16	2 15	ax-mp	⊢ 0 = ( 0g ‘ 𝐺 )
17	16	eqcomi	⊢ ( 0g ‘ 𝐺 ) = 0