Theorem 2zrng

Description: The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm . (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zlidl.u	⊢ 𝑈 = ( LIdeal ‘ ℤring )
	2zrng.r	⊢ 𝑅 = ( ℤring ↾s 𝐸 )
Assertion	2zrng	⊢ 𝑅 ∈ Rng

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zlidl.u	⊢ 𝑈 = ( LIdeal ‘ ℤring )
3		2zrng.r	⊢ 𝑅 = ( ℤring ↾s 𝐸 )
4		zringring	⊢ ℤring ∈ Ring
5	1 2	2zlidl	⊢ 𝐸 ∈ 𝑈
6	2 3	lidlrng	⊢ ( ( ℤring ∈ Ring ∧ 𝐸 ∈ 𝑈 ) → 𝑅 ∈ Rng )
7	4 5 6	mp2an	⊢ 𝑅 ∈ Rng