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 
|- ( ph -> D e. V )
cycpmrn.3 
|- ( ph -> W e. Word D )
cycpmrn.4 
|- ( ph -> W : dom W -1-1-> D )
cycpmrn.5 
|- ( ph -> 1 < ( # ` W ) )
Assertion cycpmrn 
|- ( ph -> ran W = dom ( ( M ` W ) \ _I ) )

Proof

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