Theorem cznnring

Description: The ring constructed from a Z/nZ structure with 1 < n by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypotheses	cznrng.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	cznrng.b	$$⊢B={\mathrm{Base}}_Y$$
	cznrng.x	$$⊢X=Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩$$
	cznrng.0	$$⊢\underset{\dot{}}{0}=0_Y$$
Assertion	cznnring	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to X\notin \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		cznrng.b	$$⊢B={\mathrm{Base}}_Y$$
3		cznrng.x	$$⊢X=Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩$$
4		cznrng.0	$$⊢\underset{\dot{}}{0}=0_Y$$
5		eqid	$$⊢{\mathrm{mulGrp}}_X={\mathrm{mulGrp}}_X$$
6	1 2 3	cznrnglem	$$⊢B={\mathrm{Base}}_X$$
7	5 6	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_X}$$
8	3	fveq2i	$$⊢{\mathrm{mulGrp}}_X={\mathrm{mulGrp}}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
9	1	fvexi	$$⊢Y\in \mathrm{V}$$
10	2	fvexi	$$⊢B\in \mathrm{V}$$
11	10 10	mpoex	$$⊢\left(x\in B,y\in B⟼C\right)\in \mathrm{V}$$
12		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
13	12	setsid	$$⊢\left(Y\in \mathrm{V}\wedge \left(x\in B,y\in B⟼C\right)\in \mathrm{V}\right)\to \left(x\in B,y\in B⟼C\right)={\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
14	9 11 13	mp2an	$$⊢\left(x\in B,y\in B⟼C\right)={\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
15	8 14	mgpplusg	$$⊢\left(x\in B,y\in B⟼C\right)={+}_{{\mathrm{mulGrp}}_X}$$
16	15	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_X}=\left(x\in B,y\in B⟼C\right)$$
17		simpr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to C\in B$$
18		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 2\le N\right)$$
19		1lt2	$$⊢1<2$$
20		1red	$$⊢N\in \mathbb{Z}\to 1\in ℝ$$
21		2re	$$⊢2\in ℝ$$
22	21	a1i	$$⊢N\in \mathbb{Z}\to 2\in ℝ$$
23		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
24		ltletr	$$⊢\left(1\in ℝ\wedge 2\in ℝ\wedge N\in ℝ\right)\to \left(\left(1<2\wedge 2\le N\right)\to 1<N\right)$$
25	20 22 23 24	syl3anc	$$⊢N\in \mathbb{Z}\to \left(\left(1<2\wedge 2\le N\right)\to 1<N\right)$$
26	25	expcomd	$$⊢N\in \mathbb{Z}\to \left(2\le N\to \left(1<2\to 1<N\right)\right)$$
27	26	a1i	$$⊢2\in \mathbb{Z}\to \left(N\in \mathbb{Z}\to \left(2\le N\to \left(1<2\to 1<N\right)\right)\right)$$
28	27	3imp	$$⊢\left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 2\le N\right)\to \left(1<2\to 1<N\right)$$
29	19 28	mpi	$$⊢\left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 2\le N\right)\to 1<N$$
30	18 29	sylbi	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
31		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
32	1 2	znhash	$$⊢N\in \mathbb{N}\to \left|B\right|=N$$
33	31 32	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left|B\right|=N$$
34	30 33	breqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<\left|B\right|$$
35	34	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to 1<\left|B\right|$$
36	7 16 17 35	copisnmnd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to {\mathrm{mulGrp}}_X\notin \mathrm{Mnd}$$
37		df-nel	$$⊢{\mathrm{mulGrp}}_X\notin \mathrm{Mnd}\leftrightarrow \neg {\mathrm{mulGrp}}_X\in \mathrm{Mnd}$$
38	36 37	sylib	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to \neg {\mathrm{mulGrp}}_X\in \mathrm{Mnd}$$
39	38	intn3an2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to \neg \left(X\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_X\in \mathrm{Mnd}\wedge \forall a\in B\forall b\in B\forall c\in B\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}\left(b{+}_{X}c\right)=\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}b\right){+}_X\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right)\wedge \left(a{+}_{X}b\right){\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c=\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right){+}_X\left(b{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right)\right)\right)$$
40		eqid	$$⊢{+}_X={+}_X$$
41	3	eqcomi	$$⊢Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩=X$$
42	41	fveq2i	$$⊢{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}={\cdot }_X$$
43	6 5 40 42	isring	$$⊢X\in \mathrm{Ring}\leftrightarrow \left(X\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_X\in \mathrm{Mnd}\wedge \forall a\in B\forall b\in B\forall c\in B\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}\left(b{+}_{X}c\right)=\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}b\right){+}_X\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right)\wedge \left(a{+}_{X}b\right){\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c=\left(a{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right){+}_X\left(b{\cdot }_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}c\right)\right)\right)$$
44	39 43	sylnibr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to \neg X\in \mathrm{Ring}$$
45		df-nel	$$⊢X\notin \mathrm{Ring}\leftrightarrow \neg X\in \mathrm{Ring}$$
46	44 45	sylibr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge C\in B\right)\to X\notin \mathrm{Ring}$$