This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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