Metamath Proof Explorer


Theorem cyc3fv2

Description: Function value of a 3-cycle at the second 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 cyc3fv2 ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐽 ) = 𝐾 )

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 1ex 1 ∈ V
13 12 prid2 1 ∈ { 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 1 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) )
22 21 a1i ( 𝜑 → 1 ∈ ( 0 ..^ ( ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) − 1 ) ) )
23 1 3 10 11 22 cycpmfv1 ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 1 + 1 ) ) )
24 s3fv1 ( 𝐽𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
25 5 24 syl ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
26 25 fveq2d ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) ) = ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐽 ) )
27 1p1e2 ( 1 + 1 ) = 2
28 27 fveq2i ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 1 + 1 ) ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 )
29 s3fv2 ( 𝐾𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
30 6 29 syl ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
31 28 30 syl5eq ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ ( 1 + 1 ) ) = 𝐾 )
32 23 26 31 3eqtr3d ( 𝜑 → ( ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ‘ 𝐽 ) = 𝐾 )