tocycfvres2

Description: A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-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$
Assertion	tocycfvres2	$⊢ φ \to {C (W) ↾}_{(D ∖ ran W)} = {I ↾}_{(D ∖ ran W)}$

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	1 2 3 4	tocycfv	$⊢ φ \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
6	5	reseq1d	$⊢ φ \to {C (W) ↾}_{(D ∖ ran W)} = {(({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ↾}_{(D ∖ ran W)}$
7		fnresi	$⊢ ({I ↾}_{(D ∖ ran W)}) Fn (D ∖ ran W)$
8	7	a1i	$⊢ φ \to ({I ↾}_{(D ∖ ran W)}) Fn (D ∖ ran W)$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10		cshwfn	$⊢ (W \in Word D \land 1 \in ℤ) \to (W cyclShift 1) Fn (0 ..^\|W\|)$
11	3 9 10	syl2anc	$⊢ φ \to (W cyclShift 1) Fn (0 ..^\|W\|)$
12		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
13		f1ocnv	$⊢ W : dom W \underset{1-1 onto}{⟶} ran W \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
14		f1ofn	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} Fn ran W$
15	4 12 13 14	4syl	$⊢ φ \to W^{-1} Fn ran W$
16		dfdm4	$⊢ dom W = ran W^{-1}$
17		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
18	3 17	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
19		ssidd	$⊢ φ \to (0 ..^\|W\|) \subseteq (0 ..^\|W\|)$
20	18 19	eqsstrd	$⊢ φ \to dom W \subseteq (0 ..^\|W\|)$
21	16 20	eqsstrrid	$⊢ φ \to ran W^{-1} \subseteq (0 ..^\|W\|)$
22		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$
23	11 15 21 22	syl3anc	$⊢ φ \to ((W cyclShift 1) \circ W^{-1}) Fn ran W$
24		incom	$⊢ ran W \cap (D ∖ ran W) = (D ∖ ran W) \cap ran W$
25		disjdif	$⊢ ran W \cap (D ∖ ran W) = \emptyset$
26	24 25	eqtr3i	$⊢ (D ∖ ran W) \cap ran W = \emptyset$
27	26	a1i	$⊢ φ \to (D ∖ ran W) \cap ran W = \emptyset$
28		fnunres1	$⊢ (({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) \to {(({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ↾}_{(D ∖ ran W)} = {I ↾}_{(D ∖ ran W)}$
29	8 23 27 28	syl3anc	$⊢ φ \to {(({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) ↾}_{(D ∖ ran W)} = {I ↾}_{(D ∖ ran W)}$
30	6 29	eqtrd	$⊢ φ \to {C (W) ↾}_{(D ∖ ran W)} = {I ↾}_{(D ∖ ran W)}$

Metamath Proof Explorer

Theorem tocycfvres2

Proof