Theorem cnfld0

Description: Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	cnfld0	⊢ 0 = ( 0g ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		00id	⊢ ( 0 + 0 ) = 0
2		cnring	⊢ ℂfld ∈ Ring
3		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
4	2 3	ax-mp	⊢ ℂfld ∈ Grp
5		0cn	⊢ 0 ∈ ℂ
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7		cnfldadd	⊢ + = ( +g ‘ ℂfld )
8		eqid	⊢ ( 0g ‘ ℂfld ) = ( 0g ‘ ℂfld )
9	6 7 8	grpid	⊢ ( ( ℂfld ∈ Grp ∧ 0 ∈ ℂ ) → ( ( 0 + 0 ) = 0 ↔ ( 0g ‘ ℂfld ) = 0 ) )
10	4 5 9	mp2an	⊢ ( ( 0 + 0 ) = 0 ↔ ( 0g ‘ ℂfld ) = 0 )
11	1 10	mpbi	⊢ ( 0g ‘ ℂfld ) = 0
12	11	eqcomi	⊢ 0 = ( 0g ‘ ℂfld )