Theorem cyc2fv1

Description: Function value of a 2-cycle at the first 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	cyc2fv1	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) = 𝐽 )

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		c0ex	⊢ 0 ∈ V
10	9	snid	⊢ 0 ∈ { 0 }
11		s2len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = 2
12	11	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) = ( 2 − 1 )
13		2m1e1	⊢ ( 2 − 1 ) = 1
14	12 13	eqtr2i	⊢ 1 = ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 )
15	14	oveq2i	⊢ ( 0 ..^ 1 ) = ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) )
16		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
17	15 16	eqtr3i	⊢ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) ) = { 0 }
18	10 17	eleqtrri	⊢ 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) )
19	18	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) − 1 ) ) )
20	1 2 7 8 19	cycpmfv1	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) ) = ( ⟨“ 𝐼 𝐽 ”⟩ ‘ ( 0 + 1 ) ) )
21		s2fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
22	3 21	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
23	22	fveq2d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) )
24		0p1e1	⊢ ( 0 + 1 ) = 1
25	24	fveq2i	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ ‘ ( 0 + 1 ) ) = ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 )
26		s2fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
27	4 26	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
28	25 27	syl5eq	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ ( 0 + 1 ) ) = 𝐽 )
29	20 23 28	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) = 𝐽 )