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 ⊢ V = Vtx ⁡ G
crctcsh.i ⊢ I = iEdg ⁡ G
crctcsh.d ⊢ φ → F Circuits ⁡ G P
crctcsh.n ⊢ N = F
crctcsh.s ⊢ φ → S ∈ 0 ..^ N
crctcsh.h ⊢ H = F cyclShift S
crctcsh.q ⊢ Q = x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N
Assertion crctcshtrl ⊢ φ → H Trails ⁡ G Q

Proof

Step Hyp Ref Expression
1 crctcsh.v ⊢ V = Vtx ⁡ G
2 crctcsh.i ⊢ I = iEdg ⁡ G
3 crctcsh.d ⊢ φ → F Circuits ⁡ G P
4 crctcsh.n ⊢ N = F
5 crctcsh.s ⊢ φ → S ∈ 0 ..^ N
6 crctcsh.h ⊢ H = F cyclShift S
7 crctcsh.q ⊢ Q = x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N
8 1 2 3 4 5 6 7 crctcshwlk ⊢ φ → H Walks ⁡ G Q
9 crctistrl ⊢ F Circuits ⁡ G P → F Trails ⁡ G P
10 2 trlf1 ⊢ F Trails ⁡ G P → F : 0 ..^ F ⟶ 1-1 dom ⁡ I
11 df-f1 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I ∧ Fun ⁡ F -1
12 iswrdi ⊢ F : 0 ..^ F ⟶ dom ⁡ I → F ∈ Word dom ⁡ I
13 12 anim1i ⊢ F : 0 ..^ F ⟶ dom ⁡ I ∧ Fun ⁡ F -1 → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1
14 11 13 sylbi ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ I → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1
15 3 9 10 14 4syl ⊢ φ → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1
16 elfzoelz ⊢ S ∈ 0 ..^ N → S ∈ ℤ
17 5 16 syl ⊢ φ → S ∈ ℤ
18 df-3an ⊢ F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ S ∈ ℤ ↔ F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ S ∈ ℤ
19 15 17 18 sylanbrc ⊢ φ → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ S ∈ ℤ
20 cshinj ⊢ F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ S ∈ ℤ → H = F cyclShift S → Fun ⁡ H -1
21 19 6 20 mpisyl ⊢ φ → Fun ⁡ H -1
22 istrl ⊢ H Trails ⁡ G Q ↔ H Walks ⁡ G Q ∧ Fun ⁡ H -1
23 8 21 22 sylanbrc ⊢ φ → H Trails ⁡ G Q