Metamath Proof Explorer

Theorem cycpmconjv

Description: A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of Lang p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Hypotheses cycpmconjv.s 
|- S = ( SymGrp ` D )
cycpmconjv.m 
|- M = ( toCyc ` D )
cycpmconjv.p 
|- .+ = ( +g ` S )
cycpmconjv.l 
|- .- = ( -g ` S )
cycpmconjv.b 
|- B = ( Base ` S )
Assertion cycpmconjv 
|- ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( M ` ( G o. W ) ) )

Proof

Step Hyp Ref Expression
1 cycpmconjv.s 
 |-  S = ( SymGrp ` D )
2 cycpmconjv.m 
 |-  M = ( toCyc ` D )
3 cycpmconjv.p 
 |-  .+ = ( +g ` S )
4 cycpmconjv.l 
 |-  .- = ( -g ` S )
5 cycpmconjv.b 
 |-  B = ( Base ` S )
6 1 5 symgbasf1o 
 |-  ( G e. B -> G : D -1-1-onto-> D )
7 6 3ad2ant2 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> G : D -1-1-onto-> D )
8 simp3 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> W e. dom M )
9 2 1 5 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> B )
10 9 3ad2ant1 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> M : { w e. Word D | w : dom w -1-1-> D } --> B )
11 10 fdmd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> dom M = { w e. Word D | w : dom w -1-1-> D } )
12 8 11 eleqtrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> W e. { w e. Word D | w : dom w -1-1-> D } )
13 id 
 |-  ( w = W -> w = W )
14 dmeq 
 |-  ( w = W -> dom w = dom W )
15 eqidd 
 |-  ( w = W -> D = D )
16 13 14 15 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
17 16 elrab 
 |-  ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
18 12 17 sylib 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( W e. Word D /\ W : dom W -1-1-> D ) )
19 18 simprd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> W : dom W -1-1-> D )
20 f1f 
 |-  ( W : dom W -1-1-> D -> W : dom W --> D )
21 19 20 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> W : dom W --> D )
22 21 frnd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ran W C_ D )
23 7 22 cycpmconjvlem 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G |` ( D \ ran W ) ) o. `' G ) = ( _I |` ( D \ ran ( G |` ran W ) ) ) )
24 rnco 
 |-  ran ( G o. W ) = ran ( G |` ran W )
25 24 difeq2i 
 |-  ( D \ ran ( G o. W ) ) = ( D \ ran ( G |` ran W ) )
26 25 reseq2i 
 |-  ( _I |` ( D \ ran ( G o. W ) ) ) = ( _I |` ( D \ ran ( G |` ran W ) ) )
27 23 26 eqtr4di 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G |` ( D \ ran W ) ) o. `' G ) = ( _I |` ( D \ ran ( G o. W ) ) ) )
28 coass 
 |-  ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) = ( ( ( G o. W ) cyclShift 1 ) o. ( `' W o. `' G ) )
29 cnvco 
 |-  `' ( G o. W ) = ( `' W o. `' G )
30 29 coeq2i 
 |-  ( ( ( G o. W ) cyclShift 1 ) o. `' ( G o. W ) ) = ( ( ( G o. W ) cyclShift 1 ) o. ( `' W o. `' G ) )
31 28 30 eqtr4i 
 |-  ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) = ( ( ( G o. W ) cyclShift 1 ) o. `' ( G o. W ) )
32 31 a1i 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) = ( ( ( G o. W ) cyclShift 1 ) o. `' ( G o. W ) ) )
33 27 32 uneq12d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( ( G |` ( D \ ran W ) ) o. `' G ) u. ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) ) = ( ( _I |` ( D \ ran ( G o. W ) ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' ( G o. W ) ) ) )
34 simp2 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> G e. B )
35 10 12 ffvelcdmd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( M ` W ) e. B )
36 1 5 3 symgcl 
 |-  ( ( G e. B /\ ( M ` W ) e. B ) -> ( G .+ ( M ` W ) ) e. B )
37 34 35 36 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G .+ ( M ` W ) ) e. B )
38 eqid 
 |-  ( invg ` S ) = ( invg ` S )
39 5 3 38 4 grpsubval 
 |-  ( ( ( G .+ ( M ` W ) ) e. B /\ G e. B ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( ( G .+ ( M ` W ) ) .+ ( ( invg ` S ) ` G ) ) )
40 37 34 39 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( ( G .+ ( M ` W ) ) .+ ( ( invg ` S ) ` G ) ) )
41 1 5 38 symginv 
 |-  ( G e. B -> ( ( invg ` S ) ` G ) = `' G )
42 41 3ad2ant2 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( invg ` S ) ` G ) = `' G )
43 42 oveq2d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .+ ( ( invg ` S ) ` G ) ) = ( ( G .+ ( M ` W ) ) .+ `' G ) )
44 simp1 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> D e. V )
45 f1ocnv 
 |-  ( G : D -1-1-onto-> D -> `' G : D -1-1-onto-> D )
46 7 45 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> `' G : D -1-1-onto-> D )
47 1 5 elsymgbas 
 |-  ( D e. V -> ( `' G e. B <-> `' G : D -1-1-onto-> D ) )
