Metamath Proof Explorer

Theorem clwwlknonel

Description: Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G . This theorem would not hold for N = 0 if W = X = (/) . (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlknonel.v 
 |-  V = ( Vtx ` G )
2 clwwlknonel.e 
 |-  E = ( Edg ` G )
3 1 2 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
4 simpl 
 |-  ( ( ( # ` W ) = N /\ W = (/) ) -> ( # ` W ) = N )
5 fveq2 
 |-  ( W = (/) -> ( # ` W ) = ( # ` (/) ) )
6 hash0 
 |-  ( # ` (/) ) = 0
7 5 6 eqtrdi 
 |-  ( W = (/) -> ( # ` W ) = 0 )
8 7 adantl 
 |-  ( ( ( # ` W ) = N /\ W = (/) ) -> ( # ` W ) = 0 )
9 4 8 eqtr3d 
 |-  ( ( ( # ` W ) = N /\ W = (/) ) -> N = 0 )
10 9 ex 
 |-  ( ( # ` W ) = N -> ( W = (/) -> N = 0 ) )
11 10 necon3d 
 |-  ( ( # ` W ) = N -> ( N =/= 0 -> W =/= (/) ) )
12 11 impcom 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> W =/= (/) )
13 12 biantrud 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> ( W e. Word V <-> ( W e. Word V /\ W =/= (/) ) ) )
14 13 bicomd 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> ( ( W e. Word V /\ W =/= (/) ) <-> W e. Word V ) )
15 14 3anbi1d 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> ( ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
16 3 15 syl5bb 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> ( W e. ( ClWWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
17 16 a1d 
 |-  ( ( N =/= 0 /\ ( # ` W ) = N ) -> ( ( W ` 0 ) = X -> ( W e. ( ClWWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
18 17 expimpd 
 |-  ( N =/= 0 -> ( ( ( # ` W ) = N /\ ( W ` 0 ) = X ) -> ( W e. ( ClWWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
19 18 pm5.32rd 
 |-  ( N =/= 0 -> ( ( W e. ( ClWWalks ` G ) /\ ( ( # ` W ) = N /\ ( W ` 0 ) = X ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( ( # ` W ) = N /\ ( W ` 0 ) = X ) ) ) )
20 isclwwlknon 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
21 isclwwlkn 
 |-  ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
22 21 anbi1i 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) <-> ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) /\ ( W ` 0 ) = X ) )
23 anass 
 |-  ( ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) /\ ( W ` 0 ) = X ) <-> ( W e. ( ClWWalks ` G ) /\ ( ( # ` W ) = N /\ ( W ` 0 ) = X ) ) )
24 20 22 23 3bitri 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( ClWWalks ` G ) /\ ( ( # ` W ) = N /\ ( W ` 0 ) = X ) ) )
25 3anass 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = N /\ ( W ` 0 ) = X ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( ( # ` W ) = N /\ ( W ` 0 ) = X ) ) )
26 19 24 25 3bitr4g 
 |-  ( N =/= 0 -> ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = N /\ ( W ` 0 ) = X ) ) )