Theorem znle2

Description: The ordering of the Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znle2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znle2.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_W$$
	znle2.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
	znle2.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
Assertion	znle2	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		znle2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		znle2.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_W$$
3		znle2.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
4		znle2.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
5		eqid	$$⊢\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
6		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)$$
7		eqid	$$⊢{\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W={\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W$$
8	5 6 1 7 3 4	znle	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(\left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)}^{-1}$$
9	5 6 1	znzrh	$$⊢N\in {\mathbb{N}}_0\to \mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
10	9	reseq1d	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_W$$
11	10 2	eqtr4di	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W=F$$
12	11	coeq1d	$$⊢N\in {\mathbb{N}}_0\to \left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)\circ \le =F\circ \le$$
13	11	cnveqd	$$⊢N\in {\mathbb{N}}_0\to {\left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)}^{-1}=F^{-1}$$
14	12 13	coeq12d	$$⊢N\in {\mathbb{N}}_0\to \left(\left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\upharpoonright }_W\right)}^{-1}=\left(F\circ \le \right)\circ F^{-1}$$
15	8 14	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$