Metamath Proof Explorer

Theorem clwlkclwwlk2

Description: A closed walk corresponds to a closed walk as word in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 2-Nov-2022)

Ref Expression
Hypotheses clwlkclwwlk.v ⊢ V = Vtx ⁡ G
clwlkclwwlk.e ⊢ E = iEdg ⁡ G
Assertion clwlkclwwlk2 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∃ f f ClWalks ⁡ G P ++ ⟨“ P ⁡ 0 ”⟩ ↔ P ∈ ClWWalks ⁡ G

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v ⊢ V = Vtx ⁡ G
2 clwlkclwwlk.e ⊢ E = iEdg ⁡ G
3 simp1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → G ∈ USHGraph
4 wrdsymb1 ⊢ P ∈ Word V ∧ 1 ≤ P → P ⁡ 0 ∈ V
5 4 s1cld ⊢ P ∈ Word V ∧ 1 ≤ P → ⟨“ P ⁡ 0 ”⟩ ∈ Word V
6 ccatcl ⊢ P ∈ Word V ∧ ⟨“ P ⁡ 0 ”⟩ ∈ Word V → P ++ ⟨“ P ⁡ 0 ”⟩ ∈ Word V
7 5 6 syldan ⊢ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ ∈ Word V
8 7 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ ∈ Word V
9 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
10 1e2m1 ⊢ 1 = 2 − 1
11 10 breq1i ⊢ 1 ≤ P ↔ 2 − 1 ≤ P
12 2re ⊢ 2 ∈ ℝ
13 12 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℝ
14 1red ⊢ P ∈ ℕ 0 → 1 ∈ ℝ
15 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
16 13 14 15 lesubaddd ⊢ P ∈ ℕ 0 → 2 − 1 ≤ P ↔ 2 ≤ P + 1
17 11 16 bitrid ⊢ P ∈ ℕ 0 → 1 ≤ P ↔ 2 ≤ P + 1
18 9 17 syl ⊢ P ∈ Word V → 1 ≤ P ↔ 2 ≤ P + 1
19 18 biimpa ⊢ P ∈ Word V ∧ 1 ≤ P → 2 ≤ P + 1
20 s1len ⊢ ⟨“ P ⁡ 0 ”⟩ = 1
21 20 oveq2i ⊢ P + ⟨“ P ⁡ 0 ”⟩ = P + 1
22 19 21 breqtrrdi ⊢ P ∈ Word V ∧ 1 ≤ P → 2 ≤ P + ⟨“ P ⁡ 0 ”⟩
23 ccatlen ⊢ P ∈ Word V ∧ ⟨“ P ⁡ 0 ”⟩ ∈ Word V → P ++ ⟨“ P ⁡ 0 ”⟩ = P + ⟨“ P ⁡ 0 ”⟩
24 5 23 syldan ⊢ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ = P + ⟨“ P ⁡ 0 ”⟩
25 22 24 breqtrrd ⊢ P ∈ Word V ∧ 1 ≤ P → 2 ≤ P ++ ⟨“ P ⁡ 0 ”⟩
26 25 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → 2 ≤ P ++ ⟨“ P ⁡ 0 ”⟩
27 1 2 clwlkclwwlk ⊢ G ∈ USHGraph ∧ P ++ ⟨“ P ⁡ 0 ”⟩ ∈ Word V ∧ 2 ≤ P ++ ⟨“ P ⁡ 0 ”⟩ → ∃ f f ClWalks ⁡ G P ++ ⟨“ P ⁡ 0 ”⟩ ↔ lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0 ∧ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G
28 3 8 26 27 syl3anc ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∃ f f ClWalks ⁡ G P ++ ⟨“ P ⁡ 0 ”⟩ ↔ lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0 ∧ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G
29 wrdlenccats1lenm1 ⊢ P ∈ Word V → P ++ ⟨“ P ⁡ 0 ”⟩ − 1 = P
30 29 oveq2d ⊢ P ∈ Word V → P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 = P ++ ⟨“ P ⁡ 0 ”⟩ prefix P
31 30 adantr ⊢ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 = P ++ ⟨“ P ⁡ 0 ”⟩ prefix P
32 simpl ⊢ P ∈ Word V ∧ 1 ≤ P → P ∈ Word V
33 eqidd ⊢ P ∈ Word V ∧ 1 ≤ P → P = P
34 pfxccatid ⊢ P ∈ Word V ∧ ⟨“ P ⁡ 0 ”⟩ ∈ Word V ∧ P = P → P ++ ⟨“ P ⁡ 0 ”⟩ prefix P = P
35 32 5 33 34 syl3anc ⊢ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ prefix P = P
36 31 35 eqtr2d ⊢ P ∈ Word V ∧ 1 ≤ P → P = P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1
37 36 eleq1d ⊢ P ∈ Word V ∧ 1 ≤ P → P ∈ ClWWalks ⁡ G ↔ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G
38 lswccats1fst ⊢ P ∈ Word V ∧ 1 ≤ P → lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0
39 38 biantrurd ⊢ P ∈ Word V ∧ 1 ≤ P → P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G ↔ lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0 ∧ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G
40 37 39 bitr2d ⊢ P ∈ Word V ∧ 1 ≤ P → lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0 ∧ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G ↔ P ∈ ClWWalks ⁡ G
41 40 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0 ∧ P ++ ⟨“ P ⁡ 0 ”⟩ prefix P ++ ⟨“ P ⁡ 0 ”⟩ − 1 ∈ ClWWalks ⁡ G ↔ P ∈ ClWWalks ⁡ G
42 28 41 bitrd ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∃ f f ClWalks ⁡ G P ++ ⟨“ P ⁡ 0 ”⟩ ↔ P ∈ ClWWalks ⁡ G