48 47 biimpar 
 |-  ( ( D e. V /\ `' G : D -1-1-onto-> D ) -> `' G e. B )
49 44 46 48 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> `' G e. B )
50 1 5 3 symgov 
 |-  ( ( ( G .+ ( M ` W ) ) e. B /\ `' G e. B ) -> ( ( G .+ ( M ` W ) ) .+ `' G ) = ( ( G .+ ( M ` W ) ) o. `' G ) )
51 37 49 50 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .+ `' G ) = ( ( G .+ ( M ` W ) ) o. `' G ) )
52 40 43 51 3eqtrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( ( G .+ ( M ` W ) ) o. `' G ) )
53 1 5 3 symgov 
 |-  ( ( G e. B /\ ( M ` W ) e. B ) -> ( G .+ ( M ` W ) ) = ( G o. ( M ` W ) ) )
54 34 35 53 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G .+ ( M ` W ) ) = ( G o. ( M ` W ) ) )
55 18 simpld 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> W e. Word D )
56 2 44 55 19 tocycfv 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( M ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
57 56 coeq2d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. ( M ` W ) ) = ( G o. ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ) )
58 coundi 
 |-  ( G o. ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ) = ( ( G o. ( _I |` ( D \ ran W ) ) ) u. ( G o. ( ( W cyclShift 1 ) o. `' W ) ) )
59 58 a1i 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ) = ( ( G o. ( _I |` ( D \ ran W ) ) ) u. ( G o. ( ( W cyclShift 1 ) o. `' W ) ) ) )
60 54 57 59 3eqtrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G .+ ( M ` W ) ) = ( ( G o. ( _I |` ( D \ ran W ) ) ) u. ( G o. ( ( W cyclShift 1 ) o. `' W ) ) ) )
61 coires1 
 |-  ( G o. ( _I |` ( D \ ran W ) ) ) = ( G |` ( D \ ran W ) )
62 61 a1i 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. ( _I |` ( D \ ran W ) ) ) = ( G |` ( D \ ran W ) ) )
63 coass 
 |-  ( ( G o. ( W cyclShift 1 ) ) o. `' W ) = ( G o. ( ( W cyclShift 1 ) o. `' W ) )
64 1zzd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> 1 e. ZZ )
65 f1of 
 |-  ( G : D -1-1-onto-> D -> G : D --> D )
66 7 65 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> G : D --> D )
67 cshco 
 |-  ( ( W e. Word D /\ 1 e. ZZ /\ G : D --> D ) -> ( G o. ( W cyclShift 1 ) ) = ( ( G o. W ) cyclShift 1 ) )
68 55 64 66 67 syl3anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. ( W cyclShift 1 ) ) = ( ( G o. W ) cyclShift 1 ) )
69 68 coeq1d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G o. ( W cyclShift 1 ) ) o. `' W ) = ( ( ( G o. W ) cyclShift 1 ) o. `' W ) )
70 63 69 eqtr3id 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. ( ( W cyclShift 1 ) o. `' W ) ) = ( ( ( G o. W ) cyclShift 1 ) o. `' W ) )
71 62 70 uneq12d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G o. ( _I |` ( D \ ran W ) ) ) u. ( G o. ( ( W cyclShift 1 ) o. `' W ) ) ) = ( ( G |` ( D \ ran W ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' W ) ) )
72 60 71 eqtrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G .+ ( M ` W ) ) = ( ( G |` ( D \ ran W ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' W ) ) )
73 72 coeq1d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) o. `' G ) = ( ( ( G |` ( D \ ran W ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' W ) ) o. `' G ) )
74 52 73 eqtrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( ( ( G |` ( D \ ran W ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' W ) ) o. `' G ) )
75 coundir 
 |-  ( ( ( G |` ( D \ ran W ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' W ) ) o. `' G ) = ( ( ( G |` ( D \ ran W ) ) o. `' G ) u. ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) )
76 74 75 eqtrdi 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( ( ( G |` ( D \ ran W ) ) o. `' G ) u. ( ( ( ( G o. W ) cyclShift 1 ) o. `' W ) o. `' G ) ) )
77 wrdco 
 |-  ( ( W e. Word D /\ G : D --> D ) -> ( G o. W ) e. Word D )
78 55 66 77 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. W ) e. Word D )
79 f1of1 
 |-  ( G : D -1-1-onto-> D -> G : D -1-1-> D )
80 7 79 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> G : D -1-1-> D )
81 f1co 
 |-  ( ( G : D -1-1-> D /\ W : dom W -1-1-> D ) -> ( G o. W ) : dom W -1-1-> D )
82 80 19 81 syl2anc 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. W ) : dom W -1-1-> D )
83 66 fdmd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> dom G = D )
84 22 83 sseqtrrd 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ran W C_ dom G )
85 dmcosseq 
 |-  ( ran W C_ dom G -> dom ( G o. W ) = dom W )
86 84 85 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> dom ( G o. W ) = dom W )
87 f1eq2 
 |-  ( dom ( G o. W ) = dom W -> ( ( G o. W ) : dom ( G o. W ) -1-1-> D <-> ( G o. W ) : dom W -1-1-> D ) )
88 86 87 syl 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G o. W ) : dom ( G o. W ) -1-1-> D <-> ( G o. W ) : dom W -1-1-> D ) )
89 82 88 mpbird 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( G o. W ) : dom ( G o. W ) -1-1-> D )
90 2 44 78 89 tocycfv 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( M ` ( G o. W ) ) = ( ( _I |` ( D \ ran ( G o. W ) ) ) u. ( ( ( G o. W ) cyclShift 1 ) o. `' ( G o. W ) ) ) )
91 33 76 90 3eqtr4d 
 |-  ( ( D e. V /\ G e. B /\ W e. dom M ) -> ( ( G .+ ( M ` W ) ) .- G ) = ( M ` ( G o. W ) ) )