Metamath Proof Explorer


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 𝑅 = ( ℂflds 𝐸 )
Assertion 2zrng0 0 = ( 0g𝑅 )

Proof

Step Hyp Ref Expression
1 2zrng.e 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2 2zrngbas.r 𝑅 = ( ℂflds 𝐸 )
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𝑅 )