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=\mathrm{toCyc}\left(D\right)$$
	cycpm3.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
	cycpm3.d	$$⊢\phi \to D\in V$$
	cycpm3.i	$$⊢\phi \to I\in D$$
	cycpm3.j	$$⊢\phi \to J\in D$$
	cycpm3.k	$$⊢\phi \to K\in D$$
	cycpm3.1	$$⊢\phi \to I\ne J$$
	cycpm3.2	$$⊢\phi \to J\ne K$$
	cycpm3.3	$$⊢\phi \to K\ne I$$
Assertion	cyc3fv1	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\left(I\right)=J$$

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
2		cycpm3.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
3		cycpm3.d	$$⊢\phi \to D\in V$$
4		cycpm3.i	$$⊢\phi \to I\in D$$
5		cycpm3.j	$$⊢\phi \to J\in D$$
6		cycpm3.k	$$⊢\phi \to K\in D$$
7		cycpm3.1	$$⊢\phi \to I\ne J$$
8		cycpm3.2	$$⊢\phi \to J\ne K$$
9		cycpm3.3	$$⊢\phi \to K\ne I$$
10	4 5 6	s3cld	$$⊢\phi \to ⟨“IJK”⟩\in \mathrm{Word}D$$
11	4 5 6 7 8 9	s3f1	$$⊢\phi \to ⟨“IJK”⟩:\mathrm{dom}⟨“IJK”⟩\underset{1-1}{⟶}D$$
12		c0ex	$$⊢0\in \mathrm{V}$$
13	12	prid1	$$⊢0\in \left\{0,1\right\}$$
14		s3len	$$⊢\left|⟨“IJK”⟩\right|=3$$
15	14	oveq1i	$$⊢\left|⟨“IJK”⟩\right|-1=3-1$$
16		3m1e2	$$⊢3-1=2$$
17	15 16	eqtri	$$⊢\left|⟨“IJK”⟩\right|-1=2$$
18	17	oveq2i	$$⊢\left(0..^\left|⟨“IJK”⟩\right|-1\right)=\left(0..^2\right)$$
19		fzo0to2pr	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$
20	18 19	eqtri	$$⊢\left(0..^\left|⟨“IJK”⟩\right|-1\right)=\left\{0,1\right\}$$
21	13 20	eleqtrri	$$⊢0\in \left(0..^\left|⟨“IJK”⟩\right|-1\right)$$
22	21	a1i	$$⊢\phi \to 0\in \left(0..^\left|⟨“IJK”⟩\right|-1\right)$$
23	1 3 10 11 22	cycpmfv1	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\left(⟨“IJK”⟩\left(0\right)\right)=⟨“IJK”⟩\left(0+1\right)$$
24		s3fv0	$$⊢I\in D\to ⟨“IJK”⟩\left(0\right)=I$$
25	4 24	syl	$$⊢\phi \to ⟨“IJK”⟩\left(0\right)=I$$
26	25	fveq2d	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\left(⟨“IJK”⟩\left(0\right)\right)=C\left(⟨“IJK”⟩\right)\left(I\right)$$
27		0p1e1	$$⊢0+1=1$$
28	27	fveq2i	$$⊢⟨“IJK”⟩\left(0+1\right)=⟨“IJK”⟩\left(1\right)$$
29		s3fv1	$$⊢J\in D\to ⟨“IJK”⟩\left(1\right)=J$$
30	5 29	syl	$$⊢\phi \to ⟨“IJK”⟩\left(1\right)=J$$
31	28 30	eqtrid	$$⊢\phi \to ⟨“IJK”⟩\left(0+1\right)=J$$
32	23 26 31	3eqtr3d	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\left(I\right)=J$$