Metamath Proof Explorer

Theorem wlkiswwlks1

Description: The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Assertion wlkiswwlks1 
|- ( G e. UPGraph -> ( F ( Walks ` G ) P -> P e. ( WWalks ` G ) ) )

Proof

Step Hyp Ref Expression
1 wlkn0 
 |-  ( F ( Walks ` G ) P -> P =/= (/) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
5 simpr 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P =/= (/) )
6 ffz0iswrd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P e. Word ( Vtx ` G ) )
7 6 3ad2ant2 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> P e. Word ( Vtx ` G ) )
8 7 ad2antlr 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P e. Word ( Vtx ` G ) )
9 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
10 3 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
11 funfn 
 |-  ( Fun ( iEdg ` G ) <-> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
12 11 biimpi 
 |-  ( Fun ( iEdg ` G ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
13 9 10 12 3syl 
 |-  ( G e. UPGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
14 13 ad2antlr 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
15 wrdsymbcl 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. dom ( iEdg ` G ) )
16 15 ad4ant14 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. dom ( iEdg ` G ) )
17 fnfvelrn 
 |-  ( ( ( iEdg ` G ) Fn dom ( iEdg ` G ) /\ ( F ` i ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ran ( iEdg ` G ) )
18 14 16 17 syl2anc 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ran ( iEdg ` G ) )
19 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
20 18 19 eleqtrrdi 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) )
21 eleq1 
 |-  ( { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( ( iEdg ` G ) ` ( F ` i ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) ) )
22 21 eqcoms 
 |-  ( ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) ) )
23 20 22 syl5ibrcom 
 |-  ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
24 23 ralimdva 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
25 24 ex 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( G e. UPGraph -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
26 25 com23 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
27 26 3impia 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
28 27 impcom 
 |-  ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) )
29 lencl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( # ` F ) e. NN0 )
30 ffz0hash 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
31 30 ex 
 |-  ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( # ` P ) = ( ( # ` F ) + 1 ) ) )
32 oveq1 
 |-  ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` F ) + 1 ) - 1 ) )
33 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
34 pncan1 
 |-  ( ( # ` F ) e. CC -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
35 33 34 syl 
 |-  ( ( # ` F ) e. NN0 -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
36 32 35 sylan9eqr 
 |-  ( ( ( # ` F ) e. NN0 /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) )
37 36 ex 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) )
38 31 37 syld 
 |-  ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) )
39 29 38 syl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) )
40 39 imp 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) )
41 40 oveq2d 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( 0 ..^ ( # ` F ) ) )
42 41 raleqdv 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
43 42 3adant3 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
44 43 adantl 
 |-  ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
45 28 44 mpbird 
 |-  ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) )
46 45 adantr 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) )
47 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
48 2 47 iswwlks 
 |-  ( P e. ( WWalks ` G ) <-> ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
49 5 8 46 48 syl3anbrc 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P e. ( WWalks ` G ) )
50 49 ex 
 |-  ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> ( P =/= (/) -> P e. ( WWalks ` G ) ) )
51 50 ex 
 |-  ( G e. UPGraph -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( P =/= (/) -> P e. ( WWalks ` G ) ) ) )
52 4 51 sylbid 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> ( P =/= (/) -> P e. ( WWalks ` G ) ) ) )
53 1 52 mpdi 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> P e. ( WWalks ` G ) ) )