revpfxsfxrev

Description: The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023)

		Ref	Expression
	Assertion	revpfxsfxrev	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to reverse (W prefix L) = reverse (W) substr ⟨\|W\| - L, \|W\|⟩$

Proof

Step	Hyp	Ref	Expression
1		pfxcl	$⊢ W \in Word V \to W prefix L \in Word V$
2		revcl	$⊢ W prefix L \in Word V \to reverse (W prefix L) \in Word V$
3		wrdfn	$⊢ reverse (W prefix L) \in Word V \to reverse (W prefix L) Fn (0 ..^\|reverse (W prefix L)\|)$
4	1 2 3	3syl	$⊢ W \in Word V \to reverse (W prefix L) Fn (0 ..^\|reverse (W prefix L)\|)$
5	4	adantr	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to reverse (W prefix L) Fn (0 ..^\|reverse (W prefix L)\|)$
6		revlen	$⊢ W prefix L \in Word V \to \|reverse (W prefix L)\| = \|W prefix L\|$
7	1 6	syl	$⊢ W \in Word V \to \|reverse (W prefix L)\| = \|W prefix L\|$
8	7	adantr	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| = \|W prefix L\|$
9		pfxlen	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W prefix L\| = L$
10	8 9	eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| = L$
11	10	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (0 ..^\|reverse (W prefix L)\|) = (0 ..^L)$
12	11	fneq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (reverse (W prefix L) Fn (0 ..^\|reverse (W prefix L)\|) \leftrightarrow reverse (W prefix L) Fn (0 ..^L))$
13	5 12	mpbid	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to reverse (W prefix L) Fn (0 ..^L)$
14		revcl	$⊢ W \in Word V \to reverse (W) \in Word V$
15		swrdcl	$⊢ reverse (W) \in Word V \to reverse (W) substr ⟨\|W\| - L, \|W\|⟩ \in Word V$
16		wrdfn	$⊢ reverse (W) substr ⟨\|W\| - L, \|W\|⟩ \in Word V \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^\|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\|)$
17	14 15 16	3syl	$⊢ W \in Word V \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^\|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\|)$
18	17	adantr	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^\|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\|)$
19		fznn0sub2	$⊢ L \in (0 \dots \|W\|) \to \|W\| - L \in (0 \dots \|W\|)$
20		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
21		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
22	20 21	sylib	$⊢ W \in Word V \to \|W\| \in (0 \dots \|W\|)$
23		revlen	$⊢ W \in Word V \to \|reverse (W)\| = \|W\|$
24	23	oveq2d	$⊢ W \in Word V \to (0 \dots \|reverse (W)\|) = (0 \dots \|W\|)$
25	22 24	eleqtrrd	$⊢ W \in Word V \to \|W\| \in (0 \dots \|reverse (W)\|)$
26		swrdlen	$⊢ (reverse (W) \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|reverse (W)\|)) \to \|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\| = \|W\| - (\|W\| - L)$
27	14 19 25 26	syl3an	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land W \in Word V) \to \|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\| = \|W\| - (\|W\| - L)$
28	27	3anidm13	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\| = \|W\| - (\|W\| - L)$
29	20	nn0cnd	$⊢ W \in Word V \to \|W\| \in ℂ$
30	29	adantr	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W\| \in ℂ$
31		elfzelz	$⊢ L \in (0 \dots \|W\|) \to L \in ℤ$
32	31	zcnd	$⊢ L \in (0 \dots \|W\|) \to L \in ℂ$
33	32	adantl	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to L \in ℂ$
34	30 33	nncand	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W\| - (\|W\| - L) = L$
35	28 34	eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\| = L$
36	35	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (0 ..^\|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\|) = (0 ..^L)$
37	36	fneq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to ((reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^\|reverse (W) substr ⟨\|W\| - L, \|W\|⟩\|) \leftrightarrow (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^L))$
38	18 37	mpbid	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) Fn (0 ..^L)$
39		simp1	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to W \in Word V$
40		simp3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x \in (0 ..^L)$
41	9	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (0 ..^\|W prefix L\|) = (0 ..^L)$
42	41	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (0 ..^\|W prefix L\|) = (0 ..^L)$
43	40 42	eleqtrrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x \in (0 ..^\|W prefix L\|)$
44		revfv	$⊢ (W prefix L \in Word V \land x \in (0 ..^\|W prefix L\|)) \to reverse (W prefix L) (x) = (W prefix L) (\|W prefix L\| - 1 - x)$
45	1 44	sylan	$⊢ (W \in Word V \land x \in (0 ..^\|W prefix L\|)) \to reverse (W prefix L) (x) = (W prefix L) (\|W prefix L\| - 1 - x)$
46	39 43 45	syl2anc	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to reverse (W prefix L) (x) = (W prefix L) (\|W prefix L\| - 1 - x)$
47	9	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W prefix L\| - 1 = L - 1$
48	47	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W prefix L\| - 1 - x = L - 1 - x$
49	48	fveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (W prefix L) (\|W prefix L\| - 1 - x) = (W prefix L) (L - 1 - x)$
50	49	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (W prefix L) (\|W prefix L\| - 1 - x) = (W prefix L) (L - 1 - x)$
51	32	3ad2ant2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L \in ℂ$
52		elfzoelz	$⊢ x \in (0 ..^L) \to x \in ℤ$
53	52	zcnd	$⊢ x \in (0 ..^L) \to x \in ℂ$
54	53	3ad2ant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x \in ℂ$
55		1cnd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to 1 \in ℂ$
56	51 54 55	sub32d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L - x - 1 = L - 1 - x$
57		ubmelm1fzo	$⊢ x \in (0 ..^L) \to L - x - 1 \in (0 ..^L)$
58	57	3ad2ant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L - x - 1 \in (0 ..^L)$
59	56 58	eqeltrrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L - 1 - x \in (0 ..^L)$
60		pfxfv	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - 1 - x \in (0 ..^L)) \to (W prefix L) (L - 1 - x) = W (L - 1 - x)$
61	59 60	syld3an3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (W prefix L) (L - 1 - x) = W (L - 1 - x)$
62	46 50 61	3eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to reverse (W prefix L) (x) = W (L - 1 - x)$
63	34	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (0 ..^\|W\| - (\|W\| - L)) = (0 ..^L)$
64	63	eleq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (x \in (0 ..^\|W\| - (\|W\| - L)) \leftrightarrow x \in (0 ..^L))$
65	64	biimp3ar	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x \in (0 ..^\|W\| - (\|W\| - L))$
66		id	$⊢ (W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land W \in Word V) \to (W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land W \in Word V)$
67	66	3anidm13	$⊢ (W \in Word V \land \|W\| - L \in (0 \dots \|W\|)) \to (W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land W \in Word V)$
68		swrdfv	$⊢ ((reverse (W) \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|reverse (W)\|)) \land x \in (0 ..^\|W\| - (\|W\| - L))) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
69	14 68	syl3anl1	$⊢ ((W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|reverse (W)\|)) \land x \in (0 ..^\|W\| - (\|W\| - L))) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
70	25 69	syl3anl3	$⊢ ((W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land W \in Word V) \land x \in (0 ..^\|W\| - (\|W\| - L))) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
71	67 70	stoic3	$⊢ (W \in Word V \land \|W\| - L \in (0 \dots \|W\|) \land x \in (0 ..^\|W\| - (\|W\| - L))) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
72	19 71	syl3an2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^\|W\| - (\|W\| - L))) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
73	65 72	syld3an3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = reverse (W) (x + \|W\| - L)$
74		0z	$⊢ 0 \in ℤ$
75		elfzuz3	$⊢ L \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq L}$
76	32	addlidd	$⊢ L \in (0 \dots \|W\|) \to 0 + L = L$
77	76	fveq2d	$⊢ L \in (0 \dots \|W\|) \to ℤ_{\geq (0 + L)} = ℤ_{\geq L}$
78	75 77	eleqtrrd	$⊢ L \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq (0 + L)}$
79		eluzsub	$⊢ (0 \in ℤ \land L \in ℤ \land \|W\| \in ℤ_{\geq (0 + L)}) \to \|W\| - L \in ℤ_{\geq 0}$
80	74 31 78 79	mp3an2i	$⊢ L \in (0 \dots \|W\|) \to \|W\| - L \in ℤ_{\geq 0}$
81		fzoss1	$⊢ \|W\| - L \in ℤ_{\geq 0} \to (\|W\| - L ..^\|W\|) \subseteq (0 ..^\|W\|)$
82	80 81	syl	$⊢ L \in (0 \dots \|W\|) \to (\|W\| - L ..^\|W\|) \subseteq (0 ..^\|W\|)$
83	82	3ad2ant2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - L ..^\|W\|) \subseteq (0 ..^\|W\|)$
84	20	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
85	84	3ad2ant1	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| \in ℤ$
86	31	3ad2ant2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L \in ℤ$
87	85 86	zsubcld	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - L \in ℤ$
88		fzo0addel	$⊢ (x \in (0 ..^L) \land \|W\| - L \in ℤ) \to x + \|W\| - L \in (\|W\| - L ..^L + \|W\| - L)$
89	40 87 88	syl2anc	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x + \|W\| - L \in (\|W\| - L ..^L + \|W\| - L)$
90	30	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| \in ℂ$
91	51 90	pncan3d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to L + \|W\| - L = \|W\|$
92	91	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - L ..^L + \|W\| - L) = (\|W\| - L ..^\|W\|)$
93	89 92	eleqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x + \|W\| - L \in (\|W\| - L ..^\|W\|)$
94	83 93	sseldd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to x + \|W\| - L \in (0 ..^\|W\|)$
95		revfv	$⊢ (W \in Word V \land x + \|W\| - L \in (0 ..^\|W\|)) \to reverse (W) (x + \|W\| - L) = W (\|W\| - 1 - (x + \|W\| - L))$
96	39 94 95	syl2anc	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to reverse (W) (x + \|W\| - L) = W (\|W\| - 1 - (x + \|W\| - L))$
97	90 55	subcld	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - 1 \in ℂ$
98	87	zcnd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - L \in ℂ$
99	97 54 98	sub32d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - 1) - x - (\|W\| - L) = (\|W\| - 1) - (\|W\| - L) - x$
100	97 54 98	subsub4d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - 1) - x - (\|W\| - L) = \|W\| - 1 - (x + \|W\| - L)$
101	90 55 98	sub32d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - 1 - (\|W\| - L) = \|W\| - (\|W\| - L) - 1$
102	101	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - 1) - (\|W\| - L) - x = (\|W\| - (\|W\| - L)) - 1 - x$
103	99 100 102	3eqtr3d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - 1 - (x + \|W\| - L) = (\|W\| - (\|W\| - L)) - 1 - x$
104	34	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - (\|W\| - L) = L$
105	104	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - (\|W\| - L) - 1 = L - 1$
106	105	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (\|W\| - (\|W\| - L)) - 1 - x = L - 1 - x$
107	103 106	eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to \|W\| - 1 - (x + \|W\| - L) = L - 1 - x$
108	107	fveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to W (\|W\| - 1 - (x + \|W\| - L)) = W (L - 1 - x)$
109	73 96 108	3eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x) = W (L - 1 - x)$
110	62 109	eqtr4d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land x \in (0 ..^L)) \to reverse (W prefix L) (x) = (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x)$
111	110	3expa	$⊢ ((W \in Word V \land L \in (0 \dots \|W\|)) \land x \in (0 ..^L)) \to reverse (W prefix L) (x) = (reverse (W) substr ⟨\|W\| - L, \|W\|⟩) (x)$
112	13 38 111	eqfnfvd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to reverse (W prefix L) = reverse (W) substr ⟨\|W\| - L, \|W\|⟩$

Metamath Proof Explorer

Theorem revpfxsfxrev

Proof