Metamath Proof Explorer

Theorem upgrclwlkcompim

Description: Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 2-May-2021)

Ref Expression
Hypotheses isclwlke.v 
|- V = ( Vtx ` G )
isclwlke.i 
|- I = ( iEdg ` G )
clwlkcomp.1 
|- F = ( 1st ` W )
clwlkcomp.2 
|- P = ( 2nd ` W )
Assertion upgrclwlkcompim 
|- ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 isclwlke.v 
 |-  V = ( Vtx ` G )
2 isclwlke.i 
 |-  I = ( iEdg ` G )
3 clwlkcomp.1 
 |-  F = ( 1st ` W )
4 clwlkcomp.2 
 |-  P = ( 2nd ` W )
5 1 2 3 4 clwlkcompim 
 |-  ( W e. ( ClWalks ` G ) -> ( ( 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 ) ) ) ) )
6 5 adantl 
 |-  ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) -> ( ( 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 ) ) ) ) )
7 simprl 
 |-  ( ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) /\ ( ( 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 ) )
8 clwlkwlk 
 |-  ( W e. ( ClWalks ` G ) -> W e. ( Walks ` G ) )
9 1 2 3 4 upgrwlkcompim 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
10 9 simp3d 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
11 8 10 sylan2 
 |-  ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
12 11 adantr 
 |-  ( ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) /\ ( ( 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 ) ) ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
13 simprrr 
 |-  ( ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) /\ ( ( 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 ) ) ) ) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
14 7 12 13 3jca 
 |-  ( ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) /\ ( ( 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 ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
15 6 14 mpdan 
 |-  ( ( G e. UPGraph /\ W e. ( ClWalks ` G ) ) -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )