Metamath Proof Explorer


Theorem cycpmconjs

Description: All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023)

Ref Expression
Hypotheses cycpmconjs.c C = M . -1 P
cycpmconjs.s S = SymGrp D
cycpmconjs.n N = D
cycpmconjs.m M = toCyc D
cycpmconjs.b B = Base S
cycpmconjs.a + ˙ = + S
cycpmconjs.l - ˙ = - S
cycpmconjs.p φ P 0 N
cycpmconjs.d φ D Fin
cycpmconjs.q φ Q C
cycpmconjs.t φ T C
Assertion cycpmconjs φ p B Q = p + ˙ T - ˙ p

Proof

Step Hyp Ref Expression
1 cycpmconjs.c C = M . -1 P
2 cycpmconjs.s S = SymGrp D
3 cycpmconjs.n N = D
4 cycpmconjs.m M = toCyc D
5 cycpmconjs.b B = Base S
6 cycpmconjs.a + ˙ = + S
7 cycpmconjs.l - ˙ = - S
8 cycpmconjs.p φ P 0 N
9 cycpmconjs.d φ D Fin
10 cycpmconjs.q φ Q C
11 cycpmconjs.t φ T C
12 1 2 3 4 5 6 7 8 9 10 cycpmconjslem2 φ q q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N
13 1 2 3 4 5 6 7 8 9 11 cycpmconjslem2 φ t t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N
14 13 ad2antrr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N
15 9 ad4antr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N D Fin
16 simp-4r φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q : 0 ..^ N 1-1 onto D
17 f1ocnv t : 0 ..^ N 1-1 onto D t -1 : D 1-1 onto 0 ..^ N
18 17 ad2antlr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N t -1 : D 1-1 onto 0 ..^ N
19 f1oco q : 0 ..^ N 1-1 onto D t -1 : D 1-1 onto 0 ..^ N q t -1 : D 1-1 onto D
20 16 18 19 syl2anc φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 : D 1-1 onto D
21 2 5 elsymgbas D Fin q t -1 B q t -1 : D 1-1 onto D
22 21 biimpar D Fin q t -1 : D 1-1 onto D q t -1 B
23 15 20 22 syl2anc φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 B
24 simpr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p = q t -1 p = q t -1
25 24 oveq1d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p = q t -1 p + ˙ T = q t -1 + ˙ T
26 25 24 oveq12d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p = q t -1 p + ˙ T - ˙ p = q t -1 + ˙ T - ˙ q t -1
27 26 eqeq2d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p = q t -1 Q = p + ˙ T - ˙ p Q = q t -1 + ˙ T - ˙ q t -1
28 simpllr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N
29 simpr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N
30 28 29 eqtr4d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q -1 Q q = t -1 T t
31 30 coeq1d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q -1 Q q q -1 = t -1 T t q -1
32 31 coeq2d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q q q -1 = q t -1 T t q -1
33 coass q q -1 Q q q -1 = q q -1 Q q q -1
34 coass q q -1 Q = q q -1 Q
35 34 coeq1i q q -1 Q q q -1 = q q -1 Q q q -1
36 coass q -1 Q q q -1 = q -1 Q q q -1
37 36 coeq2i q q -1 Q q q -1 = q q -1 Q q q -1
38 33 35 37 3eqtr4ri q q -1 Q q q -1 = q q -1 Q q q -1
39 f1ococnv2 q : 0 ..^ N 1-1 onto D q q -1 = I D
40 16 39 syl φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 = I D
41 40 coeq1d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q = I D Q
42 1 2 3 4 5 cycpmgcl D Fin P 0 N C B
43 9 8 42 syl2anc φ C B
44 43 10 sseldd φ Q B
45 2 5 elsymgbas D Fin Q B Q : D 1-1 onto D
46 45 biimpa D Fin Q B Q : D 1-1 onto D
47 9 44 46 syl2anc φ Q : D 1-1 onto D
48 f1of Q : D 1-1 onto D Q : D D
49 fcoi2 Q : D D I D Q = Q
50 47 48 49 3syl φ I D Q = Q
51 50 ad4antr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N I D Q = Q
52 41 51 eqtrd φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q = Q
53 52 40 coeq12d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q q q -1 = Q I D
54 fcoi1 Q : D D Q I D = Q
55 47 48 54 3syl φ Q I D = Q
56 55 ad4antr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N Q I D = Q
57 53 56 eqtrd φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q q q -1 = Q
58 38 57 syl5eq φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q q -1 Q q q -1 = Q
59 coass q t -1 T t q -1 = q t -1 T t q -1
60 coass q t -1 T = q t -1 T
61 60 coeq1i q t -1 T t q -1 = q t -1 T t q -1
62 coass t -1 T t q -1 = t -1 T t q -1
63 62 coeq2i q t -1 T t q -1 = q t -1 T t q -1
64 59 61 63 3eqtr4i q t -1 T t q -1 = q t -1 T t q -1
65 43 11 sseldd φ T B
66 65 ad4antr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N T B
67 2 5 6 symgov q t -1 B T B q t -1 + ˙ T = q t -1 T
68 23 66 67 syl2anc φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 + ˙ T = q t -1 T
69 68 oveq1d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 + ˙ T - ˙ q t -1 = q t -1 T - ˙ q t -1
70 2 symggrp D Fin S Grp
71 9 70 syl φ S Grp
72 71 ad4antr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N S Grp
73 5 6 grpcl S Grp q t -1 B T B q t -1 + ˙ T B
74 72 23 66 73 syl3anc φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 + ˙ T B
75 68 74 eqeltrrd φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 T B
76 2 5 7 symgsubg q t -1 T B q t -1 B q t -1 T - ˙ q t -1 = q t -1 T q t -1 -1
77 75 23 76 syl2anc φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 T - ˙ q t -1 = q t -1 T q t -1 -1
78 cnvco q t -1 -1 = t -1 -1 q -1
79 f1orel t : 0 ..^ N 1-1 onto D Rel t
80 dfrel2 Rel t t -1 -1 = t
81 79 80 sylib t : 0 ..^ N 1-1 onto D t -1 -1 = t
82 81 coeq1d t : 0 ..^ N 1-1 onto D t -1 -1 q -1 = t q -1
83 78 82 syl5eq t : 0 ..^ N 1-1 onto D q t -1 -1 = t q -1
84 83 coeq2d t : 0 ..^ N 1-1 onto D q t -1 T q t -1 -1 = q t -1 T t q -1
85 84 ad2antlr φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 T q t -1 -1 = q t -1 T t q -1
86 69 77 85 3eqtrrd φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 T t q -1 = q t -1 + ˙ T - ˙ q t -1
87 64 86 eqtr3id φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N q t -1 T t q -1 = q t -1 + ˙ T - ˙ q t -1
88 32 58 87 3eqtr3d φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N Q = q t -1 + ˙ T - ˙ q t -1
89 23 27 88 rspcedvd φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p B Q = p + ˙ T - ˙ p
90 89 anasss φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N t : 0 ..^ N 1-1 onto D t -1 T t = I 0 ..^ P cyclShift 1 I P ..^ N p B Q = p + ˙ T - ˙ p
91 14 90 exlimddv φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N p B Q = p + ˙ T - ˙ p
92 91 anasss φ q : 0 ..^ N 1-1 onto D q -1 Q q = I 0 ..^ P cyclShift 1 I P ..^ N p B Q = p + ˙ T - ˙ p
93 12 92 exlimddv φ p B Q = p + ˙ T - ˙ p