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 " ( `' # " { P } ) )
cycpmconjs.s 
|- S = ( SymGrp ` D )
cycpmconjs.n 
|- N = ( # ` D )
cycpmconjs.m 
|- M = ( toCyc ` D )
cycpmgcl.b 
|- B = ( Base ` S )
Assertion cycpmgcl 
|- ( ( D e. V /\ P e. ( 0 ... N ) ) -> C C_ B )

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 cycpmgcl.b 
 |-  B = ( Base ` S )
6 simpr 
 |-  ( ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = p ) -> ( M ` u ) = p )
7 simplll 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> D e. V )
8 simpr 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) )
9 8 elin1d 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> u e. { w e. Word D | w : dom w -1-1-> D } )
10 elrabi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u e. Word D )
11 9 10 syl 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> u e. 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 e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
17 16 simprbi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u : dom u -1-1-> D )
18 9 17 syl 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> u : dom u -1-1-> D )
19 4 7 11 18 2 cycpmcl 
 |-  ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) -> ( M ` u ) e. ( Base ` S ) )
20 19 adantr 
 |-  ( ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = p ) -> ( M ` u ) e. ( Base ` S ) )
21 20 5 eleqtrrdi 
 |-  ( ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = p ) -> ( M ` u ) e. B )
22 6 21 eqeltrrd 
 |-  ( ( ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ) /\ ( M ` u ) = p ) -> p e. B )
23 nfcv 
 |-  F/_ u M
24 simpl 
 |-  ( ( D e. V /\ P e. ( 0 ... N ) ) -> D e. V )
25 4 2 5 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> B )
26 ffn 
 |-  ( M : { w e. Word D | w : dom w -1-1-> D } --> B -> M Fn { w e. Word D | w : dom w -1-1-> D } )
27 24 25 26 3syl 
 |-  ( ( D e. V /\ P e. ( 0 ... N ) ) -> M Fn { w e. Word D | w : dom w -1-1-> D } )
28 27 adantr 
 |-  ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) -> M Fn { w e. Word D | w : dom w -1-1-> D } )
29 1 eleq2i 
 |-  ( p e. C <-> p e. ( M " ( `' # " { P } ) ) )
30 29 a1i 
 |-  ( ( D e. V /\ P e. ( 0 ... N ) ) -> ( p e. C <-> p e. ( M " ( `' # " { P } ) ) ) )
31 30 biimpa 
 |-  ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) -> p e. ( M " ( `' # " { P } ) ) )
32 23 28 31 fvelimad 
 |-  ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { P } ) ) ( M ` u ) = p )
33 22 32 r19.29a 
 |-  ( ( ( D e. V /\ P e. ( 0 ... N ) ) /\ p e. C ) -> p e. B )
34 33 ex 
 |-  ( ( D e. V /\ P e. ( 0 ... N ) ) -> ( p e. C -> p e. B ) )
35 34 ssrdv 
 |-  ( ( D e. V /\ P e. ( 0 ... N ) ) -> C C_ B )