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 " ( `' # " { P } ) )
cycpmconjs.s 
|- S = ( SymGrp ` D )
cycpmconjs.n 
|- N = ( # ` D )
cycpmconjs.m 
|- M = ( toCyc ` D )
cycpmconjs.b 
|- B = ( Base ` S )
cycpmconjs.a 
|- .+ = ( +g ` S )
cycpmconjs.l 
|- .- = ( -g ` S )
cycpmconjs.p 
|- ( ph -> P e. ( 0 ... N ) )
cycpmconjs.d 
|- ( ph -> D e. Fin )
cycpmconjs.q 
|- ( ph -> Q e. C )
cycpmconjs.t 
|- ( ph -> T e. C )
Assertion cycpmconjs 
|- ( ph -> E. p e. B Q = ( ( p .+ T ) .- p ) )

Proof

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