This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlknwwlkncl

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknwwlkncl 
|- ( W e. ( N ClWWalksN G ) -> ( W ++ <" ( W ` 0 ) "> ) e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } )

Proof

Step Hyp Ref Expression
1 clwwlknnn 
 |-  ( W e. ( N ClWWalksN G ) -> N e. NN )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 clwwlknbp 
 |-  ( W e. ( N ClWWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) )
4 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
5 2 4 clwwlknp 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
6 3simpc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
7 5 6 syl 
 |-  ( W e. ( N ClWWalksN G ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
8 eqid 
 |-  { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
9 8 clwwlkel 
 |-  ( ( N e. NN /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) -> ( W ++ <" ( W ` 0 ) "> ) e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } )
10 1 3 7 9 syl3anc 
 |-  ( W e. ( N ClWWalksN G ) -> ( W ++ <" ( W ` 0 ) "> ) e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } )