Metamath Proof Explorer

Theorem clwwlknp

Description: Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v 
|- V = ( Vtx ` G )
isclwwlknx.e 
|- E = ( Edg ` G )
Assertion clwwlknp 
|- ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )

Proof

Step Hyp Ref Expression
1 isclwwlknx.v 
 |-  V = ( Vtx ` G )
2 isclwwlknx.e 
 |-  E = ( Edg ` G )
3 1 clwwlknbp 
 |-  ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ ( # ` W ) = N ) )
4 simpr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( W e. Word V /\ ( # ` W ) = N ) )
5 clwwlknnn 
 |-  ( W e. ( N ClWWalksN G ) -> N e. NN )
6 1 2 isclwwlknx 
 |-  ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = N ) ) )
7 3simpc 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
8 7 adantr 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = N ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
9 6 8 syl6bi 
 |-  ( N e. NN -> ( W e. ( N ClWWalksN G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
10 5 9 mpcom 
 |-  ( W e. ( N ClWWalksN G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
11 10 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
12 oveq1 
 |-  ( ( # ` W ) = N -> ( ( # ` W ) - 1 ) = ( N - 1 ) )
13 12 oveq2d 
 |-  ( ( # ` W ) = N -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ ( N - 1 ) ) )
14 13 raleqdv 
 |-  ( ( # ` W ) = N -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
15 14 anbi1d 
 |-  ( ( # ` W ) = N -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
16 15 ad2antll 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
17 11 16 mpbid 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
18 4 17 jca 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
19 3 18 mpdan 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
20 3anass 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
21 19 20 sylibr 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )