Theorem 2zrngnring

Description: R is not a unital ring. (Contributed by AV, 6-Jan-2020)

	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	2zrngnring	$$⊢R\notin \mathrm{Ring}$$

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 3	2zrngnmlid	$$⊢\forall b\in E\exists a\in Eba\ne a$$
5	1 2	2zrngbas	$$⊢E={\mathrm{Base}}_R$$
6	3 5	mgpbas	$$⊢E={\mathrm{Base}}_M$$
7	1 2	2zrngmul	$$⊢\times ={\cdot }_R$$
8	3 7	mgpplusg	$$⊢\times ={+}_M$$
9	6 8	isnmnd	$$⊢\forall b\in E\exists a\in Eba\ne a\to M\notin \mathrm{Mnd}$$
10		df-nel	$$⊢M\notin \mathrm{Mnd}\leftrightarrow \neg M\in \mathrm{Mnd}$$
11	9 10	sylib	$$⊢\forall b\in E\exists a\in Eba\ne a\to \neg M\in \mathrm{Mnd}$$
12	4 11	ax-mp	$$⊢\neg M\in \mathrm{Mnd}$$
13	12	3mix2i	$$⊢\left(\neg R\in \mathrm{Grp}\vee \neg M\in \mathrm{Mnd}\vee \neg \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x\left(y{+}_{R}z\right)=xy{+}_{R}xz\wedge \left(x{+}_{R}y\right)z=xz{+}_{R}yz\right)\right)$$
14		3ianor	$$⊢\neg \left(R\in \mathrm{Grp}\wedge M\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x\left(y{+}_{R}z\right)=xy{+}_{R}xz\wedge \left(x{+}_{R}y\right)z=xz{+}_{R}yz\right)\right)\leftrightarrow \left(\neg R\in \mathrm{Grp}\vee \neg M\in \mathrm{Mnd}\vee \neg \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x\left(y{+}_{R}z\right)=xy{+}_{R}xz\wedge \left(x{+}_{R}y\right)z=xz{+}_{R}yz\right)\right)$$
15	13 14	mpbir	$$⊢\neg \left(R\in \mathrm{Grp}\wedge M\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x\left(y{+}_{R}z\right)=xy{+}_{R}xz\wedge \left(x{+}_{R}y\right)z=xz{+}_{R}yz\right)\right)$$
16		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
17		eqid	$$⊢{+}_R={+}_R$$
18	16 3 17 7	isring	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Grp}\wedge M\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x\left(y{+}_{R}z\right)=xy{+}_{R}xz\wedge \left(x{+}_{R}y\right)z=xz{+}_{R}yz\right)\right)$$
19	15 18	mtbir	$$⊢\neg R\in \mathrm{Ring}$$
20	19	nelir	$$⊢R\notin \mathrm{Ring}$$