Metamath Proof Explorer

Theorem swrdpfx

Description: A subword of a prefix is a subword. (Contributed by Alexander van der Vekens, 6-Apr-2018) (Revised by AV, 8-May-2020)

Ref Expression
Assertion swrdpfx ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐾 , 𝐿 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℕ0 )
2 1 anim2i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
3 2 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
4 pfxval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix 𝑁 ) = ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) )
5 3 4 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑊 prefix 𝑁 ) = ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) )
6 5 oveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( 𝑊 prefix 𝑁 ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) substr ⟨ 𝐾 , 𝐿 ⟩ ) )
7 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
8 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
9 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
10 1 9 syl ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ... 𝑁 ) )
11 10 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 0 ∈ ( 0 ... 𝑁 ) )
12 7 8 11 3jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ... 𝑁 ) ) )
13 12 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ... 𝑁 ) ) )
14 elfzelz ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
15 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
16 15 subid1d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 )
17 16 eqcomd ⊢ ( 𝑁 ∈ ℤ → 𝑁 = ( 𝑁 − 0 ) )
18 14 17 syl ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 = ( 𝑁 − 0 ) )
19 18 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 = ( 𝑁 − 0 ) )
20 19 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( 𝑁 − 0 ) ) )
21 20 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ∈ ( 0 ... ( 𝑁 − 0 ) ) ) )
22 19 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐾 ... 𝑁 ) = ( 𝐾 ... ( 𝑁 − 0 ) ) )
23 22 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 0 ) ) ) )
24 21 23 anbi12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ↔ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 0 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 0 ) ) ) ) )
25 24 biimpa ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 0 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 0 ) ) ) )
26 swrdswrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 0 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 0 ) ) ) → ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 0 + 𝐾 ) , ( 0 + 𝐿 ) ⟩ ) ) )
27 13 25 26 sylc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 0 + 𝐾 ) , ( 0 + 𝐿 ) ⟩ ) )
28 elfzelz ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
29 28 zcnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℂ )
30 29 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐾 ∈ ℂ )
31 30 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝐾 ∈ ℂ )
32 31 addlidd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 0 + 𝐾 ) = 𝐾 )
33 elfzelz ⊢ ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) → 𝐿 ∈ ℤ )
34 33 zcnd ⊢ ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) → 𝐿 ∈ ℂ )
35 34 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐿 ∈ ℂ )
36 35 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝐿 ∈ ℂ )
37 36 addlidd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 0 + 𝐿 ) = 𝐿 )
38 32 37 opeq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ⟨ ( 0 + 𝐾 ) , ( 0 + 𝐿 ) ⟩ = ⟨ 𝐾 , 𝐿 ⟩ )
39 38 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑊 substr ⟨ ( 0 + 𝐾 ) , ( 0 + 𝐿 ) ⟩ ) = ( 𝑊 substr ⟨ 𝐾 , 𝐿 ⟩ ) )
40 6 27 39 3eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( 𝑊 prefix 𝑁 ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐾 , 𝐿 ⟩ ) )
41 40 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ 𝐾 , 𝐿 ⟩ ) ) )