Metamath Proof Explorer


Theorem crctcshlem2

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
Assertion crctcshlem2 φ H = N

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 crctiswlk F Circuits G P F Walks G P
8 2 wlkf F Walks G P F Word dom I
9 3 7 8 3syl φ F Word dom I
10 elfzoelz S 0 ..^ N S
11 5 10 syl φ S
12 cshwlen F Word dom I S F cyclShift S = F
13 9 11 12 syl2anc φ F cyclShift S = F
14 6 fveq2i H = F cyclShift S
15 13 14 4 3eqtr4g φ H = N