revco

Description: Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015)

		Ref	Expression
	Assertion	revco	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ reverse (W) = reverse (F \circ W)$

Proof

Step	Hyp	Ref	Expression
1		wrdfn	$⊢ W \in Word A \to W Fn (0 ..^\|W\|)$
2	1	ad2antrr	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to W Fn (0 ..^\|W\|)$
3		lencl	$⊢ W \in Word A \to \|W\| \in ℕ_{0}$
4	3	nn0zd	$⊢ W \in Word A \to \|W\| \in ℤ$
5		fzoval	$⊢ \|W\| \in ℤ \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
6	4 5	syl	$⊢ W \in Word A \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
7	6	adantr	$⊢ (W \in Word A \land F : A ⟶ B) \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
8	7	eleq2d	$⊢ (W \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|W\|) \leftrightarrow x \in (0 \dots \|W\| - 1))$
9	8	biimpa	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to x \in (0 \dots \|W\| - 1)$
10		fznn0sub2	$⊢ x \in (0 \dots \|W\| - 1) \to \|W\| - 1 - x \in (0 \dots \|W\| - 1)$
11	9 10	syl	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to \|W\| - 1 - x \in (0 \dots \|W\| - 1)$
12	7	adantr	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
13	11 12	eleqtrrd	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to \|W\| - 1 - x \in (0 ..^\|W\|)$
14		fvco2	$⊢ (W Fn (0 ..^\|W\|) \land \|W\| - 1 - x \in (0 ..^\|W\|)) \to (F \circ W) (\|W\| - 1 - x) = F (W (\|W\| - 1 - x))$
15	2 13 14	syl2anc	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to (F \circ W) (\|W\| - 1 - x) = F (W (\|W\| - 1 - x))$
16		lenco	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$
17	16	oveq1d	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| - 1 = \|W\| - 1$
18	17	oveq1d	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| - 1 - x = \|W\| - 1 - x$
19	18	adantr	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to \|F \circ W\| - 1 - x = \|W\| - 1 - x$
20	19	fveq2d	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to (F \circ W) (\|F \circ W\| - 1 - x) = (F \circ W) (\|W\| - 1 - x)$
21		revfv	$⊢ (W \in Word A \land x \in (0 ..^\|W\|)) \to reverse (W) (x) = W (\|W\| - 1 - x)$
22	21	adantlr	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to reverse (W) (x) = W (\|W\| - 1 - x)$
23	22	fveq2d	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to F (reverse (W) (x)) = F (W (\|W\| - 1 - x))$
24	15 20 23	3eqtr4d	$⊢ ((W \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|W\|)) \to (F \circ W) (\|F \circ W\| - 1 - x) = F (reverse (W) (x))$
25	24	mpteq2dva	$⊢ (W \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x)) = (x \in (0 ..^\|W\|) ⟼ F (reverse (W) (x)))$
26	16	oveq2d	$⊢ (W \in Word A \land F : A ⟶ B) \to (0 ..^\|F \circ W\|) = (0 ..^\|W\|)$
27	26	mpteq1d	$⊢ (W \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|F \circ W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x)) = (x \in (0 ..^\|W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x))$
28		revlen	$⊢ W \in Word A \to \|reverse (W)\| = \|W\|$
29	28	adantr	$⊢ (W \in Word A \land F : A ⟶ B) \to \|reverse (W)\| = \|W\|$
30	29	oveq2d	$⊢ (W \in Word A \land F : A ⟶ B) \to (0 ..^\|reverse (W)\|) = (0 ..^\|W\|)$
31	30	mpteq1d	$⊢ (W \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|reverse (W)\|) ⟼ F (reverse (W) (x))) = (x \in (0 ..^\|W\|) ⟼ F (reverse (W) (x)))$
32	25 27 31	3eqtr4rd	$⊢ (W \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|reverse (W)\|) ⟼ F (reverse (W) (x))) = (x \in (0 ..^\|F \circ W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x))$
33		simpr	$⊢ (W \in Word A \land F : A ⟶ B) \to F : A ⟶ B$
34		revcl	$⊢ W \in Word A \to reverse (W) \in Word A$
35		wrdf	$⊢ reverse (W) \in Word A \to reverse (W) : (0 ..^\|reverse (W)\|) ⟶ A$
36	34 35	syl	$⊢ W \in Word A \to reverse (W) : (0 ..^\|reverse (W)\|) ⟶ A$
37	36	adantr	$⊢ (W \in Word A \land F : A ⟶ B) \to reverse (W) : (0 ..^\|reverse (W)\|) ⟶ A$
38		fcompt	$⊢ (F : A ⟶ B \land reverse (W) : (0 ..^\|reverse (W)\|) ⟶ A) \to F \circ reverse (W) = (x \in (0 ..^\|reverse (W)\|) ⟼ F (reverse (W) (x)))$
39	33 37 38	syl2anc	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ reverse (W) = (x \in (0 ..^\|reverse (W)\|) ⟼ F (reverse (W) (x)))$
40		ffun	$⊢ F : A ⟶ B \to Fun F$
41		simpl	$⊢ (W \in Word A \land F : A ⟶ B) \to W \in Word A$
42		cofunexg	$⊢ (Fun F \land W \in Word A) \to F \circ W \in V$
43	40 41 42	syl2an2	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ W \in V$
44		revval	$⊢ F \circ W \in V \to reverse (F \circ W) = (x \in (0 ..^\|F \circ W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x))$
45	43 44	syl	$⊢ (W \in Word A \land F : A ⟶ B) \to reverse (F \circ W) = (x \in (0 ..^\|F \circ W\|) ⟼ (F \circ W) (\|F \circ W\| - 1 - x))$
46	32 39 45	3eqtr4d	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ reverse (W) = reverse (F \circ W)$

Metamath Proof Explorer

Theorem revco

Proof