Theorem znval2

Description: Self-referential expression for the Z/nZ structure. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
	znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znval2.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
Assertion	znval2	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$

Proof

Step	Hyp	Ref	Expression
1		znval2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		znval2.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
5		eqid	$$⊢{\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}$$
6		eqid	$$⊢if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
7		eqid	$$⊢\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}=\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}$$
8	1 2 3 5 6 7	znval	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}⟩$$
9	1 2 3 5 6 4	znle	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}$$
10	9	opeq2d	$$⊢N\in {\mathbb{N}}_0\to ⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩=⟨{\le }_{\mathrm{ndx}},\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}⟩$$
11	10	oveq2d	$$⊢N\in {\mathbb{N}}_0\to U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left(\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)\circ \le \right)\circ {\left({\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right)}^{-1}⟩$$
12	8 11	eqtr4d	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$