Metamath Proof Explorer

Theorem 2zrngamnd

Description: R is an (additive) monoid. (Contributed by AV, 11-Feb-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
Assertion 2zrngamnd ⊢ R ∈ Mnd

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 1 2 2zrngasgrp Could not format R e. Smgrp : No typesetting found for |- R e. Smgrp with typecode |-
4 1 0even ⊢ 0 ∈ E
5 id ⊢ 0 ∈ E → 0 ∈ E
6 oveq1 ⊢ x = 0 → x + y = 0 + y
7 6 eqeq1d ⊢ x = 0 → x + y = y ↔ 0 + y = y
8 7 ovanraleqv ⊢ x = 0 → ∀ y ∈ E x + y = y ∧ y + x = y ↔ ∀ y ∈ E 0 + y = y ∧ y + 0 = y
9 8 adantl ⊢ 0 ∈ E ∧ x = 0 → ∀ y ∈ E x + y = y ∧ y + x = y ↔ ∀ y ∈ E 0 + y = y ∧ y + 0 = y
10 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
11 10 1 eleq2s ⊢ y ∈ E → y ∈ ℤ
12 11 zcnd ⊢ y ∈ E → y ∈ ℂ
13 addid2 ⊢ y ∈ ℂ → 0 + y = y
14 addid1 ⊢ y ∈ ℂ → y + 0 = y
15 13 14 jca ⊢ y ∈ ℂ → 0 + y = y ∧ y + 0 = y
16 12 15 syl ⊢ y ∈ E → 0 + y = y ∧ y + 0 = y
17 16 adantl ⊢ 0 ∈ E ∧ y ∈ E → 0 + y = y ∧ y + 0 = y
18 17 ralrimiva ⊢ 0 ∈ E → ∀ y ∈ E 0 + y = y ∧ y + 0 = y
19 5 9 18 rspcedvd ⊢ 0 ∈ E → ∃ x ∈ E ∀ y ∈ E x + y = y ∧ y + x = y
20 4 19 ax-mp ⊢ ∃ x ∈ E ∀ y ∈ E x + y = y ∧ y + x = y
21 1 2 2zrngbas ⊢ E = Base R
22 1 2 2zrngadd ⊢ + = + R
23 21 22 ismnddef Could not format ( R e. Mnd <-> ( R e. Smgrp /\ E. x e. E A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) ) ) : No typesetting found for |- ( R e. Mnd <-> ( R e. Smgrp /\ E. x e. E A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) ) ) with typecode |-
24 3 20 23 mpbir2an ⊢ R ∈ Mnd