Metamath Proof Explorer

Theorem clwwlknwwlksnb

Description: A word over vertices represents a closed walk of a fixed length N greater than zero iff the word concatenated with its first symbol represents a walk of length N . This theorem would not hold for N = 0 and W = (/) , because ( W ++ <" ( W0 ) "> ) = <" (/) "> e. ( 0 WWalksN G ) could be true, but not W e. ( 0 ClWWalksN G ) <-> (/) e. (/) . (Contributed by AV, 4-Mar-2022) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v 
|- V = ( Vtx ` G )
Assertion clwwlknwwlksnb 
|- ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v 
 |-  V = ( Vtx ` G )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 ccatws1lenp1b 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )
4 2 3 sylan2 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )
5 4 anbi2d 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` W ) = N ) ) )
6 simpl 
 |-  ( ( W e. Word V /\ N e. NN ) -> W e. Word V )
7 eleq1 
 |-  ( ( # ` W ) = N -> ( ( # ` W ) e. NN <-> N e. NN ) )
8 len0nnbi 
 |-  ( W e. Word V -> ( W =/= (/) <-> ( # ` W ) e. NN ) )
9 8 biimprcd 
 |-  ( ( # ` W ) e. NN -> ( W e. Word V -> W =/= (/) ) )
10 7 9 biimtrrdi 
 |-  ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word V -> W =/= (/) ) ) )
11 10 com13 
 |-  ( W e. Word V -> ( N e. NN -> ( ( # ` W ) = N -> W =/= (/) ) ) )
12 11 imp31 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> W =/= (/) )
13 1 clwwlkwwlksb 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )
14 6 12 13 syl2an2r 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )
15 14 bicomd 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
16 15 ex 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( # ` W ) = N -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> W e. ( ClWWalks ` G ) ) ) )
17 16 pm5.32rd 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` W ) = N ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) )
18 5 17 bitrd 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) )
19 2 adantl 
 |-  ( ( W e. Word V /\ N e. NN ) -> N e. NN0 )
20 iswwlksn 
 |-  ( N e. NN0 -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) ) )
21 19 20 syl 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) ) )
22 isclwwlkn 
 |-  ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
23 22 a1i 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) )
24 18 21 23 3bitr4rd 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) ) )