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 ‘ 𝐺 ) 𝑄 ) |