cycpmrn

Description: The range of the word used to build a cycle is the cycle's orbit, i.e. the set of points it moves. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypotheses	cycpmrn.1	$⊢ M = toCyc (D)$
	cycpmrn.2	$⊢ φ \to D \in V$
	cycpmrn.3	$⊢ φ \to W \in Word D$
	cycpmrn.4	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
	cycpmrn.5	$⊢ φ \to 1 < \|W\|$
Assertion	cycpmrn	$⊢ φ \to ran W = dom (M (W) ∖ I)$

Proof

Step	Hyp	Ref	Expression
1		cycpmrn.1	$⊢ M = toCyc (D)$
2		cycpmrn.2	$⊢ φ \to D \in V$
3		cycpmrn.3	$⊢ φ \to W \in Word D$
4		cycpmrn.4	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
5		cycpmrn.5	$⊢ φ \to 1 < \|W\|$
6	4	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to W : dom W \underset{1-1}{⟶} D$
7		simpllr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x \in dom W$
8		fzo0ss1	$⊢ (1 ..^\|W\|) \subseteq (0 ..^\|W\|)$
9		simpr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x \in (0 ..^\|W\| - 1)$
10		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
11	3 10	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
12	11	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to \|W\| \in ℕ_{0}$
13	12	nn0zd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to \|W\| \in ℤ$
14		1zzd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to 1 \in ℤ$
15		fzoaddel2	$⊢ (x \in (0 ..^\|W\| - 1) \land \|W\| \in ℤ \land 1 \in ℤ) \to x + 1 \in (1 ..^\|W\|)$
16	9 13 14 15	syl3anc	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x + 1 \in (1 ..^\|W\|)$
17	8 16	sseldi	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x + 1 \in (0 ..^\|W\|)$
18	3	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to W \in Word D$
19		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
20	18 19	syl	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to dom W = (0 ..^\|W\|)$
21	17 20	eleqtrrd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x + 1 \in dom W$
22		fzossz	$⊢ (0 ..^\|W\| - 1) \subseteq ℤ$
23	22 9	sseldi	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x \in ℤ$
24	23	zred	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x \in ℝ$
25	24	ltp1d	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x < x + 1$
26	24 25	ltned	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to x \neq x + 1$
27		f1veqaeq	$⊢ (W : dom W \underset{1-1}{⟶} D \land (x \in dom W \land x + 1 \in dom W)) \to (W (x) = W (x + 1) \to x = x + 1)$
28	27	necon3d	$⊢ (W : dom W \underset{1-1}{⟶} D \land (x \in dom W \land x + 1 \in dom W)) \to (x \neq x + 1 \to W (x) \neq W (x + 1))$
29	28	anassrs	$⊢ ((W : dom W \underset{1-1}{⟶} D \land x \in dom W) \land x + 1 \in dom W) \to (x \neq x + 1 \to W (x) \neq W (x + 1))$
30	29	imp	$⊢ (((W : dom W \underset{1-1}{⟶} D \land x \in dom W) \land x + 1 \in dom W) \land x \neq x + 1) \to W (x) \neq W (x + 1)$
31	6 7 21 26 30	syl1111anc	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to W (x) \neq W (x + 1)$
32	2	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to D \in V$
33	1 32 18 6 9	cycpmfv1	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to M (W) (W (x)) = W (x + 1)$
34	31 33	neeqtrrd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to W (x) \neq M (W) (W (x))$
35	34	necomd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to M (W) (W (x)) \neq W (x)$
36		simplr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to y = W (x)$
37	36	fveq2d	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to M (W) (y) = M (W) (W (x))$
38	35 37 36	3netr4d	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x \in (0 ..^\|W\| - 1)) \to M (W) (y) \neq y$
39	4	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to W : dom W \underset{1-1}{⟶} D$
40	3	ad3antrrr	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to W \in Word D$
41		eldmne0	$⊢ x \in dom W \to W \neq \emptyset$
42	41	ad2antlr	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to W \neq \emptyset$
43		lennncl	$⊢ (W \in Word D \land W \neq \emptyset) \to \|W\| \in ℕ$
44	40 42 43	syl2anc	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to \|W\| \in ℕ$
45		lbfzo0	$⊢ 0 \in (0 ..^\|W\|) \leftrightarrow \|W\| \in ℕ$
46	44 45	sylibr	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to 0 \in (0 ..^\|W\|)$
47	40 19	syl	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to dom W = (0 ..^\|W\|)$
48	46 47	eleqtrrd	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to 0 \in dom W$
49	48	adantr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to 0 \in dom W$
50		simpllr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to x \in dom W$
51		0red	$⊢ φ \to 0 \in ℝ$
52		1red	$⊢ φ \to 1 \in ℝ$
53	11	nn0red	$⊢ φ \to \|W\| \in ℝ$
54	52 53	posdifd	$⊢ φ \to (1 < \|W\| \leftrightarrow 0 < \|W\| - 1)$
55	5 54	mpbid	$⊢ φ \to 0 < \|W\| - 1$
56	51 55	ltned	$⊢ φ \to 0 \neq \|W\| - 1$
57	56	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to 0 \neq \|W\| - 1$
58		simpr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to x = \|W\| - 1$
59	57 58	neeqtrrd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to 0 \neq x$
60		f1veqaeq	$⊢ (W : dom W \underset{1-1}{⟶} D \land (0 \in dom W \land x \in dom W)) \to (W (0) = W (x) \to 0 = x)$
61	60	necon3d	$⊢ (W : dom W \underset{1-1}{⟶} D \land (0 \in dom W \land x \in dom W)) \to (0 \neq x \to W (0) \neq W (x))$
62	61	anassrs	$⊢ ((W : dom W \underset{1-1}{⟶} D \land 0 \in dom W) \land x \in dom W) \to (0 \neq x \to W (0) \neq W (x))$
63	62	imp	$⊢ (((W : dom W \underset{1-1}{⟶} D \land 0 \in dom W) \land x \in dom W) \land 0 \neq x) \to W (0) \neq W (x)$
64	39 49 50 59 63	syl1111anc	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to W (0) \neq W (x)$
65		simplr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to y = W (x)$
66	65	fveq2d	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to M (W) (y) = M (W) (W (x))$
67	2	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to D \in V$
68	3	ad4antr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to W \in Word D$
69	44	nngt0d	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to 0 < \|W\|$
70	69	adantr	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to 0 < \|W\|$
71	1 67 68 39 70 58	cycpmfv2	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to M (W) (W (x)) = W (0)$
72	66 71	eqtrd	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to M (W) (y) = W (0)$
73	64 72 65	3netr4d	$⊢ ((((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \land x = \|W\| - 1) \to M (W) (y) \neq y$
74		simplr	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to x \in dom W$
75	74 47	eleqtrd	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to x \in (0 ..^\|W\|)$
76		0z	$⊢ 0 \in ℤ$
77		0p1e1	$⊢ 0 + 1 = 1$
78	77	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
79		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
80	78 79	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
81	44 80	eleqtrrdi	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to \|W\| \in ℤ_{\geq (0 + 1)}$
82		fzosplitsnm1	$⊢ (0 \in ℤ \land \|W\| \in ℤ_{\geq (0 + 1)}) \to (0 ..^\|W\|) = (0 ..^\|W\| - 1) \cup \{\|W\| - 1\}$
83	76 81 82	sylancr	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to (0 ..^\|W\|) = (0 ..^\|W\| - 1) \cup \{\|W\| - 1\}$
84	75 83	eleqtrd	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to x \in ((0 ..^\|W\| - 1) \cup \{\|W\| - 1\})$
85		elun	$⊢ x \in ((0 ..^\|W\| - 1) \cup \{\|W\| - 1\}) \leftrightarrow (x \in (0 ..^\|W\| - 1) \lor x \in \{\|W\| - 1\})$
86	84 85	sylib	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to (x \in (0 ..^\|W\| - 1) \lor x \in \{\|W\| - 1\})$
87		velsn	$⊢ x \in \{\|W\| - 1\} \leftrightarrow x = \|W\| - 1$
88	87	orbi2i	$⊢ (x \in (0 ..^\|W\| - 1) \lor x \in \{\|W\| - 1\}) \leftrightarrow (x \in (0 ..^\|W\| - 1) \lor x = \|W\| - 1)$
89	86 88	sylib	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to (x \in (0 ..^\|W\| - 1) \lor x = \|W\| - 1)$
90	38 73 89	mpjaodan	$⊢ (((φ \land y \in ran W) \land x \in dom W) \land y = W (x)) \to M (W) (y) \neq y$
91		f1fun	$⊢ W : dom W \underset{1-1}{⟶} D \to Fun W$
92		elrnrexdmb	$⊢ Fun W \to (y \in ran W \leftrightarrow \exists x \in dom W y = W (x))$
93	4 91 92	3syl	$⊢ φ \to (y \in ran W \leftrightarrow \exists x \in dom W y = W (x))$
94	93	biimpa	$⊢ (φ \land y \in ran W) \to \exists x \in dom W y = W (x)$
95	90 94	r19.29a	$⊢ (φ \land y \in ran W) \to M (W) (y) \neq y$
96		eqid	$⊢ SymGrp (D) = SymGrp (D)$
97	1 2 3 4 96	cycpmcl	$⊢ φ \to M (W) \in {Base}_{SymGrp (D)}$
98		eqid	$⊢ {Base}_{SymGrp (D)} = {Base}_{SymGrp (D)}$
99	96 98	elsymgbas	$⊢ D \in V \to (M (W) \in {Base}_{SymGrp (D)} \leftrightarrow M (W) : D \underset{1-1 onto}{⟶} D)$
100	2 99	syl	$⊢ φ \to (M (W) \in {Base}_{SymGrp (D)} \leftrightarrow M (W) : D \underset{1-1 onto}{⟶} D)$
101	97 100	mpbid	$⊢ φ \to M (W) : D \underset{1-1 onto}{⟶} D$
102		f1ofn	$⊢ M (W) : D \underset{1-1 onto}{⟶} D \to M (W) Fn D$
103	101 102	syl	$⊢ φ \to M (W) Fn D$
104	103	adantr	$⊢ (φ \land y \in ran W) \to M (W) Fn D$
105		wrdf	$⊢ W \in Word D \to W : (0 ..^\|W\|) ⟶ D$
106		frn	$⊢ W : (0 ..^\|W\|) ⟶ D \to ran W \subseteq D$
107	3 105 106	3syl	$⊢ φ \to ran W \subseteq D$
108	107	sselda	$⊢ (φ \land y \in ran W) \to y \in D$
109		fnelnfp	$⊢ (M (W) Fn D \land y \in D) \to (y \in dom (M (W) ∖ I) \leftrightarrow M (W) (y) \neq y)$
110	104 108 109	syl2anc	$⊢ (φ \land y \in ran W) \to (y \in dom (M (W) ∖ I) \leftrightarrow M (W) (y) \neq y)$
111	95 110	mpbird	$⊢ (φ \land y \in ran W) \to y \in dom (M (W) ∖ I)$
112	111	ex	$⊢ φ \to (y \in ran W \to y \in dom (M (W) ∖ I))$
113	112	ssrdv	$⊢ φ \to ran W \subseteq dom (M (W) ∖ I)$
114	1 2 3 4	tocycfv	$⊢ φ \to M (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
115	114	difeq1d	$⊢ φ \to M (W) ∖ I = (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I$
116	115	dmeqd	$⊢ φ \to dom (M (W) ∖ I) = dom ((({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I)$
117		difundir	$⊢ (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I = (({I ↾}_{(D ∖ ran W)}) ∖ I) \cup (((W cyclShift 1) \circ W^{-1}) ∖ I)$
118		resdifcom	$⊢ ({I ↾}_{(D ∖ ran W)}) ∖ I = {(I ∖ I) ↾}_{(D ∖ ran W)}$
119		difid	$⊢ I ∖ I = \emptyset$
120	119	reseq1i	$⊢ {(I ∖ I) ↾}_{(D ∖ ran W)} = {\emptyset ↾}_{(D ∖ ran W)}$
121		0res	$⊢ {\emptyset ↾}_{(D ∖ ran W)} = \emptyset$
122	118 120 121	3eqtri	$⊢ ({I ↾}_{(D ∖ ran W)}) ∖ I = \emptyset$
123	122	uneq1i	$⊢ (({I ↾}_{(D ∖ ran W)}) ∖ I) \cup (((W cyclShift 1) \circ W^{-1}) ∖ I) = \emptyset \cup (((W cyclShift 1) \circ W^{-1}) ∖ I)$
124		0un	$⊢ \emptyset \cup (((W cyclShift 1) \circ W^{-1}) ∖ I) = ((W cyclShift 1) \circ W^{-1}) ∖ I$
125	117 123 124	3eqtri	$⊢ (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I = ((W cyclShift 1) \circ W^{-1}) ∖ I$
126	125	dmeqi	$⊢ dom ((({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I) = dom (((W cyclShift 1) \circ W^{-1}) ∖ I)$
127		difss	$⊢ ((W cyclShift 1) \circ W^{-1}) ∖ I \subseteq (W cyclShift 1) \circ W^{-1}$
128		dmss	$⊢ ((W cyclShift 1) \circ W^{-1}) ∖ I \subseteq (W cyclShift 1) \circ W^{-1} \to dom (((W cyclShift 1) \circ W^{-1}) ∖ I) \subseteq dom ((W cyclShift 1) \circ W^{-1})$
129	127 128	ax-mp	$⊢ dom (((W cyclShift 1) \circ W^{-1}) ∖ I) \subseteq dom ((W cyclShift 1) \circ W^{-1})$
130		dmcoss	$⊢ dom ((W cyclShift 1) \circ W^{-1}) \subseteq dom W^{-1}$
131		df-rn	$⊢ ran W = dom W^{-1}$
132	130 131	sseqtrri	$⊢ dom ((W cyclShift 1) \circ W^{-1}) \subseteq ran W$
133	129 132	sstri	$⊢ dom (((W cyclShift 1) \circ W^{-1}) ∖ I) \subseteq ran W$
134	126 133	eqsstri	$⊢ dom ((({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ∖ I) \subseteq ran W$
135	116 134	eqsstrdi	$⊢ φ \to dom (M (W) ∖ I) \subseteq ran W$
136	113 135	eqssd	$⊢ φ \to ran W = dom (M (W) ∖ I)$

Metamath Proof Explorer

Theorem cycpmrn

Proof