This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crctcshwlk

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

Ref Expression
Hypotheses crctcsh.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
crctcsh.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion crctcshwlk ( 𝜑 → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )

Proof

Step Hyp Ref Expression
1 crctcsh.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
4 crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
5 crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
6 crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
7 crctcsh.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
8 1 2 3 4 5 6 7 crctcshlem4 ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) )
9 crctistrl ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
11 3 9 10 3syl ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
12 breq12 ⊢ ( ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) → ( 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ↔ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
13 11 12 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ) )
15 8 14 mpd ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )
16 1 2 3 4 5 6 7 crctcshwlkn0 ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )
17 15 16 pm2.61dane ⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )