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=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
	2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
	2zrngmmgm.1	$$⊢M={\mathrm{mulGrp}}_R$$
Assertion	2zrngALT	$$⊢R\in \mathrm{Rng}$$

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
2		2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
3		2zrngmmgm.1	$$⊢M={\mathrm{mulGrp}}_R$$
4	1 2	2zrngaabl	$$⊢R\in \mathrm{Abel}$$
5	1 2 3	2zrngmsgrp	Could not format M e. Smgrp : No typesetting found for |- M e. Smgrp with typecode |-
6		elrabi	$$⊢a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to a\in \mathbb{Z}$$
7	6	zcnd	$$⊢a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to a\in ℂ$$
8	7 1	eleq2s	$$⊢a\in E\to a\in ℂ$$
9		elrabi	$$⊢b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to b\in \mathbb{Z}$$
10	9	zcnd	$$⊢b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to b\in ℂ$$
11	10 1	eleq2s	$$⊢b\in E\to b\in ℂ$$
12		elrabi	$$⊢y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to y\in \mathbb{Z}$$
13	12	zcnd	$$⊢y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to y\in ℂ$$
14	13 1	eleq2s	$$⊢y\in E\to y\in ℂ$$
15		adddi	$$⊢\left(a\in ℂ\wedge b\in ℂ\wedge y\in ℂ\right)\to a\left(b+y\right)=ab+ay$$
16		adddir	$$⊢\left(a\in ℂ\wedge b\in ℂ\wedge y\in ℂ\right)\to \left(a+b\right)y=ay+by$$
17	15 16	jca	$$⊢\left(a\in ℂ\wedge b\in ℂ\wedge y\in ℂ\right)\to \left(a\left(b+y\right)=ab+ay\wedge \left(a+b\right)y=ay+by\right)$$
18	8 11 14 17	syl3an	$$⊢\left(a\in E\wedge b\in E\wedge y\in E\right)\to \left(a\left(b+y\right)=ab+ay\wedge \left(a+b\right)y=ay+by\right)$$
19	18	rgen3	$$⊢\forall a\in E\forall b\in E\forall y\in E\left(a\left(b+y\right)=ab+ay\wedge \left(a+b\right)y=ay+by\right)$$
20	1 2	2zrngbas	$$⊢E={\mathrm{Base}}_R$$
21	1 2	2zrngadd	$$⊢+={+}_R$$
22	1 2	2zrngmul	$$⊢\times ={\cdot }_R$$
23	20 3 21 22	isrng	Could not format ( R e. Rng <-> ( R e. Abel /\ M e. Smgrp /\ A. a e. E A. b e. E A. y e. E ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) ) ) : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ M e. Smgrp /\ A. a e. E A. b e. E A. y e. E ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) ) ) with typecode |-
24	4 5 19 23	mpbir3an	$$⊢R\in \mathrm{Rng}$$