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	|- ( ph -> F ( Circuits ` G ) P )
	crctcsh.n	|- N = ( # ` F )
	crctcsh.s	|- ( ph -> S e. ( 0 ..^ N ) )
	crctcsh.h	|- H = ( F cyclShift S )
Assertion	crctcshlem2	|- ( ph -> ( # ` H ) = N )

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	|- V = ( Vtx ` G )
2		crctcsh.i	|- I = ( iEdg ` G )
3		crctcsh.d	|- ( ph -> F ( Circuits ` G ) P )
4		crctcsh.n	|- N = ( # ` F )
5		crctcsh.s	|- ( ph -> S e. ( 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 e. Word dom I )
9	3 7 8	3syl	|- ( ph -> F e. Word dom I )
10		elfzoelz	|- ( S e. ( 0 ..^ N ) -> S e. ZZ )
11	5 10	syl	|- ( ph -> S e. ZZ )
12		cshwlen	|- ( ( F e. Word dom I /\ S e. ZZ ) -> ( # ` ( F cyclShift S ) ) = ( # ` F ) )
13	9 11 12	syl2anc	|- ( ph -> ( # ` ( F cyclShift S ) ) = ( # ` F ) )
14	6	fveq2i	|- ( # ` H ) = ( # ` ( F cyclShift S ) )
15	13 14 4	3eqtr4g	|- ( ph -> ( # ` H ) = N )