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

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		3pos	⊢ 0 < 3
13		s3len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
14	12 13	breqtrri	⊢ 0 < ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ )
15	14	a1i	⊢ ( 𝜑 → 0 < ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) )
16	13	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) = ( 3 − 1 )
17		3m1e2	⊢ ( 3 − 1 ) = 2
18	16 17	eqtr2i	⊢ 2 = ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 )
19	18	a1i	⊢ ( 𝜑 → 2 = ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) )
20	1 3 10 11 15 19	cycpmfv2	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) )
21		s3fv2	⊢ ( 𝐾 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
22	6 21	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
23	22	fveq2d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐾 ) )
24		s3fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
25	4 24	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
26	20 23 25	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐾 ) = 𝐼 )