Theorem 2zrng0

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

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrng0	⊢ 0 = ( 0g ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		cncrng	⊢ ℂfld ∈ CRing
4		crngring	⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring )
5		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
6	3 4 5	mp2b	⊢ ℂfld ∈ Mnd
7	1	0even	⊢ 0 ∈ 𝐸
8		ssrab2	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ⊆ ℤ
9	1 8	eqsstri	⊢ 𝐸 ⊆ ℤ
10		zsscn	⊢ ℤ ⊆ ℂ
11	9 10	sstri	⊢ 𝐸 ⊆ ℂ
12		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
13		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
14	2 12 13	ress0g	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ 𝐸 ∧ 𝐸 ⊆ ℂ ) → 0 = ( 0g ‘ 𝑅 ) )
15	6 7 11 14	mp3an	⊢ 0 = ( 0g ‘ 𝑅 )