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 V W dom C . -1 0 1 C W = I D

Proof

Step Hyp Ref Expression
1 tocyc01.1 C = toCyc D
2 simpl D V W dom C . -1 0 1 D V
3 simpr D V W dom C . -1 0 1 W dom C . -1 0 1
4 3 elin1d D V W dom C . -1 0 1 W dom C
5 eqid SymGrp D = SymGrp D
6 eqid Base SymGrp D = Base SymGrp D
7 1 5 6 tocycf D V C : w Word D | w : dom w 1-1 D Base SymGrp D
8 fdm C : w Word D | w : dom w 1-1 D Base SymGrp D dom C = w Word D | w : dom w 1-1 D
9 2 7 8 3syl D V W dom C . -1 0 1 dom C = w Word D | w : dom w 1-1 D
10 4 9 eleqtrd D V W dom C . -1 0 1 W w 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 w Word D | w : dom w 1-1 D W Word D W : dom W 1-1 D
16 10 15 sylib D V W dom C . -1 0 1 W Word D W : dom W 1-1 D
17 16 simpld D V W dom C . -1 0 1 W Word D
18 16 simprd D V W dom C . -1 0 1 W : dom W 1-1 D
19 1 2 17 18 tocycfv D V W dom C . -1 0 1 C W = I D ran W W cyclShift 1 W -1
20 19 adantr D V W dom C . -1 0 1 W = 0 C W = I D ran W W cyclShift 1 W -1
21 hasheq0 W dom C . -1 0 1 W = 0 W =
22 3 21 syl D V W dom C . -1 0 1 W = 0 W =
23 22 biimpa D V W dom C . -1 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 -1 = -1
32 cnv0 -1 =
33 31 32 eqtrdi W = W -1 =
34 33 coeq2d W = W cyclShift 1 W -1 = W cyclShift 1
35 co02 W cyclShift 1 =
36 34 35 eqtrdi W = W cyclShift 1 W -1 =
37 30 36 uneq12d W = I D ran W W cyclShift 1 W -1 = I D
38 un0 I D = I D
39 37 38 eqtrdi W = I D ran W W cyclShift 1 W -1 = I D
40 23 39 syl D V W dom C . -1 0 1 W = 0 I D ran W W cyclShift 1 W -1 = I D
41 20 40 eqtrd D V W dom C . -1 0 1 W = 0 C W = I D
42 19 adantr D V W dom C . -1 0 1 W = 1 C W = I D ran W W cyclShift 1 W -1
43 17 adantr D V W dom C . -1 0 1 W = 1 W Word D
44 1zzd D V W dom C . -1 0 1 W = 1 1
45 simpr D V W dom C . -1 0 1 W = 1 W = 1
46 1cshid W Word D 1 W = 1 W cyclShift 1 = W
47 43 44 45 46 syl3anc D V W dom C . -1 0 1 W = 1 W cyclShift 1 = W
48 47 coeq1d D V W dom C . -1 0 1 W = 1 W cyclShift 1 W -1 = W W -1
49 wrdf W Word D W : 0 ..^ W D
50 ffun W : 0 ..^ W D Fun W
51 funcocnv2 Fun W W W -1 = I ran W
52 43 49 50 51 4syl D V W dom C . -1 0 1 W = 1 W W -1 = I ran W
53 48 52 eqtrd D V W dom C . -1 0 1 W = 1 W cyclShift 1 W -1 = I ran W
54 53 uneq2d D V W dom C . -1 0 1 W = 1 I D ran W W cyclShift 1 W -1 = I D ran W I ran W
55 resundi I D ran W ran W = I D ran W I ran W
56 frn W : 0 ..^ W D ran W D
57 undifr ran W D D ran W ran W = D
58 56 57 sylib W : 0 ..^ W D D ran W ran W = D
59 43 49 58 3syl D V W dom C . -1 0 1 W = 1 D ran W ran W = D
60 59 reseq2d D V W dom C . -1 0 1 W = 1 I D ran W ran W = I D
61 55 60 eqtr3id D V W dom C . -1 0 1 W = 1 I D ran W I ran W = I D
62 42 54 61 3eqtrd D V W dom C . -1 0 1 W = 1 C W = I D
63 3 elin2d D V W dom C . -1 0 1 W . -1 0 1
64 hashf . : V 0 +∞
65 ffn . : V 0 +∞ . Fn V
66 elpreima . Fn V W . -1 0 1 W V W 0 1
67 64 65 66 mp2b W . -1 0 1 W V W 0 1
68 63 67 sylib D V W dom C . -1 0 1 W V W 0 1
69 68 simprd D V W dom C . -1 0 1 W 0 1
70 elpri W 0 1 W = 0 W = 1
71 69 70 syl D V W dom C . -1 0 1 W = 0 W = 1
72 41 62 71 mpjaodan D V W dom C . -1 0 1 C W = I D