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 ) ) )