Metamath Proof Explorer

Theorem tocycfv

Description: Function value of a permutation cycle built from a word. (Contributed by Thierry Arnoux, 18-Sep-2023)

Ref Expression
Hypotheses tocycval.1 
|- C = ( toCyc ` D )
tocycfv.d 
|- ( ph -> D e. V )
tocycfv.w 
|- ( ph -> W e. Word D )
tocycfv.1 
|- ( ph -> W : dom W -1-1-> D )
Assertion tocycfv 
|- ( ph -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 
 |-  C = ( toCyc ` D )
2 tocycfv.d 
 |-  ( ph -> D e. V )
3 tocycfv.w 
 |-  ( ph -> W e. Word D )
4 tocycfv.1 
 |-  ( ph -> W : dom W -1-1-> D )
5 1 tocycval 
 |-  ( D e. V -> C = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
6 2 5 syl 
 |-  ( ph -> C = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
7 simpr 
 |-  ( ( ph /\ w = W ) -> w = W )
8 7 rneqd 
 |-  ( ( ph /\ w = W ) -> ran w = ran W )
9 8 difeq2d 
 |-  ( ( ph /\ w = W ) -> ( D \ ran w ) = ( D \ ran W ) )
10 9 reseq2d 
 |-  ( ( ph /\ w = W ) -> ( _I |` ( D \ ran w ) ) = ( _I |` ( D \ ran W ) ) )
11 7 oveq1d 
 |-  ( ( ph /\ w = W ) -> ( w cyclShift 1 ) = ( W cyclShift 1 ) )
12 7 cnveqd 
 |-  ( ( ph /\ w = W ) -> `' w = `' W )
13 11 12 coeq12d 
 |-  ( ( ph /\ w = W ) -> ( ( w cyclShift 1 ) o. `' w ) = ( ( W cyclShift 1 ) o. `' W ) )
14 10 13 uneq12d 
 |-  ( ( ph /\ w = W ) -> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
15 id 
 |-  ( u = W -> u = W )
16 dmeq 
 |-  ( u = W -> dom u = dom W )
17 eqidd 
 |-  ( u = W -> D = D )
18 15 16 17 f1eq123d 
 |-  ( u = W -> ( u : dom u -1-1-> D <-> W : dom W -1-1-> D ) )
19 18 3 4 elrabd 
 |-  ( ph -> W e. { u e. Word D | u : dom u -1-1-> D } )
20 2 difexd 
 |-  ( ph -> ( D \ ran W ) e. _V )
21 20 resiexd 
 |-  ( ph -> ( _I |` ( D \ ran W ) ) e. _V )
22 cshwcl 
 |-  ( W e. Word D -> ( W cyclShift 1 ) e. Word D )
23 3 22 syl 
 |-  ( ph -> ( W cyclShift 1 ) e. Word D )
24 cnvexg 
 |-  ( W e. Word D -> `' W e. _V )
25 3 24 syl 
 |-  ( ph -> `' W e. _V )
26 coexg 
 |-  ( ( ( W cyclShift 1 ) e. Word D /\ `' W e. _V ) -> ( ( W cyclShift 1 ) o. `' W ) e. _V )
27 23 25 26 syl2anc 
 |-  ( ph -> ( ( W cyclShift 1 ) o. `' W ) e. _V )
28 unexg 
 |-  ( ( ( _I |` ( D \ ran W ) ) e. _V /\ ( ( W cyclShift 1 ) o. `' W ) e. _V ) -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) e. _V )
29 21 27 28 syl2anc 
 |-  ( ph -> ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) e. _V )
30 6 14 19 29 fvmptd 
 |-  ( ph -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )