Metamath Proof Explorer


Theorem crctcshtrl

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a trail <. H , Q >. . (Contributed by AV, 14-Mar-2021) (Proof shortened by AV, 30-Oct-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 crctcshtrl ( 𝜑𝐻 ( Trails ‘ 𝐺 ) 𝑄 )

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 crctcshwlk ( 𝜑𝐻 ( Walks ‘ 𝐺 ) 𝑄 )
9 crctistrl ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10 2 trlf1 ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
11 df-f1 ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun 𝐹 ) )
12 iswrdi ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼𝐹 ∈ Word dom 𝐼 )
13 12 anim1i ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun 𝐹 ) → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹 ) )
14 11 13 sylbi ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹 ) )
15 10 14 syl ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹 ) )
16 3 9 15 3syl ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹 ) )
17 elfzoelz ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
18 5 17 syl ( 𝜑𝑆 ∈ ℤ )
19 df-3an ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹𝑆 ∈ ℤ ) ↔ ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹 ) ∧ 𝑆 ∈ ℤ ) )
20 16 18 19 sylanbrc ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹𝑆 ∈ ℤ ) )
21 cshinj ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun 𝐹𝑆 ∈ ℤ ) → ( 𝐻 = ( 𝐹 cyclShift 𝑆 ) → Fun 𝐻 ) )
22 20 6 21 mpisyl ( 𝜑 → Fun 𝐻 )
23 istrl ( 𝐻 ( Trails ‘ 𝐺 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ∧ Fun 𝐻 ) )
24 8 22 23 sylanbrc ( 𝜑𝐻 ( Trails ‘ 𝐺 ) 𝑄 )