Metamath Proof Explorer

Theorem clwlkclwwlklem3

Description: Lemma 3 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem3 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E

Proof

Step Hyp Ref Expression
1 simp1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → E : dom ⁡ E ⟶ 1-1 R
2 simp1 ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → f ∈ Word dom ⁡ E
3 2 adantr ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → f ∈ Word dom ⁡ E
4 1 3 anim12i ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → E : dom ⁡ E ⟶ 1-1 R ∧ f ∈ Word dom ⁡ E
5 simp3 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → 2 ≤ P
6 simpl2 ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → P : 0 … f ⟶ V
7 5 6 anim12ci ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → P : 0 … f ⟶ V ∧ 2 ≤ P
8 simp3 ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1
9 8 anim1i ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
10 9 adantl ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
11 clwlkclwwlklem2 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ 2 ≤ P ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
12 4 7 10 11 syl3anc ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
13 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
14 lencl ⊢ f ∈ Word dom ⁡ E → f ∈ ℕ 0
15 ffz0hash ⊢ f ∈ ℕ 0 ∧ P : 0 … f ⟶ V → P = f + 1
16 oveq1 ⊢ P = f + 1 → P − 1 = f + 1 - 1
17 16 oveq1d ⊢ P = f + 1 → P - 1 - 0 = f + 1 - 1 - 0
18 nn0cn ⊢ f ∈ ℕ 0 → f ∈ ℂ
19 peano2cn ⊢ f ∈ ℂ → f + 1 ∈ ℂ
20 peano2cnm ⊢ f + 1 ∈ ℂ → f + 1 - 1 ∈ ℂ
21 18 19 20 3syl ⊢ f ∈ ℕ 0 → f + 1 - 1 ∈ ℂ
22 21 subid1d ⊢ f ∈ ℕ 0 → f + 1 - 1 - 0 = f + 1 - 1
23 1cnd ⊢ f ∈ ℕ 0 → 1 ∈ ℂ
24 18 23 pncand ⊢ f ∈ ℕ 0 → f + 1 - 1 = f
25 22 24 eqtrd ⊢ f ∈ ℕ 0 → f + 1 - 1 - 0 = f
26 25 adantr ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 → f + 1 - 1 - 0 = f
27 17 26 sylan9eqr ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P - 1 - 0 = f
28 27 oveq1d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P − 1 - 0 - 1 = f − 1
29 28 oveq2d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → 0 ..^ P − 1 - 0 - 1 = 0 ..^ f − 1
30 29 raleqdv ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
31 oveq1 ⊢ P = f + 1 → P − 2 = f + 1 - 2
32 2cnd ⊢ f ∈ ℕ 0 → 2 ∈ ℂ
33 18 32 23 subsub3d ⊢ f ∈ ℕ 0 → f − 2 − 1 = f + 1 - 2
34 2m1e1 ⊢ 2 − 1 = 1
35 34 a1i ⊢ f ∈ ℕ 0 → 2 − 1 = 1
36 35 oveq2d ⊢ f ∈ ℕ 0 → f − 2 − 1 = f − 1
37 33 36 eqtr3d ⊢ f ∈ ℕ 0 → f + 1 - 2 = f − 1
38 37 adantr ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 → f + 1 - 2 = f − 1
39 31 38 sylan9eqr ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P − 2 = f − 1
40 39 fveq2d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P ⁡ P − 2 = P ⁡ f − 1
41 40 preq1d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P ⁡ P − 2 P ⁡ 0 = P ⁡ f − 1 P ⁡ 0
42 41 eleq1d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
43 30 42 anbi12d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
44 43 anbi2d ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
45 3anass ⊢ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
46 44 45 bitr4di ⊢ f ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ P = f + 1 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
47 46 expcom ⊢ P = f + 1 → f ∈ ℕ 0 ∧ P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
48 47 expd ⊢ P = f + 1 → f ∈ ℕ 0 → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
49 15 48 syl ⊢ f ∈ ℕ 0 ∧ P : 0 … f ⟶ V → f ∈ ℕ 0 → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
50 49 ex ⊢ f ∈ ℕ 0 → P : 0 … f ⟶ V → f ∈ ℕ 0 → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
51 50 com23 ⊢ f ∈ ℕ 0 → f ∈ ℕ 0 → P : 0 … f ⟶ V → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
52 14 14 51 sylc ⊢ f ∈ Word dom ⁡ E → P : 0 … f ⟶ V → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
53 52 imp ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
54 53 3adant3 ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
55 54 adantr ⊢ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → P ∈ ℕ 0 → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
56 13 55 syl5com ⊢ P ∈ Word V → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
57 56 3ad2ant2 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
58 57 imp ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ f − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ f − 1 P ⁡ 0 ∈ ran ⁡ E
59 12 58 mpbird ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
60 59 ex ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
61 60 exlimdv ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
62 clwlkclwwlklem1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
63 61 62 impbid ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f ↔ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E