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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
Assertion crctcshlem2 ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 crctcsh.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
4 crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
5 crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
6 crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
7 crctiswlk ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
9 3 7 8 3syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
10 elfzoelz ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
11 5 10 syl ⊢ ( 𝜑 → 𝑆 ∈ ℤ )
12 cshwlen ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑆 ∈ ℤ ) → ( ♯ ‘ ( 𝐹 cyclShift 𝑆 ) ) = ( ♯ ‘ 𝐹 ) )
13 9 11 12 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 cyclShift 𝑆 ) ) = ( ♯ ‘ 𝐹 ) )
14 6 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 cyclShift 𝑆 ) )
15 13 14 4 3eqtr4g ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )