Metamath Proof Explorer

Theorem iswwlksnx

Description: Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 iswwlksnx.v 
 |-  V = ( Vtx ` G )
2 iswwlksnx.e 
 |-  E = ( Edg ` G )
3 iswwlksn 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
4 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 ) )
5 df-3an 
 |-  ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( ( W =/= (/) /\ W e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
6 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
7 6 gt0ne0d 
 |-  ( N e. NN0 -> ( N + 1 ) =/= 0 )
8 7 adantr 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( N + 1 ) =/= 0 )
9 neeq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) =/= 0 <-> ( N + 1 ) =/= 0 ) )
10 9 adantl 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) =/= 0 <-> ( N + 1 ) =/= 0 ) )
11 8 10 mpbird 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` W ) =/= 0 )
12 hasheq0 
 |-  ( W e. Word V -> ( ( # ` W ) = 0 <-> W = (/) ) )
13 12 necon3bid 
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 <-> W =/= (/) ) )
14 11 13 syl5ibcom 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. Word V -> W =/= (/) ) )
15 14 pm4.71rd 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. Word V <-> ( W =/= (/) /\ W e. Word V ) ) )
16 15 bicomd 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W =/= (/) /\ W e. Word V ) <-> W e. Word V ) )
17 16 anbi1d 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( W =/= (/) /\ W e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
18 5 17 bitrid 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
19 4 18 bitrid 
 |-  ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. ( WWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
20 19 ex 
 |-  ( N e. NN0 -> ( ( # ` W ) = ( N + 1 ) -> ( W e. ( WWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) ) )
21 20 pm5.32rd 
 |-  ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( # ` W ) = ( N + 1 ) ) ) )
22 df-3an 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( # ` W ) = ( N + 1 ) ) )
23 21 22 bitr4di 
 |-  ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) ) )
24 3 23 bitrd 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) ) )