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 18 raleqdv 
 |-  ( ( 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 ) <-> A. i e. ( 0 ..^ ( ( # ` ( 2nd ` W ) ) - 1 ) ) { ( ( 2nd ` W ) ` i ) , ( ( 2nd ` W ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
20 15 19 mpbid 
 |-  ( ( 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 ) )
21 1 20 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 ) )
22 4 13 21 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 ) ) )
23 22 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 ) ) )
24 simpl 
 |-  ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> N e. NN0 )
25 oveq2 
 |-  ( ( # ` ( 1st ` W ) ) = N -> ( 0 ... ( # ` ( 1st ` W ) ) ) = ( 0 ... N ) )
26 25 adantl 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( # ` ( 1st ` W ) ) = N ) -> ( 0 ... ( # ` ( 1st ` W ) ) ) = ( 0 ... N ) )
27 26 feq2d 
 |-  ( ( ( 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 biimpd 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( # ` ( 1st ` W ) ) = N ) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
29 28 impancom 
 |-  ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( # ` ( 1st ` W ) ) = N -> ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) )
30 29 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 ) ) )
31 30 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 ) )
32 ffz0hash 
 |-  ( ( N e. NN0 /\ ( 2nd ` W ) : ( 0 ... N ) --> ( Vtx ` G ) ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) )
33 24 31 32 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 ) )
34 33 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 ) ) )
35 9 34 syl 
 |-  ( W e. ( Walks ` G ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) )
36 35 adantl 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) )
37 36 imp 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( # ` ( 2nd ` W ) ) = ( N + 1 ) )
38 24 adantl 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> N e. NN0 )
39 iswwlksn 
 |-  ( N e. NN0 -> ( ( 2nd ` W ) e. ( N WWalksN G ) <-> ( ( 2nd ` W ) e. ( WWalks ` G ) /\ ( # ` ( 2nd ` W ) ) = ( N + 1 ) ) ) )
40 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 ) ) )
41 40 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 ) ) ) )
42 41 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 ) ) ) )
43 39 42 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 ) ) ) )
44 38 43 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 ) ) ) )
45 23 37 44 mpbir2and 
 |-  ( ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) e. ( N WWalksN G ) )