Metamath Proof Explorer


Theorem crctcshlem3

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-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 crctcshlem3 φ G V H V Q V

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 crctistrl F Circuits G P F Trails G P
9 trliswlk F Trails G P F Walks G P
10 wlkv F Walks G P G V F V P V
11 simp1 G V F V P V G V
12 9 10 11 3syl F Trails G P G V
13 3 8 12 3syl φ G V
14 6 ovexi H V
15 14 a1i φ H V
16 ovex 0 N V
17 16 mptex x 0 N if x N S P x + S P x + S - N V
18 7 17 eqeltri Q V
19 18 a1i φ Q V
20 13 15 19 3jca φ G V H V Q V