Theorem znleval

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$$
	znleval.x	$$⊢X={\mathrm{Base}}_Y$$
Assertion	znleval	$$⊢N\in {\mathbb{N}}_0\to \left(A\underset{\dot{}}{\le }B\leftrightarrow \left(A\in X\wedge B\in X\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)\right)$$

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		znleval.x	$$⊢X={\mathrm{Base}}_Y$$
6	1 2 3 4	znle2	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$
7		relco	$$⊢\mathrm{Rel}\left(\left(F\circ \le \right)\circ F^{-1}\right)$$
8		relssdmrn	$$⊢\mathrm{Rel}\left(\left(F\circ \le \right)\circ F^{-1}\right)\to \left(F\circ \le \right)\circ F^{-1}\subseteq \mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\times \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)$$
9	7 8	ax-mp	$$⊢\left(F\circ \le \right)\circ F^{-1}\subseteq \mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\times \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)$$
10		dmcoss	$$⊢\mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq \mathrm{dom}{F}^{-1}$$
11		df-rn	$$⊢\mathrm{ran}F=\mathrm{dom}{F}^{-1}$$
12	1 5 2 3	znf1o	$$⊢N\in {\mathbb{N}}_0\to F:W\underset{1-1\; onto}{⟶}X$$
13		f1ofo	$$⊢F:W\underset{1-1\; onto}{⟶}X\to F:W\underset{onto}{⟶}X$$
14		forn	$$⊢F:W\underset{onto}{⟶}X\to \mathrm{ran}F=X$$
15	12 13 14	3syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{ran}F=X$$
16	11 15	eqtr3id	$$⊢N\in {\mathbb{N}}_0\to \mathrm{dom}{F}^{-1}=X$$
17	10 16	sseqtrid	$$⊢N\in {\mathbb{N}}_0\to \mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X$$
18		rncoss	$$⊢\mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq \mathrm{ran}\left(F\circ \le \right)$$
19		rncoss	$$⊢\mathrm{ran}\left(F\circ \le \right)\subseteq \mathrm{ran}F$$
20	19 15	sseqtrid	$$⊢N\in {\mathbb{N}}_0\to \mathrm{ran}\left(F\circ \le \right)\subseteq X$$
21	18 20	sstrid	$$⊢N\in {\mathbb{N}}_0\to \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X$$
22		xpss12	$$⊢\left(\mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X\wedge \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X\right)\to \mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\times \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X\times X$$
23	17 21 22	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \mathrm{dom}\left(\left(F\circ \le \right)\circ F^{-1}\right)\times \mathrm{ran}\left(\left(F\circ \le \right)\circ F^{-1}\right)\subseteq X\times X$$
24	9 23	sstrid	$$⊢N\in {\mathbb{N}}_0\to \left(F\circ \le \right)\circ F^{-1}\subseteq X\times X$$
25	6 24	eqsstrd	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }\subseteq X\times X$$
26	25	ssbrd	$$⊢N\in {\mathbb{N}}_0\to \left(A\underset{\dot{}}{\le }B\to A\left(X\times X\right)B\right)$$
27		brxp	$$⊢A\left(X\times X\right)B\leftrightarrow \left(A\in X\wedge B\in X\right)$$
28	26 27	imbitrdi	$$⊢N\in {\mathbb{N}}_0\to \left(A\underset{\dot{}}{\le }B\to \left(A\in X\wedge B\in X\right)\right)$$
29	28	pm4.71rd	$$⊢N\in {\mathbb{N}}_0\to \left(A\underset{\dot{}}{\le }B\leftrightarrow \left(\left(A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\le }B\right)\right)$$
30	6	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$
31	30	breqd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(A\underset{\dot{}}{\le }B\leftrightarrow A\left(\left(F\circ \le \right)\circ F^{-1}\right)B\right)$$
32		brcog	$$⊢\left(A\in X\wedge B\in X\right)\to \left(A\left(\left(F\circ \le \right)\circ F^{-1}\right)B\leftrightarrow \exists x\left(A{F}^{-1}x\wedge x\left(F\circ \le \right)B\right)\right)$$
33	32	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(A\left(\left(F\circ \le \right)\circ F^{-1}\right)B\leftrightarrow \exists x\left(A{F}^{-1}x\wedge x\left(F\circ \le \right)B\right)\right)$$
34		eqcom	$$⊢x=F^{-1}\left(A\right)\leftrightarrow F^{-1}\left(A\right)=x$$
35	12	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to F:W\underset{1-1\; onto}{⟶}X$$
36		f1ocnv	$$⊢F:W\underset{1-1\; onto}{⟶}X\to F^{-1}:X\underset{1-1\; onto}{⟶}W$$
37		f1ofn	$$⊢F^{-1}:X\underset{1-1\; onto}{⟶}W\to F^{-1}FnX$$
38	35 36 37	3syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to F^{-1}FnX$$
39		simprl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to A\in X$$
40		fnbrfvb	$$⊢\left(F^{-1}FnX\wedge A\in X\right)\to \left(F^{-1}\left(A\right)=x\leftrightarrow A{F}^{-1}x\right)$$
41	38 39 40	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(F^{-1}\left(A\right)=x\leftrightarrow A{F}^{-1}x\right)$$
42	34 41	bitr2id	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(A{F}^{-1}x\leftrightarrow x=F^{-1}\left(A\right)\right)$$
43	42	anbi1d	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\left(A{F}^{-1}x\wedge x\left(F\circ \le \right)B\right)\leftrightarrow \left(x=F^{-1}\left(A\right)\wedge x\left(F\circ \le \right)B\right)\right)$$
44	43	exbidv	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\exists x\left(A{F}^{-1}x\wedge x\left(F\circ \le \right)B\right)\leftrightarrow \exists x\left(x=F^{-1}\left(A\right)\wedge x\left(F\circ \le \right)B\right)\right)$$
45	33 44	bitrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(A\left(\left(F\circ \le \right)\circ F^{-1}\right)B\leftrightarrow \exists x\left(x=F^{-1}\left(A\right)\wedge x\left(F\circ \le \right)B\right)\right)$$
46		fvex	$$⊢F^{-1}\left(A\right)\in \mathrm{V}$$
47		breq1	$$⊢x=F^{-1}\left(A\right)\to \left(x\left(F\circ \le \right)B\leftrightarrow F^{-1}\left(A\right)\left(F\circ \le \right)B\right)$$
48	46 47	ceqsexv	$$⊢\exists x\left(x=F^{-1}\left(A\right)\wedge x\left(F\circ \le \right)B\right)\leftrightarrow F^{-1}\left(A\right)\left(F\circ \le \right)B$$
49		simprr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to B\in X$$
50		brcog	$$⊢\left(F^{-1}\left(A\right)\in \mathrm{V}\wedge B\in X\right)\to \left(F^{-1}\left(A\right)\left(F\circ \le \right)B\leftrightarrow \exists x\left(F^{-1}\left(A\right)\le x\wedge xFB\right)\right)$$
51	46 49 50	sylancr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(F^{-1}\left(A\right)\left(F\circ \le \right)B\leftrightarrow \exists x\left(F^{-1}\left(A\right)\le x\wedge xFB\right)\right)$$
52		fvex	$$⊢F^{-1}\left(B\right)\in \mathrm{V}$$
53		breq2	$$⊢x=F^{-1}\left(B\right)\to \left(F^{-1}\left(A\right)\le x\leftrightarrow F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)$$
54	52 53	ceqsexv	$$⊢\exists x\left(x=F^{-1}\left(B\right)\wedge F^{-1}\left(A\right)\le x\right)\leftrightarrow F^{-1}\left(A\right)\le F^{-1}\left(B\right)$$
55		eqcom	$$⊢x=F^{-1}\left(B\right)\leftrightarrow F^{-1}\left(B\right)=x$$
56		fnbrfvb	$$⊢\left(F^{-1}FnX\wedge B\in X\right)\to \left(F^{-1}\left(B\right)=x\leftrightarrow B{F}^{-1}x\right)$$
57	38 49 56	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(F^{-1}\left(B\right)=x\leftrightarrow B{F}^{-1}x\right)$$
58	55 57	bitrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(x=F^{-1}\left(B\right)\leftrightarrow B{F}^{-1}x\right)$$
59		vex	$$⊢x\in \mathrm{V}$$
60		brcnvg	$$⊢\left(B\in X\wedge x\in \mathrm{V}\right)\to \left(B{F}^{-1}x\leftrightarrow xFB\right)$$
61	49 59 60	sylancl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(B{F}^{-1}x\leftrightarrow xFB\right)$$
62	58 61	bitrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(x=F^{-1}\left(B\right)\leftrightarrow xFB\right)$$
63	62	anbi1d	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\left(x=F^{-1}\left(B\right)\wedge F^{-1}\left(A\right)\le x\right)\leftrightarrow \left(xFB\wedge F^{-1}\left(A\right)\le x\right)\right)$$
64	63	biancomd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\left(x=F^{-1}\left(B\right)\wedge F^{-1}\left(A\right)\le x\right)\leftrightarrow \left(F^{-1}\left(A\right)\le x\wedge xFB\right)\right)$$
65	64	exbidv	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\exists x\left(x=F^{-1}\left(B\right)\wedge F^{-1}\left(A\right)\le x\right)\leftrightarrow \exists x\left(F^{-1}\left(A\right)\le x\wedge xFB\right)\right)$$
66	54 65	bitr3id	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(F^{-1}\left(A\right)\le F^{-1}\left(B\right)\leftrightarrow \exists x\left(F^{-1}\left(A\right)\le x\wedge xFB\right)\right)$$
67	51 66	bitr4d	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(F^{-1}\left(A\right)\left(F\circ \le \right)B\leftrightarrow F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)$$
68	48 67	bitrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(\exists x\left(x=F^{-1}\left(A\right)\wedge x\left(F\circ \le \right)B\right)\leftrightarrow F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)$$
69	31 45 68	3bitrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(A\underset{\dot{}}{\le }B\leftrightarrow F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)$$
70	69	pm5.32da	$$⊢N\in {\mathbb{N}}_0\to \left(\left(\left(A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\le }B\right)\leftrightarrow \left(\left(A\in X\wedge B\in X\right)\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)\right)$$
71		df-3an	$$⊢\left(A\in X\wedge B\in X\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)\leftrightarrow \left(\left(A\in X\wedge B\in X\right)\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)$$
72	70 71	bitr4di	$$⊢N\in {\mathbb{N}}_0\to \left(\left(\left(A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\le }B\right)\leftrightarrow \left(A\in X\wedge B\in X\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)\right)$$
73	29 72	bitrd	$$⊢N\in {\mathbb{N}}_0\to \left(A\underset{\dot{}}{\le }B\leftrightarrow \left(A\in X\wedge B\in X\wedge F^{-1}\left(A\right)\le F^{-1}\left(B\right)\right)\right)$$