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∈WordV∧1≤P→∃ffClWalks⁡GP++⟨“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∈WordV∧1≤P→G∈USHGraph
4 wrdsymb1 ⊢P∈WordV∧1≤P→P⁡0∈V
5 4 s1cld ⊢P∈WordV∧1≤P→⟨“P⁡0”⟩∈WordV
6 ccatcl ⊢P∈WordV∧⟨“P⁡0”⟩∈WordV→P++⟨“P⁡0”⟩∈WordV
7 5 6 syldan ⊢P∈WordV∧1≤P→P++⟨“P⁡0”⟩∈WordV
8 7 3adant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→P++⟨“P⁡0”⟩∈WordV
9 lencl ⊢P∈WordV→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∈WordV→1≤P↔2≤P+1
19 18 biimpa ⊢P∈WordV∧1≤P→2≤P+1
20 s1len ⊢⟨“P⁡0”⟩=1
21 20 oveq2i ⊢P+⟨“P⁡0”⟩=P+1
22 19 21 breqtrrdi ⊢P∈WordV∧1≤P→2≤P+⟨“P⁡0”⟩
23 ccatlen ⊢P∈WordV∧⟨“P⁡0”⟩∈WordV→P++⟨“P⁡0”⟩=P+⟨“P⁡0”⟩
24 5 23 syldan ⊢P∈WordV∧1≤P→P++⟨“P⁡0”⟩=P+⟨“P⁡0”⟩
25 22 24 breqtrrd ⊢P∈WordV∧1≤P→2≤P++⟨“P⁡0”⟩
26 25 3adant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→2≤P++⟨“P⁡0”⟩
27 1 2 clwlkclwwlk ⊢G∈USHGraph∧P++⟨“P⁡0”⟩∈WordV∧2≤P++⟨“P⁡0”⟩→∃ffClWalks⁡GP++⟨“P⁡0”⟩↔lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0∧P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G
28 3 8 26 27 syl3anc ⊢G∈USHGraph∧P∈WordV∧1≤P→∃ffClWalks⁡GP++⟨“P⁡0”⟩↔lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0∧P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G
29 wrdlenccats1lenm1 ⊢P∈WordV→P++⟨“P⁡0”⟩−1=P
30 29 oveq2d ⊢P∈WordV→P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1=P++⟨“P⁡0”⟩prefixP
31 30 adantr ⊢P∈WordV∧1≤P→P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1=P++⟨“P⁡0”⟩prefixP
32 simpl ⊢P∈WordV∧1≤P→P∈WordV
33 eqidd ⊢P∈WordV∧1≤P→P=P
34 pfxccatid ⊢P∈WordV∧⟨“P⁡0”⟩∈WordV∧P=P→P++⟨“P⁡0”⟩prefixP=P
35 32 5 33 34 syl3anc ⊢P∈WordV∧1≤P→P++⟨“P⁡0”⟩prefixP=P
36 31 35 eqtr2d ⊢P∈WordV∧1≤P→P=P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1
37 36 eleq1d ⊢P∈WordV∧1≤P→P∈ClWWalks⁡G↔P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G
38 lswccats1fst ⊢P∈WordV∧1≤P→lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0
39 38 biantrurd ⊢P∈WordV∧1≤P→P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G↔lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0∧P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G
40 37 39 bitr2d ⊢P∈WordV∧1≤P→lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0∧P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G↔P∈ClWWalks⁡G
41 40 3adant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0∧P++⟨“P⁡0”⟩prefixP++⟨“P⁡0”⟩−1∈ClWWalks⁡G↔P∈ClWWalks⁡G
42 28 41 bitrd ⊢G∈USHGraph∧P∈WordV∧1≤P→∃ffClWalks⁡GP++⟨“P⁡0”⟩↔P∈ClWWalks⁡G