swrdrevpfx

Description: A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fznn0sub2	$⊢ F \in (0 \dots L) \to L - F \in (0 \dots L)$
2		pfxcl	$⊢ W \in Word V \to W prefix L \in Word V$
3		revcl	$⊢ W prefix L \in Word V \to reverse (W prefix L) \in Word V$
4	2 3	syl	$⊢ W \in Word V \to reverse (W prefix L) \in Word V$
5	4	3ad2ant1	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to reverse (W prefix L) \in Word V$
6		simp3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to L - F \in (0 \dots L)$
7		revlen	$⊢ W prefix L \in Word V \to \|reverse (W prefix L)\| = \|W prefix L\|$
8	2 7	syl	$⊢ W \in Word V \to \|reverse (W prefix L)\| = \|W prefix L\|$
9	8	adantr	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| = \|W prefix L\|$
10		pfxlen	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W prefix L\| = L$
11	9 10	eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| = L$
12	11	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to \|reverse (W prefix L)\| = L$
13	12	oveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to (0 \dots \|reverse (W prefix L)\|) = (0 \dots L)$
14	6 13	eleqtrrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to L - F \in (0 \dots \|reverse (W prefix L)\|)$
15	5 14	jca	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - F \in (0 \dots L)) \to (reverse (W prefix L) \in Word V \land L - F \in (0 \dots \|reverse (W prefix L)\|))$
16	1 15	syl3an3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land F \in (0 \dots L)) \to (reverse (W prefix L) \in Word V \land L - F \in (0 \dots \|reverse (W prefix L)\|))$
17	16	3com23	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (reverse (W prefix L) \in Word V \land L - F \in (0 \dots \|reverse (W prefix L)\|))$
18		revpfxsfxrev	$⊢ (reverse (W prefix L) \in Word V \land L - F \in (0 \dots \|reverse (W prefix L)\|)) \to reverse (reverse (W prefix L) prefix (L - F)) = reverse (reverse (W prefix L)) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩$
19	17 18	syl	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to reverse (reverse (W prefix L) prefix (L - F)) = reverse (reverse (W prefix L)) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩$
20		revrev	$⊢ W prefix L \in Word V \to reverse (reverse (W prefix L)) = W prefix L$
21	2 20	syl	$⊢ W \in Word V \to reverse (reverse (W prefix L)) = W prefix L$
22	21	oveq1d	$⊢ W \in Word V \to reverse (reverse (W prefix L)) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩ = (W prefix L) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩$
23	22	3ad2ant1	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to reverse (reverse (W prefix L)) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩ = (W prefix L) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩$
24	11	oveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| - (L - F) = L - (L - F)$
25	24	3adant2	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| - (L - F) = L - (L - F)$
26		elfzel2	$⊢ F \in (0 \dots L) \to L \in ℤ$
27	26	zcnd	$⊢ F \in (0 \dots L) \to L \in ℂ$
28		elfzelz	$⊢ F \in (0 \dots L) \to F \in ℤ$
29	28	zcnd	$⊢ F \in (0 \dots L) \to F \in ℂ$
30	27 29	nncand	$⊢ F \in (0 \dots L) \to L - (L - F) = F$
31	30	3ad2ant2	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to L - (L - F) = F$
32	25 31	eqtrd	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| - (L - F) = F$
33	11	3adant2	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to \|reverse (W prefix L)\| = L$
34	32 33	opeq12d	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩ = ⟨F, L⟩$
35	34	oveq2d	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (W prefix L) substr ⟨\|reverse (W prefix L)\| - (L - F), \|reverse (W prefix L)\|⟩ = (W prefix L) substr ⟨F, L⟩$
36	19 23 35	3eqtrd	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to reverse (reverse (W prefix L) prefix (L - F)) = (W prefix L) substr ⟨F, L⟩$
37		elfzuz3	$⊢ F \in (0 \dots L) \to L \in ℤ_{\geq F}$
38		eluzfz2	$⊢ L \in ℤ_{\geq F} \to L \in (F \dots L)$
39	37 38	syl	$⊢ F \in (0 \dots L) \to L \in (F \dots L)$
40	39	ancli	$⊢ F \in (0 \dots L) \to (F \in (0 \dots L) \land L \in (F \dots L))$
41	40	3ad2ant2	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (F \in (0 \dots L) \land L \in (F \dots L))$
42		swrdpfx	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to ((F \in (0 \dots L) \land L \in (F \dots L)) \to (W prefix L) substr ⟨F, L⟩ = W substr ⟨F, L⟩)$
43	41 42	syl5	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to ((W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (W prefix L) substr ⟨F, L⟩ = W substr ⟨F, L⟩)$
44	43	3adant2	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to ((W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (W prefix L) substr ⟨F, L⟩ = W substr ⟨F, L⟩)$
45	44	pm2.43i	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to (W prefix L) substr ⟨F, L⟩ = W substr ⟨F, L⟩$
46	36 45	eqtr2d	$⊢ (W \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|W\|)) \to W substr ⟨F, L⟩ = reverse (reverse (W prefix L) prefix (L - F))$

Metamath Proof Explorer

Theorem swrdrevpfx

Proof