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	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )