Metamath Proof Explorer

Theorem clwwisshclwwsn

Description: Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jun-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Assertion clwwisshclwwsn ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 clwwlkbp ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) )
4 3 simp2d ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
5 cshwn ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
6 4 5 syl ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
7 6 adantr ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
8 1 7 sylan9eq ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 cyclShift 𝑁 ) = 𝑊 )
9 simprl ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) )
10 8 9 eqeltrd ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )
11 simprl ⊢ ( ( ¬ 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) )
12 df-ne ⊢ ( 𝑁 ≠ ( ♯ ‘ 𝑊 ) ↔ ¬ 𝑁 = ( ♯ ‘ 𝑊 ) )
13 fzofzim ⊢ ( ( 𝑁 ≠ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 13 expcom ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ≠ ( ♯ ‘ 𝑊 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
15 12 14 biimtrrid ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ¬ 𝑁 = ( ♯ ‘ 𝑊 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
16 15 adantl ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ¬ 𝑁 = ( ♯ ‘ 𝑊 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
17 16 impcom ⊢ ( ( ¬ 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 clwwisshclwws ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )
19 11 17 18 syl2anc ⊢ ( ( ¬ 𝑁 = ( ♯ ‘ 𝑊 ) ∧ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )
20 10 19 pm2.61ian ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )