cshco

Description: Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018)

		Ref	Expression
	Assertion	cshco	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to F \circ (W cyclShift N) = (F \circ W) cyclShift N$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2	1	3ad2ant3	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to F Fn A$
3		cshwfn	$⊢ (W \in Word A \land N \in ℤ) \to (W cyclShift N) Fn (0 ..^\|W\|)$
4	3	3adant3	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (W cyclShift N) Fn (0 ..^\|W\|)$
5		cshwrn	$⊢ (W \in Word A \land N \in ℤ) \to ran (W cyclShift N) \subseteq A$
6	5	3adant3	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to ran (W cyclShift N) \subseteq A$
7		fnco	$⊢ (F Fn A \land (W cyclShift N) Fn (0 ..^\|W\|) \land ran (W cyclShift N) \subseteq A) \to (F \circ (W cyclShift N)) Fn (0 ..^\|W\|)$
8	2 4 6 7	syl3anc	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (F \circ (W cyclShift N)) Fn (0 ..^\|W\|)$
9		wrdco	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ W \in Word B$
10	9	3adant2	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to F \circ W \in Word B$
11		simp2	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to N \in ℤ$
12		cshwfn	$⊢ (F \circ W \in Word B \land N \in ℤ) \to ((F \circ W) cyclShift N) Fn (0 ..^\|F \circ W\|)$
13	10 11 12	syl2anc	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to ((F \circ W) cyclShift N) Fn (0 ..^\|F \circ W\|)$
14		lenco	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$
15	14	3adant2	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$
16	15	oveq2d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (0 ..^\|F \circ W\|) = (0 ..^\|W\|)$
17	16	fneq2d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (((F \circ W) cyclShift N) Fn (0 ..^\|F \circ W\|) \leftrightarrow ((F \circ W) cyclShift N) Fn (0 ..^\|W\|))$
18	13 17	mpbid	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to ((F \circ W) cyclShift N) Fn (0 ..^\|W\|)$
19	15	adantr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to \|F \circ W\| = \|W\|$
20	19	oveq2d	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|F \circ W\| = (i + N) \mod \|W\|$
21	20	fveq2d	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to W ((i + N) \mod \|F \circ W\|) = W ((i + N) \mod \|W\|)$
22	21	fveq2d	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to F (W ((i + N) \mod \|F \circ W\|)) = F (W ((i + N) \mod \|W\|))$
23		wrdfn	$⊢ W \in Word A \to W Fn (0 ..^\|W\|)$
24	23	3ad2ant1	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to W Fn (0 ..^\|W\|)$
25	24	adantr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to W Fn (0 ..^\|W\|)$
26		elfzoelz	$⊢ i \in (0 ..^\|W\|) \to i \in ℤ$
27		zaddcl	$⊢ (i \in ℤ \land N \in ℤ) \to i + N \in ℤ$
28	26 11 27	syl2anr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to i + N \in ℤ$
29		elfzo0	$⊢ i \in (0 ..^\|W\|) \leftrightarrow (i \in ℕ_{0} \land \|W\| \in ℕ \land i < \|W\|)$
30	29	simp2bi	$⊢ i \in (0 ..^\|W\|) \to \|W\| \in ℕ$
31	30	adantl	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to \|W\| \in ℕ$
32		zmodfzo	$⊢ (i + N \in ℤ \land \|W\| \in ℕ) \to (i + N) \mod \|W\| \in (0 ..^\|W\|)$
33	28 31 32	syl2anc	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|W\| \in (0 ..^\|W\|)$
34	15	oveq2d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (i + N) \mod \|F \circ W\| = (i + N) \mod \|W\|$
35	34	eleq1d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to ((i + N) \mod \|F \circ W\| \in (0 ..^\|W\|) \leftrightarrow (i + N) \mod \|W\| \in (0 ..^\|W\|))$
36	35	adantr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to ((i + N) \mod \|F \circ W\| \in (0 ..^\|W\|) \leftrightarrow (i + N) \mod \|W\| \in (0 ..^\|W\|))$
37	33 36	mpbird	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|F \circ W\| \in (0 ..^\|W\|)$
38		fvco2	$⊢ (W Fn (0 ..^\|W\|) \land (i + N) \mod \|F \circ W\| \in (0 ..^\|W\|)) \to (F \circ W) ((i + N) \mod \|F \circ W\|) = F (W ((i + N) \mod \|F \circ W\|))$
39	25 37 38	syl2anc	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (F \circ W) ((i + N) \mod \|F \circ W\|) = F (W ((i + N) \mod \|F \circ W\|))$
40		simpl1	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to W \in Word A$
41	11	adantr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to N \in ℤ$
42		simpr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to i \in (0 ..^\|W\|)$
43		cshwidxmod	$⊢ (W \in Word A \land N \in ℤ \land i \in (0 ..^\|W\|)) \to (W cyclShift N) (i) = W ((i + N) \mod \|W\|)$
44	43	fveq2d	$⊢ (W \in Word A \land N \in ℤ \land i \in (0 ..^\|W\|)) \to F ((W cyclShift N) (i)) = F (W ((i + N) \mod \|W\|))$
45	40 41 42 44	syl3anc	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to F ((W cyclShift N) (i)) = F (W ((i + N) \mod \|W\|))$
46	22 39 45	3eqtr4rd	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to F ((W cyclShift N) (i)) = (F \circ W) ((i + N) \mod \|F \circ W\|)$
47		fvco2	$⊢ ((W cyclShift N) Fn (0 ..^\|W\|) \land i \in (0 ..^\|W\|)) \to (F \circ (W cyclShift N)) (i) = F ((W cyclShift N) (i))$
48	4 47	sylan	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (F \circ (W cyclShift N)) (i) = F ((W cyclShift N) (i))$
49	10	adantr	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to F \circ W \in Word B$
50	15	eqcomd	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to \|W\| = \|F \circ W\|$
51	50	oveq2d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (0 ..^\|W\|) = (0 ..^\|F \circ W\|)$
52	51	eleq2d	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to (i \in (0 ..^\|W\|) \leftrightarrow i \in (0 ..^\|F \circ W\|))$
53	52	biimpa	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to i \in (0 ..^\|F \circ W\|)$
54		cshwidxmod	$⊢ (F \circ W \in Word B \land N \in ℤ \land i \in (0 ..^\|F \circ W\|)) \to ((F \circ W) cyclShift N) (i) = (F \circ W) ((i + N) \mod \|F \circ W\|)$
55	49 41 53 54	syl3anc	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to ((F \circ W) cyclShift N) (i) = (F \circ W) ((i + N) \mod \|F \circ W\|)$
56	46 48 55	3eqtr4d	$⊢ ((W \in Word A \land N \in ℤ \land F : A ⟶ B) \land i \in (0 ..^\|W\|)) \to (F \circ (W cyclShift N)) (i) = ((F \circ W) cyclShift N) (i)$
57	8 18 56	eqfnfvd	$⊢ (W \in Word A \land N \in ℤ \land F : A ⟶ B) \to F \circ (W cyclShift N) = (F \circ W) cyclShift N$

Metamath Proof Explorer

Theorem cshco

Proof