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 
|- ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F substr <. B , L >. ) ( Walks ` G ) ( P substr <. B , ( L + 1 ) >. ) )

Proof

Step Hyp Ref Expression
1 pfxwlk 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) )
2 1 3adant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) )
3 revwlk 
 |-  ( ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) -> ( reverse ` ( F prefix L ) ) ( Walks ` G ) ( reverse ` ( P prefix ( L + 1 ) ) ) )
4 2 3 syl 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( reverse ` ( F prefix L ) ) ( Walks ` G ) ( reverse ` ( P prefix ( L + 1 ) ) ) )
5 fznn0sub2 
 |-  ( B e. ( 0 ... L ) -> ( L - B ) e. ( 0 ... L ) )
6 5 3ad2ant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L - B ) e. ( 0 ... L ) )
7 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
8 7 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
9 8 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> F e. Word dom ( iEdg ` G ) )
10 pfxcl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( F prefix L ) e. Word dom ( iEdg ` G ) )
11 revlen 
 |-  ( ( F prefix L ) e. Word dom ( iEdg ` G ) -> ( # ` ( reverse ` ( F prefix L ) ) ) = ( # ` ( F prefix L ) ) )
12 9 10 11 3syl 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( reverse ` ( F prefix L ) ) ) = ( # ` ( F prefix L ) ) )
13 pfxlen 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix L ) ) = L )
14 8 13 sylan 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix L ) ) = L )
15 14 3adant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix L ) ) = L )
16 12 15 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( reverse ` ( F prefix L ) ) ) = L )
17 16 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... ( # ` ( reverse ` ( F prefix L ) ) ) ) = ( 0 ... L ) )
18 6 17 eleqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L - B ) e. ( 0 ... ( # ` ( reverse ` ( F prefix L ) ) ) ) )
19 pfxwlk 
 |-  ( ( ( reverse ` ( F prefix L ) ) ( Walks ` G ) ( reverse ` ( P prefix ( L + 1 ) ) ) /\ ( L - B ) e. ( 0 ... ( # ` ( reverse ` ( F prefix L ) ) ) ) ) -> ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ( Walks ` G ) ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L - B ) + 1 ) ) )
20 4 18 19 syl2anc 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ( Walks ` G ) ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L - B ) + 1 ) ) )
21 elfzel2 
 |-  ( B e. ( 0 ... L ) -> L e. ZZ )
22 21 3ad2ant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> L e. ZZ )
23 22 zcnd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> L e. CC )
24 1cnd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> 1 e. CC )
25 elfzelz 
 |-  ( B e. ( 0 ... L ) -> B e. ZZ )
26 25 3ad2ant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> B e. ZZ )
27 26 zcnd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> B e. CC )
28 23 24 27 addsubd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( L + 1 ) - B ) = ( ( L - B ) + 1 ) )
29 28 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) = ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L - B ) + 1 ) ) )
30 20 29 breqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ( Walks ` G ) ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) )
31 revwlk 
 |-  ( ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ( Walks ` G ) ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) -> ( reverse ` ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ) ( Walks ` G ) ( reverse ` ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) ) )
32 30 31 syl 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( reverse ` ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ) ( Walks ` G ) ( reverse ` ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) ) )
33 swrdrevpfx 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F substr <. B , L >. ) = ( reverse ` ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ) )
34 8 33 syl3an1 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F substr <. B , L >. ) = ( reverse ` ( ( reverse ` ( F prefix L ) ) prefix ( L - B ) ) ) )
35 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
36 35 wlkpwrd 
 |-  ( F ( Walks ` G ) P -> P e. Word ( Vtx ` G ) )
37 36 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> P e. Word ( Vtx ` G ) )
38 fzelp1 
 |-  ( B e. ( 0 ... L ) -> B e. ( 0 ... ( L + 1 ) ) )
39 38 3ad2ant2 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> B e. ( 0 ... ( L + 1 ) ) )
40 fzp1elp1 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> ( L + 1 ) e. ( 0 ... ( ( # ` F ) + 1 ) ) )
41 40 3ad2ant3 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L + 1 ) e. ( 0 ... ( ( # ` F ) + 1 ) ) )
42 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
43 42 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
44 43 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... ( # ` P ) ) = ( 0 ... ( ( # ` F ) + 1 ) ) )
45 41 44 eleqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L + 1 ) e. ( 0 ... ( # ` P ) ) )
46 swrdrevpfx 
 |-  ( ( P e. Word ( Vtx ` G ) /\ B e. ( 0 ... ( L + 1 ) ) /\ ( L + 1 ) e. ( 0 ... ( # ` P ) ) ) -> ( P substr <. B , ( L + 1 ) >. ) = ( reverse ` ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) ) )
47 37 39 45 46 syl3anc 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P substr <. B , ( L + 1 ) >. ) = ( reverse ` ( ( reverse ` ( P prefix ( L + 1 ) ) ) prefix ( ( L + 1 ) - B ) ) ) )
48 32 34 47 3brtr4d 
 |-  ( ( F ( Walks ` G ) P /\ B e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F substr <. B , L >. ) ( Walks ` G ) ( P substr <. B , ( L + 1 ) >. ) )