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