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 1ex ⊢ 1 ∈ V
13 12 prid2 ⊢ 1 ∈ 0 1
14 s3len ⊢ ⟨“ IJK ”⟩ = 3
15 14 oveq1i ⊢ ⟨“ IJK ”⟩ − 1 = 3 − 1
16 3m1e2 ⊢ 3 − 1 = 2
17 15 16 eqtri ⊢ ⟨“ IJK ”⟩ − 1 = 2
18 17 oveq2i ⊢ 0 ..^ ⟨“ IJK ”⟩ − 1 = 0 ..^ 2
19 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
20 18 19 eqtri ⊢ 0 ..^ ⟨“ IJK ”⟩ − 1 = 0 1
21 13 20 eleqtrri ⊢ 1 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
22 21 a1i ⊢ φ → 1 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
23 1 3 10 11 22 cycpmfv1 ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 1 = ⟨“ IJK ”⟩ ⁡ 1 + 1
24 s3fv1 ⊢ J ∈ D → ⟨“ IJK ”⟩ ⁡ 1 = J
25 5 24 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 1 = J
26 25 fveq2d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 1 = C ⁡ ⟨“ IJK ”⟩ ⁡ J
27 1p1e2 ⊢ 1 + 1 = 2
28 27 fveq2i ⊢ ⟨“ IJK ”⟩ ⁡ 1 + 1 = ⟨“ IJK ”⟩ ⁡ 2
29 s3fv2 ⊢ K ∈ D → ⟨“ IJK ”⟩ ⁡ 2 = K
30 6 29 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 2 = K
31 28 30 syl5eq ⊢ φ → ⟨“ IJK ”⟩ ⁡ 1 + 1 = K
32 23 26 31 3eqtr3d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ J = K