Metamath Proof Explorer

Theorem cycpmco2f1

Description: The word U used in cycpmco2 is injective, so it can represent a cycle and form a cyclic permutation ( MU ) . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c 
|- M = ( toCyc ` D )
cycpmco2.s 
|- S = ( SymGrp ` D )
cycpmco2.d 
|- ( ph -> D e. V )
cycpmco2.w 
|- ( ph -> W e. dom M )
cycpmco2.i 
|- ( ph -> I e. ( D \ ran W ) )
cycpmco2.j 
|- ( ph -> J e. ran W )
cycpmco2.e 
|- E = ( ( `' W ` J ) + 1 )
cycpmco2.1 
|- U = ( W splice <. E , E , <" I "> >. )
Assertion cycpmco2f1 
|- ( ph -> U : dom U -1-1-> D )

Proof

Step Hyp Ref Expression
1 cycpmco2.c 
 |-  M = ( toCyc ` D )
2 cycpmco2.s 
 |-  S = ( SymGrp ` D )
3 cycpmco2.d 
 |-  ( ph -> D e. V )
4 cycpmco2.w 
 |-  ( ph -> W e. dom M )
5 cycpmco2.i 
 |-  ( ph -> I e. ( D \ ran W ) )
6 cycpmco2.j 
 |-  ( ph -> J e. ran W )
7 cycpmco2.e 
 |-  E = ( ( `' W ` J ) + 1 )
8 cycpmco2.1 
 |-  U = ( W splice <. E , E , <" I "> >. )
9 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 1 2 10 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
12 3 11 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
13 12 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
14 4 13 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
15 9 14 sseldi 
 |-  ( ph -> W e. Word D )
16 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
17 15 16 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
18 5 eldifad 
 |-  ( ph -> I e. D )
19 18 s1cld 
 |-  ( ph -> <" I "> e. Word D )
20 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
21 17 19 20 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
22 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
23 15 22 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
24 id 
 |-  ( w = W -> w = W )
25 dmeq 
 |-  ( w = W -> dom w = dom W )
26 eqidd 
 |-  ( w = W -> D = D )
27 24 25 26 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
28 27 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
29 14 28 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
30 29 simprd 
 |-  ( ph -> W : dom W -1-1-> D )
31 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
32 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
33 30 31 32 3syl 
 |-  ( ph -> `' W : ran W --> dom W )
34 33 6 ffvelrnd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
35 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
36 15 35 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
37 34 36 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
38 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
39 37 38 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
40 7 39 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
41 15 30 40 pfxf1 
 |-  ( ph -> ( W prefix E ) : dom ( W prefix E ) -1-1-> D )
42 18 s1f1 
 |-  ( ph -> <" I "> : dom <" I "> -1-1-> D )
43 s1rn 
 |-  ( I e. D -> ran <" I "> = { I } )
44 18 43 syl 
 |-  ( ph -> ran <" I "> = { I } )
45 44 ineq2d 
 |-  ( ph -> ( ran ( W prefix E ) i^i ran <" I "> ) = ( ran ( W prefix E ) i^i { I } ) )
46 pfxrn2 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix E ) C_ ran W )
47 15 40 46 syl2anc 
 |-  ( ph -> ran ( W prefix E ) C_ ran W )
48 47 ssrind 
 |-  ( ph -> ( ran ( W prefix E ) i^i { I } ) C_ ( ran W i^i { I } ) )
49 5 eldifbd 
 |-  ( ph -> -. I e. ran W )
50 disjsn 
 |-  ( ( ran W i^i { I } ) = (/) <-> -. I e. ran W )
51 49 50 sylibr 
 |-  ( ph -> ( ran W i^i { I } ) = (/) )
52 48 51 sseqtrd 
 |-  ( ph -> ( ran ( W prefix E ) i^i { I } ) C_ (/) )
53 ss0 
 |-  ( ( ran ( W prefix E ) i^i { I } ) C_ (/) -> ( ran ( W prefix E ) i^i { I } ) = (/) )
54 52 53 syl 
 |-  ( ph -> ( ran ( W prefix E ) i^i { I } ) = (/) )
55 45 54 eqtrd 
 |-  ( ph -> ( ran ( W prefix E ) i^i ran <" I "> ) = (/) )
56 3 17 19 41 42 55 ccatf1 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) : dom ( ( W prefix E ) ++ <" I "> ) -1-1-> D )
57 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
58 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
59 58 biimpi 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
60 15 57 59 3syl 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
61 15 40 60 30 swrdf1 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) : dom ( W substr <. E , ( # ` W ) >. ) -1-1-> D )
62 ccatrn 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) )
63 17 19 62 syl2anc 
 |-  ( ph -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) )
