Theorem zntoslem

Description: Lemma for zntos . (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	zntoslem	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Toset}$$

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	fvexi	$$⊢Y\in \mathrm{V}$$
7	6	a1i	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{V}$$
8	5	a1i	$$⊢N\in {\mathbb{N}}_0\to X={\mathrm{Base}}_Y$$
9	4	a1i	$$⊢N\in {\mathbb{N}}_0\to \underset{\dot{}}{\le }={\le }_Y$$
10	1 5 2 3	znf1o	$$⊢N\in {\mathbb{N}}_0\to F:W\underset{1-1\; onto}{⟶}X$$
11		f1ocnv	$$⊢F:W\underset{1-1\; onto}{⟶}X\to F^{-1}:X\underset{1-1\; onto}{⟶}W$$
12	10 11	syl	$$⊢N\in {\mathbb{N}}_0\to F^{-1}:X\underset{1-1\; onto}{⟶}W$$
13		f1of	$$⊢F^{-1}:X\underset{1-1\; onto}{⟶}W\to F^{-1}:X⟶W$$
14	12 13	syl	$$⊢N\in {\mathbb{N}}_0\to F^{-1}:X⟶W$$
15		sseq1	$$⊢\mathbb{Z}=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\to \left(\mathbb{Z}\subseteq \mathbb{Z}\leftrightarrow if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\subseteq \mathbb{Z}\right)$$
16		sseq1	$$⊢\left(0..^N\right)=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\to \left(\left(0..^N\right)\subseteq \mathbb{Z}\leftrightarrow if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\subseteq \mathbb{Z}\right)$$
17		ssid	$$⊢\mathbb{Z}\subseteq \mathbb{Z}$$
18		fzossz	$$⊢\left(0..^N\right)\subseteq \mathbb{Z}$$
19	15 16 17 18	keephyp	$$⊢if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\subseteq \mathbb{Z}$$
20	3 19	eqsstri	$$⊢W\subseteq \mathbb{Z}$$
21		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
22	20 21	sstri	$$⊢W\subseteq ℝ$$
23		fss	$$⊢\left(F^{-1}:X⟶W\wedge W\subseteq ℝ\right)\to F^{-1}:X⟶ℝ$$
24	14 22 23	sylancl	$$⊢N\in {\mathbb{N}}_0\to F^{-1}:X⟶ℝ$$
25	24	ffvelcdmda	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\right)\to F^{-1}\left(x\right)\in ℝ$$
26	25	leidd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\right)\to F^{-1}\left(x\right)\le F^{-1}\left(x\right)$$
27	1 2 3 4 5	znleval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge x\in X\right)\to \left(x\underset{\dot{}}{\le }x\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(x\right)\right)$$
28	27	3anidm23	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\right)\to \left(x\underset{\dot{}}{\le }x\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(x\right)\right)$$
29	26 28	mpbird	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\right)\to x\underset{\dot{}}{\le }x$$
30	1 2 3 4 5	znleval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(x\underset{\dot{}}{\le }y\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(y\right)\right)$$
31	1 2 3 4 5	znleval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge y\in X\wedge x\in X\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)$$
32	31	3com23	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(y\underset{\dot{}}{\le }x\leftrightarrow F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)$$
33	30 32	anbi12d	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\wedge F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)\right)$$
34	25	3adant3	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to F^{-1}\left(x\right)\in ℝ$$
35	24	ffvelcdmda	$$⊢\left(N\in {\mathbb{N}}_0\wedge y\in X\right)\to F^{-1}\left(y\right)\in ℝ$$
36	35	3adant2	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to F^{-1}\left(y\right)\in ℝ$$
37	34 36	letri3d	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(F^{-1}\left(x\right)=F^{-1}\left(y\right)\leftrightarrow \left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\wedge F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)\right)$$
38		f1of1	$$⊢F^{-1}:X\underset{1-1\; onto}{⟶}W\to F^{-1}:X\underset{1-1}{⟶}W$$
39	12 38	syl	$$⊢N\in {\mathbb{N}}_0\to F^{-1}:X\underset{1-1}{⟶}W$$
40		f1fveq	$$⊢\left(F^{-1}:X\underset{1-1}{⟶}W\wedge \left(x\in X\wedge y\in X\right)\right)\to \left(F^{-1}\left(x\right)=F^{-1}\left(y\right)\leftrightarrow x=y\right)$$
41	39 40	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\right)\right)\to \left(F^{-1}\left(x\right)=F^{-1}\left(y\right)\leftrightarrow x=y\right)$$
42	41	3impb	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(F^{-1}\left(x\right)=F^{-1}\left(y\right)\leftrightarrow x=y\right)$$
43	33 37 42	3bitr2d	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\leftrightarrow x=y\right)$$
44	43	biimpd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)$$
45	25	3ad2antr1	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to F^{-1}\left(x\right)\in ℝ$$
46	35	3ad2antr2	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to F^{-1}\left(y\right)\in ℝ$$
47	24	ffvelcdmda	$$⊢\left(N\in {\mathbb{N}}_0\wedge z\in X\right)\to F^{-1}\left(z\right)\in ℝ$$
48	47	3ad2antr3	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to F^{-1}\left(z\right)\in ℝ$$
49		letr	$$⊢\left(F^{-1}\left(x\right)\in ℝ\wedge F^{-1}\left(y\right)\in ℝ\wedge F^{-1}\left(z\right)\in ℝ\right)\to \left(\left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\wedge F^{-1}\left(y\right)\le F^{-1}\left(z\right)\right)\to F^{-1}\left(x\right)\le F^{-1}\left(z\right)\right)$$
50	45 46 48 49	syl3anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(\left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\wedge F^{-1}\left(y\right)\le F^{-1}\left(z\right)\right)\to F^{-1}\left(x\right)\le F^{-1}\left(z\right)\right)$$
51	30	3adant3r3	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(x\underset{\dot{}}{\le }y\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(y\right)\right)$$
52	1 2 3 4 5	znleval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge y\in X\wedge z\in X\right)\to \left(y\underset{\dot{}}{\le }z\leftrightarrow F^{-1}\left(y\right)\le F^{-1}\left(z\right)\right)$$
53	52	3adant3r1	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(y\underset{\dot{}}{\le }z\leftrightarrow F^{-1}\left(y\right)\le F^{-1}\left(z\right)\right)$$
54	51 53	anbi12d	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\wedge F^{-1}\left(y\right)\le F^{-1}\left(z\right)\right)\right)$$
55	1 2 3 4 5	znleval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge z\in X\right)\to \left(x\underset{\dot{}}{\le }z\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(z\right)\right)$$
56	55	3adant3r2	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(x\underset{\dot{}}{\le }z\leftrightarrow F^{-1}\left(x\right)\le F^{-1}\left(z\right)\right)$$
57	50 54 56	3imtr4d	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)$$
58	7 8 9 29 44 57	isposd	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Poset}$$
59	34 36	letrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\vee F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)$$
60	30 32	orbi12d	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(F^{-1}\left(x\right)\le F^{-1}\left(y\right)\vee F^{-1}\left(y\right)\le F^{-1}\left(x\right)\right)\right)$$
61	59 60	mpbird	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in X\wedge y\in X\right)\to \left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
62	61	3expb	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in X\wedge y\in X\right)\right)\to \left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
63	62	ralrimivva	$$⊢N\in {\mathbb{N}}_0\to \forall x\in X\forall y\in X\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)$$
64	5 4	istos	$$⊢Y\in \mathrm{Toset}\leftrightarrow \left(Y\in \mathrm{Poset}\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }x\right)\right)$$
65	58 63 64	sylanbrc	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Toset}$$