Metamath Proof Explorer

Theorem tocycf

Description: The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023)

Ref Expression
Hypotheses tocycf.c 
|- C = ( toCyc ` D )
tocycf.s 
|- S = ( SymGrp ` D )
tocycf.b 
|- B = ( Base ` S )
Assertion tocycf 
|- ( D e. V -> C : { w e. Word D | w : dom w -1-1-> D } --> B )

Proof

Step Hyp Ref Expression
1 tocycf.c 
 |-  C = ( toCyc ` D )
2 tocycf.s 
 |-  S = ( SymGrp ` D )
3 tocycf.b 
 |-  B = ( Base ` S )
4 1 tocycval 
 |-  ( D e. V -> C = ( u e. { w e. Word D | w : dom w -1-1-> D } |-> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) ) )
5 simpr 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> u = (/) )
6 5 rneqd 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ran u = ran (/) )
7 rn0 
 |-  ran (/) = (/)
8 6 7 eqtrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ran u = (/) )
9 8 difeq2d 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( D \ ran u ) = ( D \ (/) ) )
10 dif0 
 |-  ( D \ (/) ) = D
11 9 10 eqtrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( D \ ran u ) = D )
12 11 reseq2d 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( _I |` ( D \ ran u ) ) = ( _I |` D ) )
13 5 cnveqd 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> `' u = `' (/) )
14 cnv0 
 |-  `' (/) = (/)
15 13 14 eqtrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> `' u = (/) )
16 15 coeq2d 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( ( u cyclShift 1 ) o. `' u ) = ( ( u cyclShift 1 ) o. (/) ) )
17 co02 
 |-  ( ( u cyclShift 1 ) o. (/) ) = (/)
18 16 17 eqtrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( ( u cyclShift 1 ) o. `' u ) = (/) )
19 12 18 uneq12d 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) = ( ( _I |` D ) u. (/) ) )
20 un0 
 |-  ( ( _I |` D ) u. (/) ) = ( _I |` D )
21 19 20 eqtrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) = ( _I |` D ) )
22 2 idresperm 
 |-  ( D e. V -> ( _I |` D ) e. ( Base ` S ) )
23 22 3 eleqtrrdi 
 |-  ( D e. V -> ( _I |` D ) e. B )
24 23 ad2antrr 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( _I |` D ) e. B )
25 21 24 eqeltrd 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u = (/) ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. B )
26 difexg 
 |-  ( D e. V -> ( D \ ran u ) e. _V )
27 26 resiexd 
 |-  ( D e. V -> ( _I |` ( D \ ran u ) ) e. _V )
28 ovex 
 |-  ( u cyclShift 1 ) e. _V
29 vex 
 |-  u e. _V
30 29 cnvex 
 |-  `' u e. _V
31 28 30 coex 
 |-  ( ( u cyclShift 1 ) o. `' u ) e. _V
32 unexg 
 |-  ( ( ( _I |` ( D \ ran u ) ) e. _V /\ ( ( u cyclShift 1 ) o. `' u ) e. _V ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. _V )
33 27 31 32 sylancl 
 |-  ( D e. V -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. _V )
34 33 adantr 
 |-  ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. _V )
35 4 34 fvmpt2d 
 |-  ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) -> ( C ` u ) = ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) )
36 35 adantr 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> ( C ` u ) = ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) )
37 simpll 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> D e. V )
38 simplr 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> u e. { w e. Word D | w : dom w -1-1-> D } )
39 id 
 |-  ( w = u -> w = u )
40 dmeq 
 |-  ( w = u -> dom w = dom u )
41 eqidd 
 |-  ( w = u -> D = D )
42 39 40 41 f1eq123d 
 |-  ( w = u -> ( w : dom w -1-1-> D <-> u : dom u -1-1-> D ) )
43 42 elrab 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
44 38 43 sylib 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> ( u e. Word D /\ u : dom u -1-1-> D ) )
45 44 simpld 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> u e. Word D )
46 44 simprd 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> u : dom u -1-1-> D )
47 1 37 45 46 2 cycpmcl 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> ( C ` u ) e. ( Base ` S ) )
48 47 3 eleqtrrdi 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> ( C ` u ) e. B )
49 36 48 eqeltrrd 
 |-  ( ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) /\ u =/= (/) ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. B )
50 25 49 pm2.61dane 
 |-  ( ( D e. V /\ u e. { w e. Word D | w : dom w -1-1-> D } ) -> ( ( _I |` ( D \ ran u ) ) u. ( ( u cyclShift 1 ) o. `' u ) ) e. B )
51 4 50 fmpt3d 
 |-  ( D e. V -> C : { w e. Word D | w : dom w -1-1-> D } --> B )