Metamath Proof Explorer

Theorem cyc3fv1

Description: Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses cycpm3.c 
|- C = ( toCyc ` D )
cycpm3.s 
|- S = ( SymGrp ` D )
cycpm3.d 
|- ( ph -> D e. V )
cycpm3.i 
|- ( ph -> I e. D )
cycpm3.j 
|- ( ph -> J e. D )
cycpm3.k 
|- ( ph -> K e. D )
cycpm3.1 
|- ( ph -> I =/= J )
cycpm3.2 
|- ( ph -> J =/= K )
cycpm3.3 
|- ( ph -> K =/= I )
Assertion cyc3fv1 
|- ( ph -> ( ( C ` <" I J K "> ) ` I ) = J )

Proof

Step Hyp Ref Expression
1 cycpm3.c 
 |-  C = ( toCyc ` D )
2 cycpm3.s 
 |-  S = ( SymGrp ` D )
3 cycpm3.d 
 |-  ( ph -> D e. V )
4 cycpm3.i 
 |-  ( ph -> I e. D )
5 cycpm3.j 
 |-  ( ph -> J e. D )
6 cycpm3.k 
 |-  ( ph -> K e. D )
7 cycpm3.1 
 |-  ( ph -> I =/= J )
8 cycpm3.2 
 |-  ( ph -> J =/= K )
9 cycpm3.3 
 |-  ( ph -> K =/= I )
10 4 5 6 s3cld 
 |-  ( ph -> <" I J K "> e. Word D )
11 4 5 6 7 8 9 s3f1 
 |-  ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D )
12 c0ex 
 |-  0 e. _V
13 12 prid1 
 |-  0 e. { 0 , 1 }
14 s3len 
 |-  ( # ` <" I J K "> ) = 3
15 14 oveq1i 
 |-  ( ( # ` <" I J K "> ) - 1 ) = ( 3 - 1 )
16 3m1e2 
 |-  ( 3 - 1 ) = 2
17 15 16 eqtri 
 |-  ( ( # ` <" I J K "> ) - 1 ) = 2
18 17 oveq2i 
 |-  ( 0 ..^ ( ( # ` <" I J K "> ) - 1 ) ) = ( 0 ..^ 2 )
19 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
20 18 19 eqtri 
 |-  ( 0 ..^ ( ( # ` <" I J K "> ) - 1 ) ) = { 0 , 1 }
21 13 20 eleqtrri 
 |-  0 e. ( 0 ..^ ( ( # ` <" I J K "> ) - 1 ) )
22 21 a1i 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` <" I J K "> ) - 1 ) ) )
23 1 3 10 11 22 cycpmfv1 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` ( <" I J K "> ` 0 ) ) = ( <" I J K "> ` ( 0 + 1 ) ) )
24 s3fv0 
 |-  ( I e. D -> ( <" I J K "> ` 0 ) = I )
25 4 24 syl 
 |-  ( ph -> ( <" I J K "> ` 0 ) = I )
26 25 fveq2d 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` ( <" I J K "> ` 0 ) ) = ( ( C ` <" I J K "> ) ` I ) )
27 0p1e1 
 |-  ( 0 + 1 ) = 1
28 27 fveq2i 
 |-  ( <" I J K "> ` ( 0 + 1 ) ) = ( <" I J K "> ` 1 )
29 s3fv1 
 |-  ( J e. D -> ( <" I J K "> ` 1 ) = J )
30 5 29 syl 
 |-  ( ph -> ( <" I J K "> ` 1 ) = J )
31 28 30 syl5eq 
 |-  ( ph -> ( <" I J K "> ` ( 0 + 1 ) ) = J )
32 23 26 31 3eqtr3d 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` I ) = J )