Metamath Proof Explorer

Theorem clwlkclwwlk

Description: A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlk.v ⊢ V = Vtx ⁡ G
clwlkclwwlk.e ⊢ E = iEdg ⁡ G
Assertion clwlkclwwlk ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ClWalks ⁡ G P ↔ lastS ⁡ P = P ⁡ 0 ∧ P prefix P − 1 ∈ ClWWalks ⁡ G

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v ⊢ V = Vtx ⁡ G
2 clwlkclwwlk.e ⊢ E = iEdg ⁡ G
3 2 uspgrf1oedg ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
4 f1of1 ⊢ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G → E : dom ⁡ E ⟶ 1-1 Edg ⁡ G
5 3 4 syl ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 Edg ⁡ G
6 clwlkclwwlklem3 ⊢ E : dom ⁡ E ⟶ 1-1 Edg ⁡ G ∧ 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
7 5 6 syl3an1 ⊢ G ∈ USHGraph ∧ 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
8 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
9 ige2m1fz ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P − 1 ∈ 0 … P
10 8 9 sylan ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 ∈ 0 … P
11 pfxlen ⊢ P ∈ Word V ∧ P − 1 ∈ 0 … P → P prefix P − 1 = P − 1
12 10 11 syldan ⊢ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 = P − 1
13 8 nn0cnd ⊢ P ∈ Word V → P ∈ ℂ
14 1cnd ⊢ P ∈ Word V → 1 ∈ ℂ
15 13 14 subcld ⊢ P ∈ Word V → P − 1 ∈ ℂ
16 15 subid1d ⊢ P ∈ Word V → P - 1 - 0 = P − 1
17 16 eqcomd ⊢ P ∈ Word V → P − 1 = P - 1 - 0
18 17 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 = P - 1 - 0
19 12 18 eqtrd ⊢ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 = P - 1 - 0
20 19 oveq1d ⊢ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 − 1 = P − 1 - 0 - 1
21 20 oveq2d ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P prefix P − 1 − 1 = 0 ..^ P − 1 - 0 - 1
22 12 oveq1d ⊢ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 − 1 = P - 1 - 1
23 22 oveq2d ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P prefix P − 1 − 1 = 0 ..^ P - 1 - 1
24 23 eleq2d ⊢ P ∈ Word V ∧ 2 ≤ P → i ∈ 0 ..^ P prefix P − 1 − 1 ↔ i ∈ 0 ..^ P - 1 - 1
25 simpll ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P ∈ Word V
26 wrdlenge2n0 ⊢ P ∈ Word V ∧ 2 ≤ P → P ≠ ∅
27 26 adantr ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P ≠ ∅
28 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
29 peano2zm ⊢ P ∈ ℤ → P − 1 ∈ ℤ
30 28 29 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℤ
31 8 30 syl ⊢ P ∈ Word V → P − 1 ∈ ℤ
32 31 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 ∈ ℤ
33 elfzom1elfzo ⊢ P − 1 ∈ ℤ ∧ i ∈ 0 ..^ P - 1 - 1 → i ∈ 0 ..^ P − 1
34 32 33 sylan ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → i ∈ 0 ..^ P − 1
35 pfxtrcfv ⊢ P ∈ Word V ∧ P ≠ ∅ ∧ i ∈ 0 ..^ P − 1 → P prefix P − 1 ⁡ i = P ⁡ i
36 25 27 34 35 syl3anc ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P prefix P − 1 ⁡ i = P ⁡ i
37 8 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → P ∈ ℕ 0
38 elfzom1elp1fzo ⊢ P − 1 ∈ ℤ ∧ i ∈ 0 ..^ P - 1 - 1 → i + 1 ∈ 0 ..^ P − 1
39 30 38 sylan ⊢ P ∈ ℕ 0 ∧ i ∈ 0 ..^ P - 1 - 1 → i + 1 ∈ 0 ..^ P − 1
40 37 39 sylan ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → i + 1 ∈ 0 ..^ P − 1
41 pfxtrcfv ⊢ P ∈ Word V ∧ P ≠ ∅ ∧ i + 1 ∈ 0 ..^ P − 1 → P prefix P − 1 ⁡ i + 1 = P ⁡ i + 1
42 25 27 40 41 syl3anc ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P prefix P − 1 ⁡ i + 1 = P ⁡ i + 1
43 36 42 preq12d ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 = P ⁡ i P ⁡ i + 1
44 43 eleq1d ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P - 1 - 1 → P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
45 44 ex ⊢ P ∈ Word V ∧ 2 ≤ P → i ∈ 0 ..^ P - 1 - 1 → P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
46 24 45 sylbid ⊢ P ∈ Word V ∧ 2 ≤ P → i ∈ 0 ..^ P prefix P − 1 − 1 → P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
47 46 imp ⊢ P ∈ Word V ∧ 2 ≤ P ∧ i ∈ 0 ..^ P prefix P − 1 − 1 → P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
48 21 47 raleqbidva ⊢ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
49 pfxtrcfvl ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P prefix P − 1 = P ⁡ P − 2
50 pfxtrcfv0 ⊢ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ⁡ 0 = P ⁡ 0
51 49 50 preq12d ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 = P ⁡ P − 2 P ⁡ 0
52 51 eleq1d ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E ↔ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
53 48 52 anbi12d ⊢ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
54 53 bicomd ⊢ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
55 54 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
56 pfxcl ⊢ P ∈ Word V → P prefix P − 1 ∈ Word V
57 56 3ad2ant2 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ Word V
58 57 3biant1d ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
59 55 58 bitrd ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
60 59 anbi2d ⊢ G ∈ USHGraph ∧ 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 ↔ lastS ⁡ P = P ⁡ 0 ∧ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
61 7 60 bitrd ⊢ G ∈ USHGraph ∧ 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 ∧ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
62 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
63 1 2 isclwlkupgr ⊢ G ∈ UPGraph → f ClWalks ⁡ G P ↔ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
64 3an4anass ⊢ 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 ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
65 63 64 bitr4di ⊢ G ∈ UPGraph → f ClWalks ⁡ G P ↔ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
66 62 65 syl ⊢ G ∈ USHGraph → f ClWalks ⁡ G P ↔ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
67 66 adantr ⊢ G ∈ USHGraph ∧ P ∈ Word V → f ClWalks ⁡ G P ↔ f ∈ Word dom ⁡ E ∧ P : 0 … f ⟶ V ∧ ∀ i ∈ 0 ..^ f E ⁡ f ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ f
68 67 exbidv ⊢ G ∈ USHGraph ∧ P ∈ Word V → ∃ f f ClWalks ⁡ G 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
69 68 3adant3 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ClWalks ⁡ G 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
70 eqid ⊢ Edg ⁡ G = Edg ⁡ G
71 1 70 isclwwlk ⊢ P prefix P − 1 ∈ ClWWalks ⁡ G ↔ P prefix P − 1 ∈ Word V ∧ P prefix P − 1 ≠ ∅ ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G
72 simpl ⊢ P ∈ Word V ∧ 2 ≤ P → P ∈ Word V
73 nn0ge2m1nn ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P − 1 ∈ ℕ
74 8 73 sylan ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 ∈ ℕ
75 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
76 75 lem1d ⊢ P ∈ ℕ 0 → P − 1 ≤ P
77 76 a1d ⊢ P ∈ ℕ 0 → 2 ≤ P → P − 1 ≤ P
78 8 77 syl ⊢ P ∈ Word V → 2 ≤ P → P − 1 ≤ P
79 78 imp ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 ≤ P
80 72 74 79 3jca ⊢ P ∈ Word V ∧ 2 ≤ P → P ∈ Word V ∧ P − 1 ∈ ℕ ∧ P − 1 ≤ P
81 80 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P ∈ Word V ∧ P − 1 ∈ ℕ ∧ P − 1 ≤ P
82 pfxn0 ⊢ P ∈ Word V ∧ P − 1 ∈ ℕ ∧ P − 1 ≤ P → P prefix P − 1 ≠ ∅
83 81 82 syl ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ≠ ∅
84 83 biantrud ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ Word V ↔ P prefix P − 1 ∈ Word V ∧ P prefix P − 1 ≠ ∅
85 84 bicomd ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ Word V ∧ P prefix P − 1 ≠ ∅ ↔ P prefix P − 1 ∈ Word V
86 85 3anbi1d ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ Word V ∧ P prefix P − 1 ≠ ∅ ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G
87 71 86 syl5bb ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ ClWWalks ⁡ G ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G
88 biid ⊢ P prefix P − 1 ∈ Word V ↔ P prefix P − 1 ∈ Word V
89 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
90 2 eqcomi ⊢ iEdg ⁡ G = E
91 90 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ E
92 89 91 eqtri ⊢ Edg ⁡ G = ran ⁡ E
93 92 eleq2i ⊢ P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ↔ P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E
94 93 ralbii ⊢ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ↔ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E
95 92 eleq2i ⊢ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G ↔ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
96 88 94 95 3anbi123i ⊢ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ Edg ⁡ G ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
97 87 96 bitrdi ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → P prefix P − 1 ∈ ClWWalks ⁡ G ↔ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
98 97 anbi2d ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ P prefix P − 1 ∈ ClWWalks ⁡ G ↔ lastS ⁡ P = P ⁡ 0 ∧ P prefix P − 1 ∈ Word V ∧ ∀ i ∈ 0 ..^ P prefix P − 1 − 1 P prefix P − 1 ⁡ i P prefix P − 1 ⁡ i + 1 ∈ ran ⁡ E ∧ lastS ⁡ P prefix P − 1 P prefix P − 1 ⁡ 0 ∈ ran ⁡ E
99 61 69 98 3bitr4d ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 2 ≤ P → ∃ f f ClWalks ⁡ G P ↔ lastS ⁡ P = P ⁡ 0 ∧ P prefix P − 1 ∈ ClWWalks ⁡ G