Theorem znle

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
	znval.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znval.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W$$
	znval.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
	znle.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
Assertion	znle	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		znval.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		znval.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W$$
5		znval.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
6		znle.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
7		eqid	$$⊢\left(F\circ \le \right)\circ F^{-1}=\left(F\circ \le \right)\circ F^{-1}$$
8	1 2 3 4 5 7	znval	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(F\circ \le \right)\circ F^{-1}⟩$$
9	8	fveq2d	$$⊢N\in {\mathbb{N}}_0\to {\le }_Y={\le }_{\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(F\circ \le \right)\circ F^{-1}⟩\right)}$$
10	2	ovexi	$$⊢U\in \mathrm{V}$$
11		fvex	$$⊢\mathrm{\mathbb{Z}RHom}\left(U\right)\in \mathrm{V}$$
12	11	resex	$$⊢{\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W\in \mathrm{V}$$
13	4 12	eqeltri	$$⊢F\in \mathrm{V}$$
14		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
15	14 14	xpex	$$⊢{ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}$$
16		lerelxr	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$
17	15 16	ssexi	$$⊢\le \in \mathrm{V}$$
18	13 17	coex	$$⊢F\circ \le \in \mathrm{V}$$
19	13	cnvex	$$⊢F^{-1}\in \mathrm{V}$$
20	18 19	coex	$$⊢\left(F\circ \le \right)\circ F^{-1}\in \mathrm{V}$$
21		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
22	21	setsid	$$⊢\left(U\in \mathrm{V}\wedge \left(F\circ \le \right)\circ F^{-1}\in \mathrm{V}\right)\to \left(F\circ \le \right)\circ F^{-1}={\le }_{\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(F\circ \le \right)\circ F^{-1}⟩\right)}$$
23	10 20 22	mp2an	$$⊢\left(F\circ \le \right)\circ F^{-1}={\le }_{\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(F\circ \le \right)\circ F^{-1}⟩\right)}$$
24	9 6 23	3eqtr4g	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$