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 . -1 P
cycpmconjs.s S = SymGrp D
cycpmconjs.n N = D
cycpmconjs.m M = toCyc D
cycpmgcl.b B = Base S
Assertion cycpmgcl D V P 0 N C B

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 cycpmgcl.b B = Base S
6 simpr D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u = p M u = p
7 simplll D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P D V
8 simpr D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P u w Word D | w : dom w 1-1 D . -1 P
9 8 elin1d D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P u w Word D | w : dom w 1-1 D
10 elrabi u w Word D | w : dom w 1-1 D u Word D
11 9 10 syl D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P u Word D
12 id w = u w = u
13 dmeq w = u dom w = dom u
14 eqidd w = u D = D
15 12 13 14 f1eq123d w = u w : dom w 1-1 D u : dom u 1-1 D
16 15 elrab u w Word D | w : dom w 1-1 D u Word D u : dom u 1-1 D
17 16 simprbi u w Word D | w : dom w 1-1 D u : dom u 1-1 D
18 9 17 syl D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P u : dom u 1-1 D
19 4 7 11 18 2 cycpmcl D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u Base S
20 19 adantr D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u = p M u Base S
21 20 5 eleqtrrdi D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u = p M u B
22 6 21 eqeltrrd D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u = p p B
23 nfcv _ u M
24 simpl D V P 0 N D V
25 4 2 5 tocycf D V M : w Word D | w : dom w 1-1 D B
26 ffn M : w Word D | w : dom w 1-1 D B M Fn w Word D | w : dom w 1-1 D
27 24 25 26 3syl D V P 0 N M Fn w Word D | w : dom w 1-1 D
28 27 adantr D V P 0 N p C M Fn w Word D | w : dom w 1-1 D
29 1 eleq2i p C p M . -1 P
30 29 a1i D V P 0 N p C p M . -1 P
31 30 biimpa D V P 0 N p C p M . -1 P
32 23 28 31 fvelimad D V P 0 N p C u w Word D | w : dom w 1-1 D . -1 P M u = p
33 22 32 r19.29a D V P 0 N p C p B
34 33 ex D V P 0 N p C p B
35 34 ssrdv D V P 0 N C B