Metamath Proof Explorer

Theorem tocyc01

Description: Permutation cycles built from the empty set or a singleton are the identity. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Hypothesis tocyc01.1 
|- C = ( toCyc ` D )
Assertion tocyc01 
|- ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( C ` W ) = ( _I |` D ) )

Proof

Step Hyp Ref Expression
1 tocyc01.1 
 |-  C = ( toCyc ` D )
2 simpl 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> D e. V )
3 simpr 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) )
4 3 elin1d 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W e. dom C )
5 eqid 
 |-  ( SymGrp ` D ) = ( SymGrp ` D )
6 eqid 
 |-  ( Base ` ( SymGrp ` D ) ) = ( Base ` ( SymGrp ` D ) )
7 1 5 6 tocycf 
 |-  ( D e. V -> C : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` ( SymGrp ` D ) ) )
8 fdm 
 |-  ( C : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` ( SymGrp ` D ) ) -> dom C = { w e. Word D | w : dom w -1-1-> D } )
9 2 7 8 3syl 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> dom C = { w e. Word D | w : dom w -1-1-> D } )
10 4 9 eleqtrd 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W e. { w e. Word D | w : dom w -1-1-> D } )
11 id 
 |-  ( w = W -> w = W )
12 dmeq 
 |-  ( w = W -> dom w = dom W )
13 eqidd 
 |-  ( w = W -> D = D )
14 11 12 13 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
15 14 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
16 10 15 sylib 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( W e. Word D /\ W : dom W -1-1-> D ) )
17 16 simpld 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W e. Word D )
18 16 simprd 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W : dom W -1-1-> D )
19 1 2 17 18 tocycfv 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
20 19 adantr 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 0 ) -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
21 hasheq0 
 |-  ( W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) -> ( ( # ` W ) = 0 <-> W = (/) ) )
22 3 21 syl 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( ( # ` W ) = 0 <-> W = (/) ) )
23 22 biimpa 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 0 ) -> W = (/) )
24 rneq 
 |-  ( W = (/) -> ran W = ran (/) )
25 rn0 
 |-  ran (/) = (/)
26 24 25 eqtrdi 
 |-  ( W = (/) -> ran W = (/) )
27 26 difeq2d 
 |-  ( W = (/) -> ( D \ ran W ) = ( D \ (/) ) )
28 dif0 
 |-  ( D \ (/) ) = D
29 27 28 eqtrdi 
 |-  ( W = (/) -> ( D \ ran W ) = D )
30 29 reseq2d 
 |-  ( W = (/) -> ( _I |` ( D \ ran W ) ) = ( _I |` D ) )
31 cnveq 
 |-  ( W = (/) -> `' W = `' (/) )
32 cnv0 
 |-  `' (/) = (/)
33 31 32 eqtrdi 
 |-  ( W = (/) -> `' W = (/) )
34 33 coeq2d 
 |-  ( W = (/) -> ( ( W cyclShift 1 ) o. `' W ) = ( ( W cyclShift 1 ) o. (/) ) )
35 co02 
 |-  ( ( W cyclShift 1 ) o. (/) ) = (/)
36 34 35 eqtrdi 
 |-  ( W = (/) -> ( ( W cyclShift 1 ) o. `' W ) = (/) )
37 30 36 uneq12d 
 |-  ( W = (/) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) = ( ( _I |` D ) u. (/) ) )
38 un0 
 |-  ( ( _I |` D ) u. (/) ) = ( _I |` D )
39 37 38 eqtrdi 
 |-  ( W = (/) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) = ( _I |` D ) )
40 23 39 syl 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 0 ) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) = ( _I |` D ) )
41 20 40 eqtrd 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 0 ) -> ( C ` W ) = ( _I |` D ) )
42 19 adantr 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
43 17 adantr 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> W e. Word D )
44 1zzd 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> 1 e. ZZ )
45 simpr 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( # ` W ) = 1 )
46 1cshid 
 |-  ( ( W e. Word D /\ 1 e. ZZ /\ ( # ` W ) = 1 ) -> ( W cyclShift 1 ) = W )
47 43 44 45 46 syl3anc 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( W cyclShift 1 ) = W )
48 47 coeq1d 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( ( W cyclShift 1 ) o. `' W ) = ( W o. `' W ) )
49 wrdf 
 |-  ( W e. Word D -> W : ( 0 ..^ ( # ` W ) ) --> D )
50 ffun 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> D -> Fun W )
51 funcocnv2 
 |-  ( Fun W -> ( W o. `' W ) = ( _I |` ran W ) )
52 43 49 50 51 4syl 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( W o. `' W ) = ( _I |` ran W ) )
53 48 52 eqtrd 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( ( W cyclShift 1 ) o. `' W ) = ( _I |` ran W ) )
54 53 uneq2d 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) = ( ( _I |` ( D \ ran W ) ) u. ( _I |` ran W ) ) )
55 resundi 
 |-  ( _I |` ( ( D \ ran W ) u. ran W ) ) = ( ( _I |` ( D \ ran W ) ) u. ( _I |` ran W ) )
56 frn 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> D -> ran W C_ D )
57 undifr 
 |-  ( ran W C_ D <-> ( ( D \ ran W ) u. ran W ) = D )
58 56 57 sylib 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> D -> ( ( D \ ran W ) u. ran W ) = D )
59 43 49 58 3syl 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( ( D \ ran W ) u. ran W ) = D )
60 59 reseq2d 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( _I |` ( ( D \ ran W ) u. ran W ) ) = ( _I |` D ) )
61 55 60 eqtr3id 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( ( _I |` ( D \ ran W ) ) u. ( _I |` ran W ) ) = ( _I |` D ) )
62 42 54 61 3eqtrd 
 |-  ( ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) /\ ( # ` W ) = 1 ) -> ( C ` W ) = ( _I |` D ) )
63 3 elin2d 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> W e. ( `' # " { 0 , 1 } ) )
64 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
65 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
66 elpreima 
 |-  ( # Fn _V -> ( W e. ( `' # " { 0 , 1 } ) <-> ( W e. _V /\ ( # ` W ) e. { 0 , 1 } ) ) )
67 64 65 66 mp2b 
 |-  ( W e. ( `' # " { 0 , 1 } ) <-> ( W e. _V /\ ( # ` W ) e. { 0 , 1 } ) )
68 63 67 sylib 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( W e. _V /\ ( # ` W ) e. { 0 , 1 } ) )
69 68 simprd 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( # ` W ) e. { 0 , 1 } )
70 elpri 
 |-  ( ( # ` W ) e. { 0 , 1 } -> ( ( # ` W ) = 0 \/ ( # ` W ) = 1 ) )
71 69 70 syl 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( ( # ` W ) = 0 \/ ( # ` W ) = 1 ) )
72 41 62 71 mpjaodan 
 |-  ( ( D e. V /\ W e. ( dom C i^i ( `' # " { 0 , 1 } ) ) ) -> ( C ` W ) = ( _I |` D ) )