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 ) } )