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 ⊢ C = toCyc ⁡ D
cycpm3.s ⊢ S = SymGrp ⁡ D
cycpm3.d ⊢ φ → D ∈ V
cycpm3.i ⊢ φ → I ∈ D
cycpm3.j ⊢ φ → J ∈ D
cycpm3.k ⊢ φ → K ∈ D
cycpm3.1 ⊢ φ → I ≠ J
cycpm3.2 ⊢ φ → J ≠ K
cycpm3.3 ⊢ φ → K ≠ I
Assertion cyc3fv2 ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ J = K

Proof

Step Hyp Ref Expression
1 cycpm3.c ⊢ C = toCyc ⁡ D
2 cycpm3.s ⊢ S = SymGrp ⁡ D
3 cycpm3.d ⊢ φ → D ∈ V
4 cycpm3.i ⊢ φ → I ∈ D
5 cycpm3.j ⊢ φ → J ∈ D
6 cycpm3.k ⊢ φ → K ∈ D
7 cycpm3.1 ⊢ φ → I ≠ J
8 cycpm3.2 ⊢ φ → J ≠ K
9 cycpm3.3 ⊢ φ → K ≠ I
10 4 5 6 s3cld ⊢ φ → ⟨“ IJK ”⟩ ∈ Word D
11 4 5 6 7 8 9 s3f1 ⊢ φ → ⟨“ IJK ”⟩ : dom ⁡ ⟨“ IJK ”⟩ ⟶ 1-1 D
12 1elpr01 ⊢ 1 ∈ 0 1
13 s3len ⊢ ⟨“ IJK ”⟩ = 3
14 13 oveq1i ⊢ ⟨“ IJK ”⟩ − 1 = 3 − 1
15 3m1e2 ⊢ 3 − 1 = 2
16 14 15 eqtri ⊢ ⟨“ IJK ”⟩ − 1 = 2
17 16 oveq2i ⊢ 0 ..^ ⟨“ IJK ”⟩ − 1 = 0 ..^ 2
18 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
19 17 18 eqtri ⊢ 0 ..^ ⟨“ IJK ”⟩ − 1 = 0 1
20 12 19 eleqtrri ⊢ 1 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
21 20 a1i ⊢ φ → 1 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
22 1 3 10 11 21 cycpmfv1 ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 1 = ⟨“ IJK ”⟩ ⁡ 1 + 1
23 s3fv1 ⊢ J ∈ D → ⟨“ IJK ”⟩ ⁡ 1 = J
24 5 23 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 1 = J
25 24 fveq2d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 1 = C ⁡ ⟨“ IJK ”⟩ ⁡ J
26 1p1e2 ⊢ 1 + 1 = 2
27 26 fveq2i ⊢ ⟨“ IJK ”⟩ ⁡ 1 + 1 = ⟨“ IJK ”⟩ ⁡ 2
28 s3fv2 ⊢ K ∈ D → ⟨“ IJK ”⟩ ⁡ 2 = K
29 6 28 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 2 = K
30 27 29 eqtrid ⊢ φ → ⟨“ IJK ”⟩ ⁡ 1 + 1 = K
31 22 25 30 3eqtr3d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ J = K