Metamath Proof Explorer

Theorem cyc2fv1

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

Ref Expression
Hypotheses cycpm2.c 
|- C = ( toCyc ` D )
cycpm2.d 
|- ( ph -> D e. V )
cycpm2.i 
|- ( ph -> I e. D )
cycpm2.j 
|- ( ph -> J e. D )
cycpm2.1 
|- ( ph -> I =/= J )
cycpm2cl.s 
|- S = ( SymGrp ` D )
Assertion cyc2fv1 
|- ( ph -> ( ( C ` <" I J "> ) ` I ) = J )

Proof

Step Hyp Ref Expression
1 cycpm2.c 
 |-  C = ( toCyc ` D )
2 cycpm2.d 
 |-  ( ph -> D e. V )
3 cycpm2.i 
 |-  ( ph -> I e. D )
4 cycpm2.j 
 |-  ( ph -> J e. D )
5 cycpm2.1 
 |-  ( ph -> I =/= J )
6 cycpm2cl.s 
 |-  S = ( SymGrp ` D )
7 3 4 s2cld 
 |-  ( ph -> <" I J "> e. Word D )
8 3 4 5 s2f1 
 |-  ( ph -> <" I J "> : dom <" I J "> -1-1-> D )
9 c0ex 
 |-  0 e. _V
10 9 snid 
 |-  0 e. { 0 }
11 s2len 
 |-  ( # ` <" I J "> ) = 2
12 11 oveq1i 
 |-  ( ( # ` <" I J "> ) - 1 ) = ( 2 - 1 )
13 2m1e1 
 |-  ( 2 - 1 ) = 1
14 12 13 eqtr2i 
 |-  1 = ( ( # ` <" I J "> ) - 1 )
15 14 oveq2i 
 |-  ( 0 ..^ 1 ) = ( 0 ..^ ( ( # ` <" I J "> ) - 1 ) )
16 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
17 15 16 eqtr3i 
 |-  ( 0 ..^ ( ( # ` <" I J "> ) - 1 ) ) = { 0 }
18 10 17 eleqtrri 
 |-  0 e. ( 0 ..^ ( ( # ` <" I J "> ) - 1 ) )
19 18 a1i 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` <" I J "> ) - 1 ) ) )
20 1 2 7 8 19 cycpmfv1 
 |-  ( ph -> ( ( C ` <" I J "> ) ` ( <" I J "> ` 0 ) ) = ( <" I J "> ` ( 0 + 1 ) ) )
21 s2fv0 
 |-  ( I e. D -> ( <" I J "> ` 0 ) = I )
22 3 21 syl 
 |-  ( ph -> ( <" I J "> ` 0 ) = I )
23 22 fveq2d 
 |-  ( ph -> ( ( C ` <" I J "> ) ` ( <" I J "> ` 0 ) ) = ( ( C ` <" I J "> ) ` I ) )
24 0p1e1 
 |-  ( 0 + 1 ) = 1
25 24 fveq2i 
 |-  ( <" I J "> ` ( 0 + 1 ) ) = ( <" I J "> ` 1 )
26 s2fv1 
 |-  ( J e. D -> ( <" I J "> ` 1 ) = J )
27 4 26 syl 
 |-  ( ph -> ( <" I J "> ` 1 ) = J )
28 25 27 syl5eq 
 |-  ( ph -> ( <" I J "> ` ( 0 + 1 ) ) = J )
29 20 23 28 3eqtr3d 
 |-  ( ph -> ( ( C ` <" I J "> ) ` I ) = J )