Metamath Proof Explorer

Theorem isclwwlknx

Description: Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v 
|- V = ( Vtx ` G )
isclwwlknx.e 
|- E = ( Edg ` G )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 isclwwlknx.v 
 |-  V = ( Vtx ` G )
2 isclwwlknx.e 
 |-  E = ( Edg ` G )
3 eleq1 
 |-  ( ( # ` W ) = N -> ( ( # ` W ) e. NN <-> N e. NN ) )
4 len0nnbi 
 |-  ( W e. Word V -> ( W =/= (/) <-> ( # ` W ) e. NN ) )
5 4 biimprcd 
 |-  ( ( # ` W ) e. NN -> ( W e. Word V -> W =/= (/) ) )
6 3 5 biimtrrdi 
 |-  ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word V -> W =/= (/) ) ) )
7 6 impcom 
 |-  ( ( N e. NN /\ ( # ` W ) = N ) -> ( W e. Word V -> W =/= (/) ) )
8 7 imp 
 |-  ( ( ( N e. NN /\ ( # ` W ) = N ) /\ W e. Word V ) -> W =/= (/) )
9 8 biantrurd 
 |-  ( ( ( N e. NN /\ ( # ` W ) = N ) /\ W e. Word V ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
10 9 bicomd 
 |-  ( ( ( N e. NN /\ ( # ` W ) = N ) /\ W e. Word V ) -> ( ( W =/= (/) /\ ( 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 ) ) )
11 10 pm5.32da 
 |-  ( ( N e. NN /\ ( # ` W ) = N ) -> ( ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) <-> ( W e. Word V /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
12 11 ex 
 |-  ( N e. NN -> ( ( # ` W ) = N -> ( ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) <-> ( W e. Word V /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) ) )
13 12 pm5.32rd 
 |-  ( N e. NN -> ( ( ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) /\ ( # ` W ) = N ) <-> ( ( 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 ) ) )
14 isclwwlkn 
 |-  ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
15 1 2 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) )
16 3anass 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
17 anass 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) <-> ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
18 16 17 bitri 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
19 15 18 bitri 
 |-  ( W e. ( ClWWalks ` G ) <-> ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) )
20 19 anbi1i 
 |-  ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) <-> ( ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) /\ ( # ` W ) = N ) )
21 14 20 bitri 
 |-  ( W e. ( N ClWWalksN G ) <-> ( ( W e. Word V /\ ( W =/= (/) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) ) /\ ( # ` W ) = N ) )
22 3anass 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) <-> ( W e. Word V /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) )
23 22 anbi1i 
 |-  ( ( ( 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 ) <-> ( ( 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 ) )
24 13 21 23 3bitr4g 
 |-  ( 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 ) ) )