cycpmfv2

Description: Value of a cycle function for the last element of the orbit. (Contributed by Thierry Arnoux, 22-Sep-2023)

	Ref	Expression
Hypotheses	tocycval.1	$⊢ C = toCyc (D)$
	tocycfv.d	$⊢ φ \to D \in V$
	tocycfv.w	$⊢ φ \to W \in Word D$
	tocycfv.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
	cycpmfv2.1	$⊢ φ \to 0 < \|W\|$
	cycpmfv2.2	$⊢ φ \to N = \|W\| - 1$
Assertion	cycpmfv2	$⊢ φ \to C (W) (W (N)) = W (0)$

Proof

Step	Hyp	Ref	Expression
1		tocycval.1	$⊢ C = toCyc (D)$
2		tocycfv.d	$⊢ φ \to D \in V$
3		tocycfv.w	$⊢ φ \to W \in Word D$
4		tocycfv.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
5		cycpmfv2.1	$⊢ φ \to 0 < \|W\|$
6		cycpmfv2.2	$⊢ φ \to N = \|W\| - 1$
7		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
8	3 7	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
9		elnnnn0b	$⊢ \|W\| \in ℕ \leftrightarrow (\|W\| \in ℕ_{0} \land 0 < \|W\|)$
10	8 5 9	sylanbrc	$⊢ φ \to \|W\| \in ℕ$
11		elfz1end	$⊢ \|W\| \in ℕ \leftrightarrow \|W\| \in (1 \dots \|W\|)$
12	10 11	sylib	$⊢ φ \to \|W\| \in (1 \dots \|W\|)$
13		fz1fzo0m1	$⊢ \|W\| \in (1 \dots \|W\|) \to \|W\| - 1 \in (0 ..^\|W\|)$
14	12 13	syl	$⊢ φ \to \|W\| - 1 \in (0 ..^\|W\|)$
15	6 14	eqeltrd	$⊢ φ \to N \in (0 ..^\|W\|)$
16	1 2 3 4 15	cycpmfvlem	$⊢ φ \to C (W) (W (N)) = ((W cyclShift 1) \circ W^{-1}) (W (N))$
17		df-f1	$⊢ W : dom W \underset{1-1}{⟶} D \leftrightarrow (W : dom W ⟶ D \land Fun W^{-1})$
18	4 17	sylib	$⊢ φ \to (W : dom W ⟶ D \land Fun W^{-1})$
19	18	simprd	$⊢ φ \to Fun W^{-1}$
20		wrdfn	$⊢ W \in Word D \to W Fn (0 ..^\|W\|)$
21	3 20	syl	$⊢ φ \to W Fn (0 ..^\|W\|)$
22		fnfvelrn	$⊢ (W Fn (0 ..^\|W\|) \land N \in (0 ..^\|W\|)) \to W (N) \in ran W$
23	21 15 22	syl2anc	$⊢ φ \to W (N) \in ran W$
24		df-rn	$⊢ ran W = dom W^{-1}$
25	23 24	eleqtrdi	$⊢ φ \to W (N) \in dom W^{-1}$
26		fvco	$⊢ (Fun W^{-1} \land W (N) \in dom W^{-1}) \to ((W cyclShift 1) \circ W^{-1}) (W (N)) = (W cyclShift 1) (W^{-1} (W (N)))$
27	19 25 26	syl2anc	$⊢ φ \to ((W cyclShift 1) \circ W^{-1}) (W (N)) = (W cyclShift 1) (W^{-1} (W (N)))$
28		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
29	4 28	syl	$⊢ φ \to W : dom W \underset{1-1 onto}{⟶} ran W$
30	21	fndmd	$⊢ φ \to dom W = (0 ..^\|W\|)$
31	15 30	eleqtrrd	$⊢ φ \to N \in dom W$
32		f1ocnvfv1	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land N \in dom W) \to W^{-1} (W (N)) = N$
33	29 31 32	syl2anc	$⊢ φ \to W^{-1} (W (N)) = N$
34	33	fveq2d	$⊢ φ \to (W cyclShift 1) (W^{-1} (W (N))) = (W cyclShift 1) (N)$
35		1zzd	$⊢ φ \to 1 \in ℤ$
36		cshwidxmod	$⊢ (W \in Word D \land 1 \in ℤ \land N \in (0 ..^\|W\|)) \to (W cyclShift 1) (N) = W ((N + 1) \mod \|W\|)$
37	3 35 15 36	syl3anc	$⊢ φ \to (W cyclShift 1) (N) = W ((N + 1) \mod \|W\|)$
38		fzossfz	$⊢ (0 ..^\|W\|) \subseteq (0 \dots \|W\|)$
39		fzssz	$⊢ (0 \dots \|W\|) \subseteq ℤ$
40	38 39	sstri	$⊢ (0 ..^\|W\|) \subseteq ℤ$
41	40 15	sselid	$⊢ φ \to N \in ℤ$
42	41	zred	$⊢ φ \to N \in ℝ$
43	10	nnrpd	$⊢ φ \to \|W\| \in ℝ^{+}$
44	6	oveq1d	$⊢ φ \to N \mod \|W\| = (\|W\| - 1) \mod \|W\|$
45		zmodidfzoimp	$⊢ \|W\| - 1 \in (0 ..^\|W\|) \to (\|W\| - 1) \mod \|W\| = \|W\| - 1$
46	14 45	syl	$⊢ φ \to (\|W\| - 1) \mod \|W\| = \|W\| - 1$
47	44 46	eqtrd	$⊢ φ \to N \mod \|W\| = \|W\| - 1$
48		modm1p1mod0	$⊢ (N \in ℝ \land \|W\| \in ℝ^{+}) \to (N \mod \|W\| = \|W\| - 1 \to (N + 1) \mod \|W\| = 0)$
49	48	imp	$⊢ ((N \in ℝ \land \|W\| \in ℝ^{+}) \land N \mod \|W\| = \|W\| - 1) \to (N + 1) \mod \|W\| = 0$
50	42 43 47 49	syl21anc	$⊢ φ \to (N + 1) \mod \|W\| = 0$
51	50	fveq2d	$⊢ φ \to W ((N + 1) \mod \|W\|) = W (0)$
52	34 37 51	3eqtrd	$⊢ φ \to (W cyclShift 1) (W^{-1} (W (N))) = W (0)$
53	16 27 52	3eqtrd	$⊢ φ \to C (W) (W (N)) = W (0)$

Metamath Proof Explorer

Theorem cycpmfv2

Proof