Theorem cyc2fv2

Description: Function value of a 2-cycle at the second 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	cyc2fv2	|- ( ph -> ( ( C ` <" I J "> ) ` J ) = I )

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		2pos	|- 0 < 2
10		s2len	|- ( # ` <" I J "> ) = 2
11	9 10	breqtrri	|- 0 < ( # ` <" I J "> )
12	11	a1i	|- ( ph -> 0 < ( # ` <" I J "> ) )
13	10	oveq1i	|- ( ( # ` <" I J "> ) - 1 ) = ( 2 - 1 )
14		2m1e1	|- ( 2 - 1 ) = 1
15	13 14	eqtr2i	|- 1 = ( ( # ` <" I J "> ) - 1 )
16	15	a1i	|- ( ph -> 1 = ( ( # ` <" I J "> ) - 1 ) )
17	1 2 7 8 12 16	cycpmfv2	|- ( ph -> ( ( C ` <" I J "> ) ` ( <" I J "> ` 1 ) ) = ( <" I J "> ` 0 ) )
18		s2fv1	|- ( J e. D -> ( <" I J "> ` 1 ) = J )
19	4 18	syl	|- ( ph -> ( <" I J "> ` 1 ) = J )
20	19	fveq2d	|- ( ph -> ( ( C ` <" I J "> ) ` ( <" I J "> ` 1 ) ) = ( ( C ` <" I J "> ) ` J ) )
21		s2fv0	|- ( I e. D -> ( <" I J "> ` 0 ) = I )
22	3 21	syl	|- ( ph -> ( <" I J "> ` 0 ) = I )
23	17 20 22	3eqtr3d	|- ( ph -> ( ( C ` <" I J "> ) ` J ) = I )