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 | |
|
cycpmconjs.s | |
||
cycpmconjs.n | |
||
cycpmconjs.m | |
||
cycpmgcl.b | |
||
Assertion | cycpmgcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cycpmconjs.c | |
|
2 | cycpmconjs.s | |
|
3 | cycpmconjs.n | |
|
4 | cycpmconjs.m | |
|
5 | cycpmgcl.b | |
|
6 | simpr | |
|
7 | simplll | |
|
8 | simpr | |
|
9 | 8 | elin1d | |
10 | elrabi | |
|
11 | 9 10 | syl | |
12 | id | |
|
13 | dmeq | |
|
14 | eqidd | |
|
15 | 12 13 14 | f1eq123d | |
16 | 15 | elrab | |
17 | 16 | simprbi | |
18 | 9 17 | syl | |
19 | 4 7 11 18 2 | cycpmcl | |
20 | 19 | adantr | |
21 | 20 5 | eleqtrrdi | |
22 | 6 21 | eqeltrrd | |
23 | nfcv | |
|
24 | simpl | |
|
25 | 4 2 5 | tocycf | |
26 | ffn | |
|
27 | 24 25 26 | 3syl | |
28 | 27 | adantr | |
29 | 1 | eleq2i | |
30 | 29 | a1i | |
31 | 30 | biimpa | |
32 | 23 28 31 | fvelimad | |
33 | 22 32 | r19.29a | |
34 | 33 | ex | |
35 | 34 | ssrdv | |