# Metamath Proof Explorer

## Theorem crctcshlem2

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-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}$
Assertion crctcshlem2 ${⊢}{\phi }\to \left|{H}\right|={N}$

### 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 crctiswlk ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
8 2 wlkf ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
9 3 7 8 3syl ${⊢}{\phi }\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
10 elfzoelz ${⊢}{S}\in \left(0..^{N}\right)\to {S}\in ℤ$
11 5 10 syl ${⊢}{\phi }\to {S}\in ℤ$
12 cshwlen ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {S}\in ℤ\right)\to \left|{F}\mathrm{cyclShift}{S}\right|=\left|{F}\right|$
13 9 11 12 syl2anc ${⊢}{\phi }\to \left|{F}\mathrm{cyclShift}{S}\right|=\left|{F}\right|$
14 6 fveq2i ${⊢}\left|{H}\right|=\left|{F}\mathrm{cyclShift}{S}\right|$
15 13 14 4 3eqtr4g ${⊢}{\phi }\to \left|{H}\right|={N}$