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	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
	2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	2zrngALT	⊢ 𝑅 ∈ Rng

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4	1 2	2zrngaabl	⊢ 𝑅 ∈ Abel
5	1 2 3	2zrngmsgrp	⊢ 𝑀 ∈ Smgrp
6		elrabi	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑎 ∈ ℤ )
7	6	zcnd	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑎 ∈ ℂ )
8	7 1	eleq2s	⊢ ( 𝑎 ∈ 𝐸 → 𝑎 ∈ ℂ )
9		elrabi	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℤ )
10	9	zcnd	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℂ )
11	10 1	eleq2s	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ∈ ℂ )
12		elrabi	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℤ )
13	12	zcnd	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℂ )
14	13 1	eleq2s	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℂ )
15		adddi	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑎 · ( 𝑏 + 𝑦 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑦 ) ) )
16		adddir	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) )
17	15 16	jca	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑎 · ( 𝑏 + 𝑦 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑦 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) )
18	8 11 14 17	syl3an	⊢ ( ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → ( ( 𝑎 · ( 𝑏 + 𝑦 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑦 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) )
19	18	rgen3	⊢ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑎 · ( 𝑏 + 𝑦 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑦 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) )
20	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
21	1 2	2zrngadd	⊢ + = ( +g ‘ 𝑅 )
22	1 2	2zrngmul	⊢ · = ( .r ‘ 𝑅 )
23	20 3 21 22	isrng	⊢ ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ 𝑀 ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑎 · ( 𝑏 + 𝑦 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑦 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) ) )
24	4 5 19 23	mpbir3an	⊢ 𝑅 ∈ Rng