# 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}=\mathrm{Vtx}\left({G}\right)$
crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
crctcsh.n ${⊢}{N}=\left|{F}\right|$
crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
Assertion crctcshtrl ${⊢}{\phi }\to {H}\mathrm{Trails}\left({G}\right){Q}$

### Proof

Step Hyp Ref Expression
1 crctcsh.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
4 crctcsh.n ${⊢}{N}=\left|{F}\right|$
5 crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
6 crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
7 crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
8 1 2 3 4 5 6 7 crctcshwlk ${⊢}{\phi }\to {H}\mathrm{Walks}\left({G}\right){Q}$
9 crctistrl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
10 2 trlf1 ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}$
11 df-f1 ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}↔\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
12 iswrdi ${⊢}{F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{I}\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
13 12 anim1i ${⊢}\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
14 11 13 sylbi ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
15 10 14 syl ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
16 3 9 15 3syl ${⊢}{\phi }\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
17 elfzoelz ${⊢}{S}\in \left(0..^{N}\right)\to {S}\in ℤ$
18 5 17 syl ${⊢}{\phi }\to {S}\in ℤ$
19 df-3an ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\wedge {S}\in ℤ\right)↔\left(\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\right)\wedge {S}\in ℤ\right)$
20 16 18 19 sylanbrc ${⊢}{\phi }\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\wedge {S}\in ℤ\right)$
21 cshinj ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \mathrm{Fun}{{F}}^{-1}\wedge {S}\in ℤ\right)\to \left({H}={F}\mathrm{cyclShift}{S}\to \mathrm{Fun}{{H}}^{-1}\right)$
22 20 6 21 mpisyl ${⊢}{\phi }\to \mathrm{Fun}{{H}}^{-1}$
23 istrl ${⊢}{H}\mathrm{Trails}\left({G}\right){Q}↔\left({H}\mathrm{Walks}\left({G}\right){Q}\wedge \mathrm{Fun}{{H}}^{-1}\right)$
24 8 22 23 sylanbrc ${⊢}{\phi }\to {H}\mathrm{Trails}\left({G}\right){Q}$