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 e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) ( P ++ <" ( P ` 0 ) "> ) <-> P e. ( ClWWalks ` G ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v 
 |-  V = ( Vtx ` G )
2 clwlkclwwlk.e 
 |-  E = ( iEdg ` G )
3 simp1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> G e. USPGraph )
4 wrdsymb1 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( P ` 0 ) e. V )
5 4 s1cld 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> <" ( P ` 0 ) "> e. Word V )
6 ccatcl 
 |-  ( ( P e. Word V /\ <" ( P ` 0 ) "> e. Word V ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word V )
7 5 6 syldan 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word V )
8 7 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word V )
9 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
10 1e2m1 
 |-  1 = ( 2 - 1 )
11 10 breq1i 
 |-  ( 1 <_ ( # ` P ) <-> ( 2 - 1 ) <_ ( # ` P ) )
12 2re 
 |-  2 e. RR
13 12 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. RR )
14 1red 
 |-  ( ( # ` P ) e. NN0 -> 1 e. RR )
15 nn0re 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
16 13 14 15 lesubaddd 
 |-  ( ( # ` P ) e. NN0 -> ( ( 2 - 1 ) <_ ( # ` P ) <-> 2 <_ ( ( # ` P ) + 1 ) ) )
17 11 16 bitrid 
 |-  ( ( # ` P ) e. NN0 -> ( 1 <_ ( # ` P ) <-> 2 <_ ( ( # ` P ) + 1 ) ) )
18 9 17 syl 
 |-  ( P e. Word V -> ( 1 <_ ( # ` P ) <-> 2 <_ ( ( # ` P ) + 1 ) ) )
19 18 biimpa 
 |-  ( ( P e. 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 e. Word V /\ 1 <_ ( # ` P ) ) -> 2 <_ ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) )
23 ccatlen 
 |-  ( ( P e. Word V /\ <" ( P ` 0 ) "> e. Word V ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) )
24 5 23 syldan 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) )
25 22 24 breqtrrd 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> 2 <_ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) )
26 25 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> 2 <_ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) )
27 1 2 clwlkclwwlk 
 |-  ( ( G e. USPGraph /\ ( P ++ <" ( P ` 0 ) "> ) e. Word V /\ 2 <_ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) ) -> ( E. f f ( ClWalks ` G ) ( P ++ <" ( P ` 0 ) "> ) <-> ( ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) /\ ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) )
28 3 8 26 27 syl3anc 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) ( P ++ <" ( P ` 0 ) "> ) <-> ( ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) /\ ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) )
29 wrdlenccats1lenm1 
 |-  ( P e. Word V -> ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) = ( # ` P ) )
30 29 oveq2d 
 |-  ( P e. Word V -> ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) = ( ( P ++ <" ( P ` 0 ) "> ) prefix ( # ` P ) ) )
31 30 adantr 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) = ( ( P ++ <" ( P ` 0 ) "> ) prefix ( # ` P ) ) )
32 simpl 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P e. Word V )
33 eqidd 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` P ) = ( # ` P ) )
34 pfxccatid 
 |-  ( ( P e. Word V /\ <" ( P ` 0 ) "> e. Word V /\ ( # ` P ) = ( # ` P ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) prefix ( # ` P ) ) = P )
35 32 5 33 34 syl3anc 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) prefix ( # ` P ) ) = P )
36 31 35 eqtr2d 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P = ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) )
37 36 eleq1d 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( P e. ( ClWWalks ` G ) <-> ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) )
38 lswccats1fst 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )
39 38 biantrurd 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) <-> ( ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) /\ ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) ) )
40 37 39 bitr2d 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) /\ ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) <-> P e. ( ClWWalks ` G ) ) )
41 40 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) /\ ( ( P ++ <" ( P ` 0 ) "> ) prefix ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) e. ( ClWWalks ` G ) ) <-> P e. ( ClWWalks ` G ) ) )
42 28 41 bitrd 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( E. f f ( ClWalks ` G ) ( P ++ <" ( P ` 0 ) "> ) <-> P e. ( ClWWalks ` G ) ) )