64 63 ineq1d 
 |-  ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) u. ran <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) )
65 indir 
 |-  ( ( ran ( W prefix E ) u. ran <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) )
66 64 65 eqtrdi 
 |-  ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) )
67 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
68 67 40 sseldi 
 |-  ( ph -> E e. NN0 )
69 pfxval 
 |-  ( ( W e. Word D /\ E e. NN0 ) -> ( W prefix E ) = ( W substr <. 0 , E >. ) )
70 15 68 69 syl2anc 
 |-  ( ph -> ( W prefix E ) = ( W substr <. 0 , E >. ) )
71 70 rneqd 
 |-  ( ph -> ran ( W prefix E ) = ran ( W substr <. 0 , E >. ) )
72 71 ineq1d 
 |-  ( ph -> ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( W substr <. 0 , E >. ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) )
73 0elfz 
 |-  ( E e. NN0 -> 0 e. ( 0 ... E ) )
74 68 73 syl 
 |-  ( ph -> 0 e. ( 0 ... E ) )
75 elfzuz3 
 |-  ( E e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` E ) )
76 eluzfz1 
 |-  ( ( # ` W ) e. ( ZZ>= ` E ) -> E e. ( E ... ( # ` W ) ) )
77 40 75 76 3syl 
 |-  ( ph -> E e. ( E ... ( # ` W ) ) )
78 eluzfz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` E ) -> ( # ` W ) e. ( E ... ( # ` W ) ) )
79 40 75 78 3syl 
 |-  ( ph -> ( # ` W ) e. ( E ... ( # ` W ) ) )
80 15 74 40 30 77 79 swrdrndisj 
 |-  ( ph -> ( ran ( W substr <. 0 , E >. ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) )
81 72 80 eqtrd 
 |-  ( ph -> ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) )
82 incom 
 |-  ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> )
83 44 ineq2d 
 |-  ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> ) = ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) )
84 swrdrn2 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. E , ( # ` W ) >. ) C_ ran W )
85 15 40 60 84 syl3anc 
 |-  ( ph -> ran ( W substr <. E , ( # ` W ) >. ) C_ ran W )
86 85 ssrind 
 |-  ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ ( ran W i^i { I } ) )
87 86 51 sseqtrd 
 |-  ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ (/) )
88 ss0 
 |-  ( ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ (/) -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) = (/) )
89 87 88 syl 
 |-  ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) = (/) )
90 83 89 eqtrd 
 |-  ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> ) = (/) )
91 82 90 syl5eq 
 |-  ( ph -> ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) )
92 81 91 uneq12d 
 |-  ( ph -> ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) = ( (/) u. (/) ) )
93 unidm 
 |-  ( (/) u. (/) ) = (/)
94 93 a1i 
 |-  ( ph -> ( (/) u. (/) ) = (/) )
95 66 92 94 3eqtrd 
 |-  ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) )
96 3 21 23 56 61 95 ccatf1 
 |-  ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) : dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) -1-1-> D )
97 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
98 7 97 eqeltrid 
 |-  ( ph -> E e. _V )
99 splval 
 |-  ( ( W e. dom M /\ ( E e. _V /\ E e. _V /\ <" I "> e. Word D ) ) -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
100 4 98 98 19 99 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
101 8 100 syl5eq 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
102 101 dmeqd 
 |-  ( ph -> dom U = dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
103 eqidd 
 |-  ( ph -> D = D )
104 101 102 103 f1eq123d 
 |-  ( ph -> ( U : dom U -1-1-> D <-> ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) : dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) -1-1-> D ) )
105 96 104 mpbird 
 |-  ( ph -> U : dom U -1-1-> D )