Metamath Proof Explorer

Theorem swrdwlk

Description: Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023)

Ref Expression
Assertion swrdwlk ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 substr ⟨ 𝐵 , 𝐿 ⟩ ) ( Walks ‘ 𝐺 ) ( 𝑃 substr ⟨ 𝐵 , ( 𝐿 + 1 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 pfxwlk ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) )
2 1 3adant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) )
3 revwlk ⊢ ( ( 𝐹 prefix 𝐿 ) ( Walks ‘ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) → ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) )
4 2 3 syl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) )
5 fznn0sub2 ⊢ ( 𝐵 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − 𝐵 ) ∈ ( 0 ... 𝐿 ) )
6 5 3ad2ant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 − 𝐵 ) ∈ ( 0 ... 𝐿 ) )
7 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8 7 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
9 8 3ad2ant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
10 pfxcl ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) )
11 revlen ⊢ ( ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) = ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) )
12 9 10 11 3syl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) = ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) )
13 pfxlen ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) = 𝐿 )
14 8 13 sylan ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) = 𝐿 )
15 14 3adant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝐿 ) ) = 𝐿 )
16 12 15 eqtrd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) = 𝐿 )
17 16 oveq2d ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) ) = ( 0 ... 𝐿 ) )
18 6 17 eleqtrrd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 − 𝐵 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) ) )
19 pfxwlk ⊢ ( ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) ∧ ( 𝐿 − 𝐵 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) ) ) ) → ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ( Walks ‘ 𝐺 ) ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 − 𝐵 ) + 1 ) ) )
20 4 18 19 syl2anc ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ( Walks ‘ 𝐺 ) ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 − 𝐵 ) + 1 ) ) )
21 elfzel2 ⊢ ( 𝐵 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℤ )
22 21 3ad2ant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐿 ∈ ℤ )
23 22 zcnd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐿 ∈ ℂ )
24 1cnd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 1 ∈ ℂ )
25 elfzelz ⊢ ( 𝐵 ∈ ( 0 ... 𝐿 ) → 𝐵 ∈ ℤ )
26 25 3ad2ant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐵 ∈ ℤ )
27 26 zcnd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐵 ∈ ℂ )
28 23 24 27 addsubd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐿 + 1 ) − 𝐵 ) = ( ( 𝐿 − 𝐵 ) + 1 ) )
29 28 oveq2d ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) = ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 − 𝐵 ) + 1 ) ) )
30 20 29 breqtrrd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ( Walks ‘ 𝐺 ) ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) )
31 revwlk ⊢ ( ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ( Walks ‘ 𝐺 ) ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) → ( reverse ‘ ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) ) )
32 30 31 syl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( reverse ‘ ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ) ( Walks ‘ 𝐺 ) ( reverse ‘ ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) ) )
33 swrdrevpfx ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 substr ⟨ 𝐵 , 𝐿 ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ) )
34 8 33 syl3an1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 substr ⟨ 𝐵 , 𝐿 ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝐹 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐵 ) ) ) )
35 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
36 35 wlkpwrd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
37 36 3ad2ant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
38 fzelp1 ⊢ ( 𝐵 ∈ ( 0 ... 𝐿 ) → 𝐵 ∈ ( 0 ... ( 𝐿 + 1 ) ) )
39 38 3ad2ant2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → 𝐵 ∈ ( 0 ... ( 𝐿 + 1 ) ) )
40 fzp1elp1 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
41 40 3ad2ant3 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
42 wlklenvp1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
43 42 3ad2ant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
44 43 oveq2d ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
45 41 44 eleqtrrd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐿 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) )
46 swrdrevpfx ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( 0 ... ( 𝐿 + 1 ) ) ∧ ( 𝐿 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) ) → ( 𝑃 substr ⟨ 𝐵 , ( 𝐿 + 1 ) ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) ) )
47 37 39 45 46 syl3anc ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 substr ⟨ 𝐵 , ( 𝐿 + 1 ) ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝑃 prefix ( 𝐿 + 1 ) ) ) prefix ( ( 𝐿 + 1 ) − 𝐵 ) ) ) )
48 32 34 47 3brtr4d ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐵 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 substr ⟨ 𝐵 , 𝐿 ⟩ ) ( Walks ‘ 𝐺 ) ( 𝑃 substr ⟨ 𝐵 , ( 𝐿 + 1 ) ⟩ ) )