Theorem cyc2fv2

Description: Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	cycpm2.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
	cycpm2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpm2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	cycpm2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	cycpm2.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
	cycpm2cl.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
Assertion	cyc2fv2	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		cycpm2.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2		cycpm2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		cycpm2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
4		cycpm2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
5		cycpm2.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
6		cycpm2cl.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
7	3 4	s2cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
8	3 4 5	s2f1	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
9		2pos	⊢ 0 < 2
10		s2len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = 2
11	9 10	breqtrri	⊢ 0 < ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ )
12	11	a1i	⊢ ( 𝜑 → 0 < ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) )
13	10	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) = ( 2 − 1 )
14		2m1e1	⊢ ( 2 − 1 ) = 1
15	13 14	eqtr2i	⊢ 1 = ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 )
16	15	a1i	⊢ ( 𝜑 → 1 = ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) )
17	1 2 7 8 12 16	cycpmfv2	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) ) = ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) )
18		s2fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
19	4 18	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
20	19	fveq2d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) )
21		s2fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
22	3 21	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
23	17 20 22	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) = 𝐼 )