Metamath Proof Explorer

Theorem pfxswrd

Description: A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018) (Revised by AV, 8-May-2020)

Ref Expression
Assertion pfxswrd ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) prefix 𝐿 ) = ( 𝑊 substr ⟨ 𝑀 , ( 𝑀 + 𝐿 ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 ovexd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ V )
2 elfznn0 ⊢ ( 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝐿 ∈ ℕ0 )
3 pfxval ⊢ ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) prefix 𝐿 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 0 , 𝐿 ⟩ ) )
4 1 2 3 syl2an ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) prefix 𝐿 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 0 , 𝐿 ⟩ ) )
5 fznn0sub ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
6 5 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
7 0elfz ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )
8 6 7 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )
9 8 anim1i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 0 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) )
10 swrdswrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 0 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 𝑀 + 0 ) , ( 𝑀 + 𝐿 ) ⟩ ) ) )
11 10 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 0 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 𝑀 + 0 ) , ( 𝑀 + 𝐿 ) ⟩ ) )
12 9 11 syldan ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 𝑀 + 0 ) , ( 𝑀 + 𝐿 ) ⟩ ) )
13 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
14 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
15 14 addid1d ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 0 ) = 𝑀 )
16 13 15 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 + 0 ) = 𝑀 )
17 16 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 + 0 ) = 𝑀 )
18 17 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 0 ) = 𝑀 )
19 18 opeq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ⟨ ( 𝑀 + 0 ) , ( 𝑀 + 𝐿 ) ⟩ = ⟨ 𝑀 , ( 𝑀 + 𝐿 ) ⟩ )
20 19 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑊 substr ⟨ ( 𝑀 + 0 ) , ( 𝑀 + 𝐿 ) ⟩ ) = ( 𝑊 substr ⟨ 𝑀 , ( 𝑀 + 𝐿 ) ⟩ ) )
21 4 12 20 3eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) prefix 𝐿 ) = ( 𝑊 substr ⟨ 𝑀 , ( 𝑀 + 𝐿 ) ⟩ ) )
22 21 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝐿 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) prefix 𝐿 ) = ( 𝑊 substr ⟨ 𝑀 , ( 𝑀 + 𝐿 ) ⟩ ) ) )