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	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
	cycpm3.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	cycpm3.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpm3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	cycpm3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	cycpm3.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
	cycpm3.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
	cycpm3.2	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
	cycpm3.3	⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
Assertion	cyc3fv1	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐼 ) = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2		cycpm3.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3		cycpm3.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		cycpm3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
5		cycpm3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
6		cycpm3.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
7		cycpm3.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
8		cycpm3.2	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
9		cycpm3.3	⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
10	4 5 6	s3cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 )
11	4 5 6 7 8 9	s3f1	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 )
12		0elpr01	⊢ 0 ∈ { 0 , 1 }
13		s3len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
14	13	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) = ( 3 − 1 )
15		3m1e2	⊢ ( 3 − 1 ) = 2
16	14 15	eqtri	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) = 2
17	16	oveq2i	⊢ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) = ( 0 ..^ 2 )
18		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
19	17 18	eqtri	⊢ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) = { 0 , 1 }
20	12 19	eleqtrri	⊢ 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) )
21	20	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) )
22	1 3 10 11 21	cycpmfv1	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) )
23		s3fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
24	4 23	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
25	24	fveq2d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐼 ) )
26		0p1e1	⊢ ( 0 + 1 ) = 1
27	26	fveq2i	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 )
28		s3fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
29	5 28	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
30	27 29	eqtrid	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) = 𝐽 )
31	22 25 30	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐼 ) = 𝐽 )