Metamath Proof Explorer

Theorem cycpmcl

Description: Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses tocycval.1 
|- C = ( toCyc ` D )
tocycfv.d 
|- ( ph -> D e. V )
tocycfv.w 
|- ( ph -> W e. Word D )
tocycfv.1 
|- ( ph -> W : dom W -1-1-> D )
cycpmcl.s 
|- S = ( SymGrp ` D )
Assertion cycpmcl 
|- ( ph -> ( C ` W ) e. ( Base ` S ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 
 |-  C = ( toCyc ` D )
2 tocycfv.d 
 |-  ( ph -> D e. V )
3 tocycfv.w 
 |-  ( ph -> W e. Word D )
4 tocycfv.1 
 |-  ( ph -> W : dom W -1-1-> D )
5 cycpmcl.s 
 |-  S = ( SymGrp ` D )
6 f1oi 
 |-  ( _I |` ( D \ ran W ) ) : ( D \ ran W ) -1-1-onto-> ( D \ ran W )
7 6 a1i 
 |-  ( ph -> ( _I |` ( D \ ran W ) ) : ( D \ ran W ) -1-1-onto-> ( D \ ran W ) )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 cshwf 
 |-  ( ( W e. Word D /\ 1 e. ZZ ) -> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) --> D )
10 3 8 9 syl2anc 
 |-  ( ph -> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) --> D )
11 10 ffnd 
 |-  ( ph -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
12 df-f1 
 |-  ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
13 4 12 sylib 
 |-  ( ph -> ( W : dom W --> D /\ Fun `' W ) )
14 13 simprd 
 |-  ( ph -> Fun `' W )
15 eqid 
 |-  ( W cyclShift 1 ) = ( W cyclShift 1 )
16 cshinj 
 |-  ( ( W e. Word D /\ Fun `' W /\ 1 e. ZZ ) -> ( ( W cyclShift 1 ) = ( W cyclShift 1 ) -> Fun `' ( W cyclShift 1 ) ) )
17 15 16 mpi 
 |-  ( ( W e. Word D /\ Fun `' W /\ 1 e. ZZ ) -> Fun `' ( W cyclShift 1 ) )
18 3 14 8 17 syl3anc 
 |-  ( ph -> Fun `' ( W cyclShift 1 ) )
19 f1orn 
 |-  ( ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ran ( W cyclShift 1 ) <-> ( ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) /\ Fun `' ( W cyclShift 1 ) ) )
20 11 18 19 sylanbrc 
 |-  ( ph -> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ran ( W cyclShift 1 ) )
21 eqidd 
 |-  ( ph -> ( W cyclShift 1 ) = ( W cyclShift 1 ) )
22 wrdf 
 |-  ( W e. Word D -> W : ( 0 ..^ ( # ` W ) ) --> D )
23 3 22 syl 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> D )
24 23 fdmd 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
25 cshwrnid 
 |-  ( ( W e. Word D /\ 1 e. ZZ ) -> ran ( W cyclShift 1 ) = ran W )
26 3 8 25 syl2anc 
 |-  ( ph -> ran ( W cyclShift 1 ) = ran W )
27 26 eqcomd 
 |-  ( ph -> ran W = ran ( W cyclShift 1 ) )
28 21 24 27 f1oeq123d 
 |-  ( ph -> ( ( W cyclShift 1 ) : dom W -1-1-onto-> ran W <-> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ran ( W cyclShift 1 ) ) )
29 20 28 mpbird 
 |-  ( ph -> ( W cyclShift 1 ) : dom W -1-1-onto-> ran W )
30 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
31 f1ocnv 
 |-  ( W : dom W -1-1-onto-> ran W -> `' W : ran W -1-1-onto-> dom W )
32 4 30 31 3syl 
 |-  ( ph -> `' W : ran W -1-1-onto-> dom W )
33 f1oco 
 |-  ( ( ( W cyclShift 1 ) : dom W -1-1-onto-> ran W /\ `' W : ran W -1-1-onto-> dom W ) -> ( ( W cyclShift 1 ) o. `' W ) : ran W -1-1-onto-> ran W )
34 29 32 33 syl2anc 
 |-  ( ph -> ( ( W cyclShift 1 ) o. `' W ) : ran W -1-1-onto-> ran W )
35 incom 
 |-  ( ran W i^i ( D \ ran W ) ) = ( ( D \ ran W ) i^i ran W )
36 disjdif 
 |-  ( ran W i^i ( D \ ran W ) ) = (/)
37 35 36 eqtr3i 
 |-  ( ( D \ ran W ) i^i ran W ) = (/)
38 37 a1i 
 |-  ( ph -> ( ( D \ ran W ) i^i ran W ) = (/) )
39 f1oun 
 |-  ( ( ( ( _I |` ( D \ ran W ) ) : ( D \ ran W ) -1-1-onto-> ( D \ ran W ) /\ ( ( W cyclShift 1 ) o. `' W ) : ran W -1-1-onto-> ran W ) /\ ( ( ( D \ ran W ) i^i ran W ) = (/) /\ ( ( D \ ran W ) i^i ran W ) = (/) ) ) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) : ( ( D \ ran W ) u. ran W ) -1-1-onto-> ( ( D \ ran W ) u. ran W ) )
40 7 34 38 38 39 syl22anc 
 |-  ( ph -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) : ( ( D \ ran W ) u. ran W ) -1-1-onto-> ( ( D \ ran W ) u. ran W ) )
41 1 2 3 4 tocycfv 
 |-  ( ph -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
42 uncom 
 |-  ( ran W u. ( D \ ran W ) ) = ( ( D \ ran W ) u. ran W )
43 23 frnd 
 |-  ( ph -> ran W C_ D )
44 undif 
 |-  ( ran W C_ D <-> ( ran W u. ( D \ ran W ) ) = D )
45 43 44 sylib 
 |-  ( ph -> ( ran W u. ( D \ ran W ) ) = D )
46 42 45 syl5reqr 
 |-  ( ph -> D = ( ( D \ ran W ) u. ran W ) )
47 41 46 46 f1oeq123d 
 |-  ( ph -> ( ( C ` W ) : D -1-1-onto-> D <-> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) : ( ( D \ ran W ) u. ran W ) -1-1-onto-> ( ( D \ ran W ) u. ran W ) ) )
48 40 47 mpbird 
 |-  ( ph -> ( C ` W ) : D -1-1-onto-> D )
49 fvex 
 |-  ( C ` W ) e. _V
50 eqid 
 |-  ( Base ` S ) = ( Base ` S )
51 5 50 elsymgbas2 
 |-  ( ( C ` W ) e. _V -> ( ( C ` W ) e. ( Base ` S ) <-> ( C ` W ) : D -1-1-onto-> D ) )
52 49 51 ax-mp 
 |-  ( ( C ` W ) e. ( Base ` S ) <-> ( C ` W ) : D -1-1-onto-> D )
53 48 52 sylibr 
 |-  ( ph -> ( C ` W ) e. ( Base ` S ) )