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