Metamath Proof Explorer

Theorem wwlknp

Description: Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Hypotheses wwlkbp.v 
|- V = ( Vtx ` G )
wwlknp.e 
|- E = ( Edg ` G )
Assertion wwlknp 
|- ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )

Proof

Step Hyp Ref Expression
1 wwlkbp.v 
 |-  V = ( Vtx ` G )
2 wwlknp.e 
 |-  E = ( Edg ` G )
3 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
4 iswwlksn 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
5 1 2 iswwlks 
 |-  ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
6 simpl2 
 |-  ( ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) ) -> W e. Word V )
7 simprl 
 |-  ( ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) ) -> ( # ` W ) = ( N + 1 ) )
8 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
9 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
10 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
11 9 10 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
12 8 11 sylan9eq 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> ( ( # ` W ) - 1 ) = N )
13 12 oveq2d 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ N ) )
14 13 raleqdv 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
15 14 biimpcd 
 |-  ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
16 15 3ad2ant3 
 |-  ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
17 16 imp 
 |-  ( ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) ) -> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E )
18 6 7 17 3jca 
 |-  ( ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
19 18 ex 
 |-  ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
20 5 19 sylbi 
 |-  ( W e. ( WWalks ` G ) -> ( ( ( # ` W ) = ( N + 1 ) /\ N e. NN0 ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
21 20 expdimp 
 |-  ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( N e. NN0 -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
22 21 com12 
 |-  ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
23 4 22 sylbid 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
24 23 3ad2ant2 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
25 3 24 mpcom 
 |-  ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )