Metamath Proof Explorer

Theorem 2zrngALT

Description: The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng , based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl ) and a multiplicative semigroup (see 2zrngmsgrp ). (Contributed by AV, 11-Feb-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
2zrngmmgm.1 ⊢ M = mulGrp R
Assertion 2zrngALT ⊢ R ∈ Rng

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 2zrngmmgm.1 ⊢ M = mulGrp R
4 1 2 2zrngaabl ⊢ R ∈ Abel
5 1 2 3 2zrngmsgrp ⊢ M ∈ Smgrp
6 elrabi ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ
7 6 zcnd ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℂ
8 7 1 eleq2s ⊢ a ∈ E → a ∈ ℂ
9 elrabi ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℤ
10 9 zcnd ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℂ
11 10 1 eleq2s ⊢ b ∈ E → b ∈ ℂ
12 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
13 12 zcnd ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℂ
14 13 1 eleq2s ⊢ y ∈ E → y ∈ ℂ
15 adddi ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a ⁢ b + y = a ⁢ b + a ⁢ y
16 adddir ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + b ⁢ y = a ⁢ y + b ⁢ y
17 15 16 jca ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a ⁢ b + y = a ⁢ b + a ⁢ y ∧ a + b ⁢ y = a ⁢ y + b ⁢ y
18 8 11 14 17 syl3an ⊢ a ∈ E ∧ b ∈ E ∧ y ∈ E → a ⁢ b + y = a ⁢ b + a ⁢ y ∧ a + b ⁢ y = a ⁢ y + b ⁢ y
19 18 rgen3 ⊢ ∀ a ∈ E ∀ b ∈ E ∀ y ∈ E a ⁢ b + y = a ⁢ b + a ⁢ y ∧ a + b ⁢ y = a ⁢ y + b ⁢ y
20 1 2 2zrngbas ⊢ E = Base R
21 1 2 2zrngadd ⊢ + = + R
22 1 2 2zrngmul ⊢ × = ⋅ R
23 20 3 21 22 isrng ⊢ R ∈ Rng ↔ R ∈ Abel ∧ M ∈ Smgrp ∧ ∀ a ∈ E ∀ b ∈ E ∀ y ∈ E a ⁢ b + y = a ⁢ b + a ⁢ y ∧ a + b ⁢ y = a ⁢ y + b ⁢ y
24 4 5 19 23 mpbir3an ⊢ R ∈ Rng