Theorem crctcshlem2

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)

	Ref	Expression
Hypotheses	crctcsh.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	crctcsh.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	crctcsh.d	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
	crctcsh.n	$$⊢N=\left|F\right|$$
	crctcsh.s	$$⊢\phi \to S\in \left(0..^N\right)$$
	crctcsh.h	$$⊢H=F\mathrm{cyclShift}S$$
Assertion	crctcshlem2	$$⊢\phi \to \left|H\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		crctcsh.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		crctcsh.d	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
4		crctcsh.n	$$⊢N=\left|F\right|$$
5		crctcsh.s	$$⊢\phi \to S\in \left(0..^N\right)$$
6		crctcsh.h	$$⊢H=F\mathrm{cyclShift}S$$
7		crctiswlk	$$⊢F\mathrm{Circuits}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
8	2	wlkf	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$
9	3 7 8	3syl	$$⊢\phi \to F\in \mathrm{Word}\mathrm{dom}I$$
10		elfzoelz	$$⊢S\in \left(0..^N\right)\to S\in \mathbb{Z}$$
11	5 10	syl	$$⊢\phi \to S\in \mathbb{Z}$$
12		cshwlen	$$⊢\left(F\in \mathrm{Word}\mathrm{dom}I\wedge S\in \mathbb{Z}\right)\to \left|F\mathrm{cyclShift}S\right|=\left|F\right|$$
13	9 11 12	syl2anc	$$⊢\phi \to \left|F\mathrm{cyclShift}S\right|=\left|F\right|$$
14	6	fveq2i	$$⊢\left|H\right|=\left|F\mathrm{cyclShift}S\right|$$
15	13 14 4	3eqtr4g	$$⊢\phi \to \left|H\right|=N$$