Metamath Proof Explorer

Theorem swrdrevpfx

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

Ref Expression
Assertion swrdrevpfx ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 fznn0sub2 ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) )
2 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 )
3 revcl ⊢ ( ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 → ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 )
4 2 3 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 )
5 4 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 )
6 simp3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) )
7 revlen ⊢ ( ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) )
8 2 7 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) )
9 8 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) )
10 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) = 𝐿 )
11 9 10 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = 𝐿 )
12 11 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = 𝐿 )
13 12 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) = ( 0 ... 𝐿 ) )
14 6 13 eleqtrrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( 𝐿 − 𝐹 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) )
15 5 14 jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... 𝐿 ) ) → ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) ) )
16 1 15 syl3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ) → ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) ) )
17 16 3com23 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) ) )
18 revpfxsfxrev ⊢ ( ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ∈ Word 𝑉 ∧ ( 𝐿 − 𝐹 ) ∈ ( 0 ... ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ) ) → ( reverse ‘ ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐹 ) ) ) = ( ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) )
19 17 18 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( reverse ‘ ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐹 ) ) ) = ( ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) )
20 revrev ⊢ ( ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 → ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = ( 𝑊 prefix 𝐿 ) )
21 2 20 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = ( 𝑊 prefix 𝐿 ) )
22 21 oveq1d ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) = ( ( 𝑊 prefix 𝐿 ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) )
23 22 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) = ( ( 𝑊 prefix 𝐿 ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) )
24 11 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) = ( 𝐿 − ( 𝐿 − 𝐹 ) ) )
25 24 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) = ( 𝐿 − ( 𝐿 − 𝐹 ) ) )
26 elfzel2 ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℤ )
27 26 zcnd ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℂ )
28 elfzelz ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐹 ∈ ℤ )
29 28 zcnd ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐹 ∈ ℂ )
30 27 29 nncand ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − ( 𝐿 − 𝐹 ) ) = 𝐹 )
31 30 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 − ( 𝐿 − 𝐹 ) ) = 𝐹 )
32 25 31 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) = 𝐹 )
33 11 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) = 𝐿 )
34 32 33 opeq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ = ⟨ 𝐹 , 𝐿 ⟩ )
35 34 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) substr ⟨ ( ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) − ( 𝐿 − 𝐹 ) ) , ( ♯ ‘ ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) ) ⟩ ) = ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) )
36 19 23 35 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( reverse ‘ ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐹 ) ) ) = ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) )
37 elfzuz3 ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) )
38 eluzfz2 ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) → 𝐿 ∈ ( 𝐹 ... 𝐿 ) )
39 37 38 syl ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ( 𝐹 ... 𝐿 ) )
40 39 ancli ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 𝐹 ... 𝐿 ) ) )
41 40 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 𝐹 ... 𝐿 ) ) )
42 swrdpfx ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 𝐹 ... 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) )
43 41 42 syl5 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) )
44 43 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) )
45 44 pm2.43i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) )
46 36 45 eqtr2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( reverse ‘ ( ( reverse ‘ ( 𝑊 prefix 𝐿 ) ) prefix ( 𝐿 − 𝐹 ) ) ) )