cycpmfvlem

	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$
	cycpmfvlem.1	$⊢ φ \to N \in (0 ..^\|W\|)$
Assertion	cycpmfvlem	$⊢ φ \to C (W) (W (N)) = ((W cyclShift 1) \circ W^{-1}) (W (N))$

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

Metamath Proof Explorer

Theorem cycpmfvlem

Proof