Metamath Proof Explorer

Theorem isclwlke

Description: Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 16-Feb-2021)

Ref Expression
Hypotheses isclwlke.v 
|- V = ( Vtx ` G )
isclwlke.i 
|- I = ( iEdg ` G )
Assertion isclwlke 
|- ( G e. X -> ( F ( ClWalks ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isclwlke.v 
 |-  V = ( Vtx ` G )
2 isclwlke.i 
 |-  I = ( iEdg ` G )
3 isclwlk 
 |-  ( F ( ClWalks ` G ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 1 2 iswlkg 
 |-  ( G e. X -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
5 df-3an 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
6 4 5 bitrdi 
 |-  ( G e. X -> ( F ( Walks ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
7 6 anbi1d 
 |-  ( G e. X -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
8 anass 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
9 7 8 bitrdi 
 |-  ( G e. X -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
10 3 9 syl5bb 
 |-  ( G e. X -> ( F ( ClWalks ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )