Metamath Proof Explorer

Theorem clwwlknwwlksn

Description: A word representing a closed walk of length N also represents a walk of length N - 1 . The walk is one edge shorter than the closed walk, because the last edge connecting the last with the first vertex is missing. For example, if <" a b c "> e. ( 3 ClWWalksN G ) represents a closed walk "abca" of length 3, then <" a b c "> e. ( 2 WWalksN G ) represents a walk "abc" (not closed if a =/= c ) of length 2, and <" a b c a "> e. ( 3 WWalksN G ) represents also a closed walk "abca" of length 3. (Contributed by AV, 24-Jan-2022) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknwwlksn 
|- ( W e. ( N ClWWalksN G ) -> W e. ( ( N - 1 ) WWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlknnn 
 |-  ( W e. ( N ClWWalksN G ) -> N e. NN )
2 idd 
 |-  ( N e. NN -> ( W e. Word ( Vtx ` G ) -> W e. Word ( Vtx ` G ) ) )
3 idd 
 |-  ( N e. NN -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
4 nncn 
 |-  ( N e. NN -> N e. CC )
5 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
6 4 5 syl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
7 6 eqcomd 
 |-  ( N e. NN -> N = ( ( N - 1 ) + 1 ) )
8 7 eqeq2d 
 |-  ( N e. NN -> ( ( # ` W ) = N <-> ( # ` W ) = ( ( N - 1 ) + 1 ) ) )
9 8 biimpd 
 |-  ( N e. NN -> ( ( # ` W ) = N -> ( # ` W ) = ( ( N - 1 ) + 1 ) ) )
10 2 3 9 3anim123d 
 |-  ( N e. NN -> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = N ) -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
11 10 com12 
 |-  ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = N ) -> ( N e. NN -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
12 11 3exp 
 |-  ( W e. Word ( Vtx ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) ) ) )
13 12 a1dd 
 |-  ( W e. Word ( Vtx ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) ) ) ) )
14 13 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) ) ) ) )
15 14 3imp1 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = N ) -> ( N e. NN -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
16 15 com12 
 |-  ( N e. NN -> ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = N ) -> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
17 isclwwlkn 
 |-  ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
18 17 a1i 
 |-  ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) )
19 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
20 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
21 19 20 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
22 21 anbi1i 
 |-  ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) <-> ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = N ) )
23 18 22 bitrdi 
 |-  ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = N ) ) )
24 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
25 19 20 iswwlksnx 
 |-  ( ( N - 1 ) e. NN0 -> ( W e. ( ( N - 1 ) WWalksN G ) <-> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
26 24 25 syl 
 |-  ( N e. NN -> ( W e. ( ( N - 1 ) WWalksN G ) <-> ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ ( # ` W ) = ( ( N - 1 ) + 1 ) ) ) )
27 16 23 26 3imtr4d 
 |-  ( N e. NN -> ( W e. ( N ClWWalksN G ) -> W e. ( ( N - 1 ) WWalksN G ) ) )
28 1 27 mpcom 
 |-  ( W e. ( N ClWWalksN G ) -> W e. ( ( N - 1 ) WWalksN G ) )