Metamath Proof Explorer

Theorem clwwnisshclwwsn

Description: Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018) (Revised by AV, 29-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Assertion clwwnisshclwwsn ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 cyclShift 𝑀 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlkclwwlkn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) )
2 clwwlknlen ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
3 2 eqcomd ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
4 3 oveq2d ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑊 ) ) )
5 4 eleq2d ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
6 5 biimpa ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
7 clwwisshclwwsn ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑀 ) ∈ ( ClWWalks ‘ 𝐺 ) )
8 1 6 7 syl2an2r ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 cyclShift 𝑀 ) ∈ ( ClWWalks ‘ 𝐺 ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 clwwlknwrd ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
11 elfzelz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℤ )
12 cshwlen ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
13 10 11 12 syl2an ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
14 2 adantr ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
15 13 14 eqtrd ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = 𝑁 )
16 isclwwlkn ⊢ ( ( 𝑊 cyclShift 𝑀 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 cyclShift 𝑀 ) ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = 𝑁 ) )
17 8 15 16 sylanbrc ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 cyclShift 𝑀 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )