Theorem cyc3fv3

Description: Function value of a 3-cycle at the third 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	cyc3fv3	|- ( ph -> ( ( C ` <" I J K "> ) ` K ) = I )

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		3pos	|- 0 < 3
13		s3len	|- ( # ` <" I J K "> ) = 3
14	12 13	breqtrri	|- 0 < ( # ` <" I J K "> )
15	14	a1i	|- ( ph -> 0 < ( # ` <" I J K "> ) )
16	13	oveq1i	|- ( ( # ` <" I J K "> ) - 1 ) = ( 3 - 1 )
17		3m1e2	|- ( 3 - 1 ) = 2
18	16 17	eqtr2i	|- 2 = ( ( # ` <" I J K "> ) - 1 )
19	18	a1i	|- ( ph -> 2 = ( ( # ` <" I J K "> ) - 1 ) )
20	1 3 10 11 15 19	cycpmfv2	|- ( ph -> ( ( C ` <" I J K "> ) ` ( <" I J K "> ` 2 ) ) = ( <" I J K "> ` 0 ) )
21		s3fv2	|- ( K e. D -> ( <" I J K "> ` 2 ) = K )
22	6 21	syl	|- ( ph -> ( <" I J K "> ` 2 ) = K )
23	22	fveq2d	|- ( ph -> ( ( C ` <" I J K "> ) ` ( <" I J K "> ` 2 ) ) = ( ( C ` <" I J K "> ) ` K ) )
24		s3fv0	|- ( I e. D -> ( <" I J K "> ` 0 ) = I )
25	4 24	syl	|- ( ph -> ( <" I J K "> ` 0 ) = I )
26	20 23 25	3eqtr3d	|- ( ph -> ( ( C ` <" I J K "> ) ` K ) = I )