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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwlkclwwlk.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion clwlkclwwlk2 ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ↔ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) )

Proof

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