cycpmfv3

Description: Values outside of the orbit are unchanged by a cycle. (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$
	cycpmfv3.1	$⊢ φ \to X \in D$
	cycpmfv3.2	$⊢ φ \to \neg X \in ran W$
Assertion	cycpmfv3	$⊢ φ \to C (W) (X) = X$

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		cycpmfv3.1	$⊢ φ \to X \in D$
6		cycpmfv3.2	$⊢ φ \to \neg X \in ran W$
7	1 2 3 4	tocycfv	$⊢ φ \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
8	7	fveq1d	$⊢ φ \to C (W) (X) = (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) (X)$
9		f1oi	$⊢ ({I ↾}_{(D ∖ ran W)}) : D ∖ ran W \underset{1-1 onto}{⟶} D ∖ ran W$
10		f1ofn	$⊢ ({I ↾}_{(D ∖ ran W)}) : D ∖ ran W \underset{1-1 onto}{⟶} D ∖ ran W \to ({I ↾}_{(D ∖ ran W)}) Fn (D ∖ ran W)$
11	9 10	mp1i	$⊢ φ \to ({I ↾}_{(D ∖ ran W)}) Fn (D ∖ ran W)$
12		1zzd	$⊢ φ \to 1 \in ℤ$
13		cshwf	$⊢ (W \in Word D \land 1 \in ℤ) \to (W cyclShift 1) : (0 ..^\|W\|) ⟶ D$
14	3 12 13	syl2anc	$⊢ φ \to (W cyclShift 1) : (0 ..^\|W\|) ⟶ D$
15	14	ffnd	$⊢ φ \to (W cyclShift 1) Fn (0 ..^\|W\|)$
16		df-f1	$⊢ W : dom W \underset{1-1}{⟶} D \leftrightarrow (W : dom W ⟶ D \land Fun W^{-1})$
17	4 16	sylib	$⊢ φ \to (W : dom W ⟶ D \land Fun W^{-1})$
18	17	simprd	$⊢ φ \to Fun W^{-1}$
19	18	funfnd	$⊢ φ \to W^{-1} Fn dom W^{-1}$
20		df-rn	$⊢ ran W = dom W^{-1}$
21	20	fneq2i	$⊢ W^{-1} Fn ran W \leftrightarrow W^{-1} Fn dom W^{-1}$
22	19 21	sylibr	$⊢ φ \to W^{-1} Fn ran W$
23		dfdm4	$⊢ dom W = ran W^{-1}$
24	23	eqimss2i	$⊢ ran W^{-1} \subseteq dom W$
25		wrdfn	$⊢ W \in Word D \to W Fn (0 ..^\|W\|)$
26	3 25	syl	$⊢ φ \to W Fn (0 ..^\|W\|)$
27	26	fndmd	$⊢ φ \to dom W = (0 ..^\|W\|)$
28	24 27	sseqtrid	$⊢ φ \to ran W^{-1} \subseteq (0 ..^\|W\|)$
29		fnco	$⊢ ((W cyclShift 1) Fn (0 ..^\|W\|) \land W^{-1} Fn ran W \land ran W^{-1} \subseteq (0 ..^\|W\|)) \to ((W cyclShift 1) \circ W^{-1}) Fn ran W$
30	15 22 28 29	syl3anc	$⊢ φ \to ((W cyclShift 1) \circ W^{-1}) Fn ran W$
31		disjdifr	$⊢ (D ∖ ran W) \cap ran W = \emptyset$
32	31	a1i	$⊢ φ \to (D ∖ ran W) \cap ran W = \emptyset$
33	5 6	eldifd	$⊢ φ \to X \in (D ∖ ran W)$
34		fvun1	$⊢ (({I ↾}_{(D ∖ ran W)}) Fn (D ∖ ran W) \land ((W cyclShift 1) \circ W^{-1}) Fn ran W \land ((D ∖ ran W) \cap ran W = \emptyset \land X \in (D ∖ ran W))) \to (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) (X) = ({I ↾}_{(D ∖ ran W)}) (X)$
35	11 30 32 33 34	syl112anc	$⊢ φ \to (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) (X) = ({I ↾}_{(D ∖ ran W)}) (X)$
36		fvresi	$⊢ X \in (D ∖ ran W) \to ({I ↾}_{(D ∖ ran W)}) (X) = X$
37	33 36	syl	$⊢ φ \to ({I ↾}_{(D ∖ ran W)}) (X) = X$
38	8 35 37	3eqtrd	$⊢ φ \to C (W) (X) = X$

Metamath Proof Explorer

Theorem cycpmfv3

Proof