Metamath Proof Explorer

Theorem isclwwlk

Description: Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Hypotheses clwwlk.v 
|- V = ( Vtx ` G )
clwwlk.e 
|- E = ( Edg ` G )
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 clwwlk.v 
 |-  V = ( Vtx ` G )
2 clwwlk.e 
 |-  E = ( Edg ` G )
3 neeq1 
 |-  ( w = W -> ( w =/= (/) <-> W =/= (/) ) )
4 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
5 4 oveq1d 
 |-  ( w = W -> ( ( # ` w ) - 1 ) = ( ( # ` W ) - 1 ) )
6 5 oveq2d 
 |-  ( w = W -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = ( 0 ..^ ( ( # ` W ) - 1 ) ) )
7 fveq1 
 |-  ( w = W -> ( w ` i ) = ( W ` i ) )
8 fveq1 
 |-  ( w = W -> ( w ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
9 7 8 preq12d 
 |-  ( w = W -> { ( w ` i ) , ( w ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
10 9 eleq1d 
 |-  ( w = W -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
11 6 10 raleqbidv 
 |-  ( w = W -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
12 fveq2 
 |-  ( w = W -> ( lastS ` w ) = ( lastS ` W ) )
13 fveq1 
 |-  ( w = W -> ( w ` 0 ) = ( W ` 0 ) )
14 12 13 preq12d 
 |-  ( w = W -> { ( lastS ` w ) , ( w ` 0 ) } = { ( lastS ` W ) , ( W ` 0 ) } )
15 14 eleq1d 
 |-  ( w = W -> ( { ( lastS ` w ) , ( w ` 0 ) } e. E <-> { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
16 3 11 15 3anbi123d 
 |-  ( w = W -> ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) <-> ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
17 16 elrab 
 |-  ( W e. { 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 /\ ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
18 1 2 clwwlk 
 |-  ( 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 ) }
19 18 eleq2i 
 |-  ( W e. ( ClWWalks ` G ) <-> W e. { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } )
20 3anass 
 |-  ( ( ( 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 /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
21 anass 
 |-  ( ( ( 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 /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
22 3anass 
 |-  ( ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
23 22 bicomi 
 |-  ( ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) <-> ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
24 23 anbi2i 
 |-  ( ( 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 /\ ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
25 20 21 24 3bitri 
 |-  ( ( ( 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 /\ ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
26 17 19 25 3bitr4i 
 |-  ( 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 ) )