Metamath Proof Explorer

Theorem wlknewwlksn

Description: If a walk in a pseudograph has length N , then the sequence of the vertices of the walk is a word representing the walk as word of length N . (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion wlknewwlksn 
|- ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) e. ( N WWalksN G ) )

Proof

Step Hyp Ref Expression
1 wlkcpr 
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
2 wlkn0 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 2nd ` W ) =/= (/) )
3 1 2 sylbi 
 |-  ( W e. ( Walks ` G ) -> ( 2nd ` W ) =/= (/) )
4 3 adantl 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( 2nd ` W ) =/= (/) )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 eqid 
 |-  ( 1st ` W ) = ( 1st ` W )
8 eqid 
 |-  ( 2nd ` W ) = ( 2nd ` W )
9 5 6 7 8 wlkelwrd 
 |-  ( W e. ( Walks ` G ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) )
10 ffz0iswrd 
 |-  ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) -> ( 2nd ` W ) e. Word ( Vtx ` G ) )
11 10 adantl 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( 2nd ` W ) e. Word ( Vtx ` G ) )
12 9 11 syl 
 |-  ( W e. ( Walks ` G ) -> ( 2nd ` W ) e. Word ( Vtx ` G ) )
13 12 adantl 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( 2nd ` W ) e. Word ( Vtx ` G ) )
14 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
15 14 upgrwlkvtxedg 
 |-  ( ( G e. UPGraph /\ ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) -> A. i e. ( 0 ..^ ( # ` ( 1st ` W ) ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
16 wlklenvm1 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( # ` ( 1st ` W ) ) = ( ( # ` ( 2nd ` W ) ) - 1 ) )
17 16 adantl 
 |-  ( ( G e. UPGraph /\ ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) -> ( # ` ( 1st ` W ) ) = ( ( # ` ( 2nd ` W ) ) - 1 ) )
18 17 oveq2d 
 |-  ( ( G e. UPGraph /\ ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) -> ( 0 ..^ ( # ` ( 1st ` W ) ) ) = ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) )
19 15 18 raleqtrdv 
 |-  ( ( G e. UPGraph /\ ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) -> A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
20 1 19 sylan2b 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
21 4 13 20 3jca 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
22 21 adantr 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
23 simpl 
 |-  ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> N e. NN0 )
24 oveq2 
 |-  ( ( # ` ( 1st ` W ) ) = N -> ( 0 ... ( # ` ( 1st ` W ) ) ) = ( 0 ... N ) )
25 24 adantl 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( # ` ( 1st ` W ) ) = N ) -> ( 0 ... ( # ` ( 1st ` W ) ) ) = ( 0 ... N ) )
26 25 feq2d 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( # ` ( 1st ` W ) ) = N ) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) <-> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
27 26 biimpd 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( # ` ( 1st ` W ) ) = N ) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
28 27 impancom 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( # ` ( 1st ` W ) ) = N -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
29 28 adantld 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
30 29 imp 
 |-  ( ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) )
31 ffz0hash 
 |-  ( ( N e. NN0 /\ ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) )
32 23 30 31 syl2an2 
 |-  ( ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) )
33 32 ex 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) )
34 9 33 syl 
 |-  ( W e. ( Walks ` G ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) )
35 34 adantl 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) )
36 35 imp 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) )
37 23 adantl 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> N e. NN0 )
38 iswwlksn 
 |-  ( N e. NN0 -> ( ( 2nd ` W ) e. ( N WWalksN G ) <-> ( ( 2nd ` W ) e. ( WWalks ` G ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) ) )
39 5 14 iswwlks 
 |-  ( ( 2nd ` W ) e. ( WWalks ` G ) <-> ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
40 39 a1i 
 |-  ( N e. NN0 -> ( ( 2nd ` W ) e. ( WWalks ` G ) <-> ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
41 40 anbi1d 
 |-  ( N e. NN0 -> ( ( ( 2nd ` W ) e. ( WWalks ` G ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) <-> ( ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) ) )
42 38 41 bitrd 
 |-  ( N e. NN0 -> ( ( 2nd ` W ) e. ( N WWalksN G ) <-> ( ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) ) )
43 37 42 syl 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( ( 2nd ` W ) e. ( N WWalksN G ) <-> ( ( ( 2nd ` W ) =/= (/) /\ ( 2nd ` W ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) ) )
44 22 36 43 mpbir2and 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) e. ( N WWalksN G ) )