Metamath Proof Explorer


Theorem 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 φ D V
cycpmrn.3 φ W Word D
cycpmrn.4 φ W : dom W 1-1 D
cycpmrn.5 φ 1 < W
Assertion cycpmrn φ ran W = dom M W I

Proof

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