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 ` CCfld )

Proof

Step	Hyp	Ref	Expression
1		00id	|- ( 0 + 0 ) = 0
2		cnring	|- CCfld e. Ring
3		ringgrp	|- ( CCfld e. Ring -> CCfld e. Grp )
4	2 3	ax-mp	|- CCfld e. Grp
5		0cn	|- 0 e. CC
6		cnfldbas	|- CC = ( Base ` CCfld )
7		cnfldadd	|- + = ( +g ` CCfld )
8		eqid	|- ( 0g ` CCfld ) = ( 0g ` CCfld )
9	6 7 8	grpid	|- ( ( CCfld e. Grp /\ 0 e. CC ) -> ( ( 0 + 0 ) = 0 <-> ( 0g ` CCfld ) = 0 ) )
10	4 5 9	mp2an	|- ( ( 0 + 0 ) = 0 <-> ( 0g ` CCfld ) = 0 )
11	1 10	mpbi	|- ( 0g ` CCfld ) = 0
12	11	eqcomi	|- 0 = ( 0g ` CCfld )