Metamath Proof Explorer


Theorem cycpmgcl

Description: Cyclic permutations are permutations, similar to cycpmcl , but where the set of cyclic permutations of length P is expressed in terms of a preimage. (Contributed by Thierry Arnoux, 13-Oct-2023)

Ref Expression
Hypotheses cycpmconjs.c C=M.-1P
cycpmconjs.s S=SymGrpD
cycpmconjs.n N=D
cycpmconjs.m M=toCycD
cycpmgcl.b B=BaseS
Assertion cycpmgcl DVP0NCB

Proof

Step Hyp Ref Expression
1 cycpmconjs.c C=M.-1P
2 cycpmconjs.s S=SymGrpD
3 cycpmconjs.n N=D
4 cycpmconjs.m M=toCycD
5 cycpmgcl.b B=BaseS
6 simpr DVP0NpCuwWordD|w:domw1-1D.-1PMu=pMu=p
7 simplll DVP0NpCuwWordD|w:domw1-1D.-1PDV
8 simpr DVP0NpCuwWordD|w:domw1-1D.-1PuwWordD|w:domw1-1D.-1P
9 8 elin1d DVP0NpCuwWordD|w:domw1-1D.-1PuwWordD|w:domw1-1D
10 elrabi uwWordD|w:domw1-1DuWordD
11 9 10 syl DVP0NpCuwWordD|w:domw1-1D.-1PuWordD
12 id w=uw=u
13 dmeq w=udomw=domu
14 eqidd w=uD=D
15 12 13 14 f1eq123d w=uw:domw1-1Du:domu1-1D
16 15 elrab uwWordD|w:domw1-1DuWordDu:domu1-1D
17 16 simprbi uwWordD|w:domw1-1Du:domu1-1D
18 9 17 syl DVP0NpCuwWordD|w:domw1-1D.-1Pu:domu1-1D
19 4 7 11 18 2 cycpmcl DVP0NpCuwWordD|w:domw1-1D.-1PMuBaseS
20 19 adantr DVP0NpCuwWordD|w:domw1-1D.-1PMu=pMuBaseS
21 20 5 eleqtrrdi DVP0NpCuwWordD|w:domw1-1D.-1PMu=pMuB
22 6 21 eqeltrrd DVP0NpCuwWordD|w:domw1-1D.-1PMu=ppB
23 nfcv _uM
24 simpl DVP0NDV
25 4 2 5 tocycf DVM:wWordD|w:domw1-1DB
26 ffn M:wWordD|w:domw1-1DBMFnwWordD|w:domw1-1D
27 24 25 26 3syl DVP0NMFnwWordD|w:domw1-1D
28 27 adantr DVP0NpCMFnwWordD|w:domw1-1D
29 1 eleq2i pCpM.-1P
30 29 a1i DVP0NpCpM.-1P
31 30 biimpa DVP0NpCpM.-1P
32 23 28 31 fvelimad DVP0NpCuwWordD|w:domw1-1D.-1PMu=p
33 22 32 r19.29a DVP0NpCpB
34 33 ex DVP0NpCpB
35 34 ssrdv DVP0NCB