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		c0ex	⊢ 0 ∈ V
13	12	prid1	⊢ 0 ∈ { 0 , 1 }
14		s3len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
15	14	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) = ( 3 − 1 )
16		3m1e2	⊢ ( 3 − 1 ) = 2
17	15 16	eqtri	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) = 2
18	17	oveq2i	⊢ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) = ( 0 ..^ 2 )
19		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
20	18 19	eqtri	⊢ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) = { 0 , 1 }
21	13 20	eleqtrri	⊢ 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) )
22	21	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) )
23	1 3 10 11 22	cycpmfv1	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) )
24		s3fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
25	4 24	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
26	25	fveq2d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐼 ) )
27		0p1e1	⊢ ( 0 + 1 ) = 1
28	27	fveq2i	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 )
29		s3fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
30	5 29	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
31	28 30	syl5eq	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 0 + 1 ) ) = 𝐽 )
32	23 26 31	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐼 ) = 𝐽 )