# Metamath Proof Explorer

## Theorem crctcshlem3

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}$
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 crctcshlem3 ${⊢}{\phi }\to \left({G}\in \mathrm{V}\wedge {H}\in \mathrm{V}\wedge {Q}\in \mathrm{V}\right)$

### 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 crctistrl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
9 trliswlk ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
10 wlkv ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
11 simp1 ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to {G}\in \mathrm{V}$
12 9 10 11 3syl ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {G}\in \mathrm{V}$
13 3 8 12 3syl ${⊢}{\phi }\to {G}\in \mathrm{V}$
14 6 ovexi ${⊢}{H}\in \mathrm{V}$
15 14 a1i ${⊢}{\phi }\to {H}\in \mathrm{V}$
16 ovex ${⊢}\left(0\dots {N}\right)\in \mathrm{V}$
17 16 mptex ${⊢}\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)\in \mathrm{V}$
18 7 17 eqeltri ${⊢}{Q}\in \mathrm{V}$
19 18 a1i ${⊢}{\phi }\to {Q}\in \mathrm{V}$
20 13 15 19 3jca ${⊢}{\phi }\to \left({G}\in \mathrm{V}\wedge {H}\in \mathrm{V}\wedge {Q}\in \mathrm{V}\right)$