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 syl6bir
 |-  ( ( # ` 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 ) ) )