Metamath Proof Explorer

Theorem cyc3fv1

Description: Function value of a 3-cycle at the first 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 cyc3fv1 ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ I = J

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 0elpr01 ⊢ 0 ∈ 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 ⊢ 0 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
21 20 a1i ⊢ φ → 0 ∈ 0 ..^ ⟨“ IJK ”⟩ − 1
22 1 3 10 11 21 cycpmfv1 ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 0 = ⟨“ IJK ”⟩ ⁡ 0 + 1
23 s3fv0 ⊢ I ∈ D → ⟨“ IJK ”⟩ ⁡ 0 = I
24 4 23 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 0 = I
25 24 fveq2d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ ⟨“ IJK ”⟩ ⁡ 0 = C ⁡ ⟨“ IJK ”⟩ ⁡ I
26 0p1e1 ⊢ 0 + 1 = 1
27 26 fveq2i ⊢ ⟨“ IJK ”⟩ ⁡ 0 + 1 = ⟨“ IJK ”⟩ ⁡ 1
28 s3fv1 ⊢ J ∈ D → ⟨“ IJK ”⟩ ⁡ 1 = J
29 5 28 syl ⊢ φ → ⟨“ IJK ”⟩ ⁡ 1 = J
30 27 29 eqtrid ⊢ φ → ⟨“ IJK ”⟩ ⁡ 0 + 1 = J
31 22 25 30 3eqtr3d ⊢ φ → C ⁡ ⟨“ IJK ”⟩ ⁡ I = J