Metamath Proof Explorer

Theorem clwlkcompbp

Description: Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022)

Ref Expression
Hypotheses clwlkcompbp.1 
|- F = ( 1st ` W )
clwlkcompbp.2 
|- P = ( 2nd ` W )
Assertion clwlkcompbp 
|- ( W e. ( ClWalks ` G ) -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlkcompbp.1 
 |-  F = ( 1st ` W )
2 clwlkcompbp.2 
 |-  P = ( 2nd ` W )
3 clwlkwlk 
 |-  ( W e. ( ClWalks ` G ) -> W e. ( Walks ` G ) )
4 wlkop 
 |-  ( W e. ( Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
5 3 4 syl 
 |-  ( W e. ( ClWalks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
6 eleq1 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. ( ClWalks ` G ) <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. ( ClWalks ` G ) ) )
7 df-br 
 |-  ( ( 1st ` W ) ( ClWalks ` G ) ( 2nd ` W ) <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. ( ClWalks ` G ) )
8 6 7 bitr4di 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. ( ClWalks ` G ) <-> ( 1st ` W ) ( ClWalks ` G ) ( 2nd ` W ) ) )
9 isclwlk 
 |-  ( ( 1st ` W ) ( ClWalks ` G ) ( 2nd ` W ) <-> ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) /\ ( ( 2nd ` W ) ` 0 ) = ( ( 2nd ` W ) ` ( # ` ( 1st ` W ) ) ) ) )
10 1 2 breq12i 
 |-  ( F ( Walks ` G ) P <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
11 2 fveq1i 
 |-  ( P ` 0 ) = ( ( 2nd ` W ) ` 0 )
12 1 fveq2i 
 |-  ( # ` F ) = ( # ` ( 1st ` W ) )
13 2 12 fveq12i 
 |-  ( P ` ( # ` F ) ) = ( ( 2nd ` W ) ` ( # ` ( 1st ` W ) ) )
14 11 13 eqeq12i 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( ( 2nd ` W ) ` 0 ) = ( ( 2nd ` W ) ` ( # ` ( 1st ` W ) ) ) )
15 10 14 anbi12i 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) /\ ( ( 2nd ` W ) ` 0 ) = ( ( 2nd ` W ) ` ( # ` ( 1st ` W ) ) ) ) )
16 9 15 sylbb2 
 |-  ( ( 1st ` W ) ( ClWalks ` G ) ( 2nd ` W ) -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
17 8 16 syl6bi 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. ( ClWalks ` G ) -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
18 5 17 mpcom 
 |-  ( W e. ( ClWalks ` G ) -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )