Theorem 2zrng0

Description: The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020)

	Ref	Expression
Hypotheses	2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zrngbas.r	|- R = ( CCfld |`s E )
Assertion	2zrng0	|- 0 = ( 0g ` R )

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2		2zrngbas.r	|- R = ( CCfld |`s E )
3		cncrng	|- CCfld e. CRing
4		crngring	|- ( CCfld e. CRing -> CCfld e. Ring )
5		ringmnd	|- ( CCfld e. Ring -> CCfld e. Mnd )
6	3 4 5	mp2b	|- CCfld e. Mnd
7	1	0even	|- 0 e. E
8		ssrab2	|- { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } C_ ZZ
9	1 8	eqsstri	|- E C_ ZZ
10		zsscn	|- ZZ C_ CC
11	9 10	sstri	|- E C_ CC
12		cnfldbas	|- CC = ( Base ` CCfld )
13		cnfld0	|- 0 = ( 0g ` CCfld )
14	2 12 13	ress0g	|- ( ( CCfld e. Mnd /\ 0 e. E /\ E C_ CC ) -> 0 = ( 0g ` R ) )
15	6 7 11 14	mp3an	|- 0 = ( 0g ` R )