Metamath Proof Explorer

Theorem pfxpfx

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

Ref Expression
Assertion pfxpfx ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) prefix 𝐿 ) = ( 𝑊 prefix 𝐿 ) )

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℕ0 )
2 1 anim2i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
3 2 3adant3 ⊢ ( ( 𝑊 ∈ 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 𝑁 ) prefix 𝐿 ) = ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) prefix 𝐿 ) )
7 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝑊 ∈ Word 𝑉 )
8 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
9 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
10 1 9 syl ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ... 𝑁 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ( 0 ... 𝑁 ) )
12 7 8 11 3jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ... 𝑁 ) ) )
13 1 nn0cnd ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℂ )
14 13 subid1d ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑁 − 0 ) = 𝑁 )
15 14 eqcomd ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 = ( 𝑁 − 0 ) )
16 15 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 = ( 𝑁 − 0 ) )
17 16 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( 𝑁 − 0 ) ) )
18 17 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 ∈ ( 0 ... 𝑁 ) ↔ 𝐿 ∈ ( 0 ... ( 𝑁 − 0 ) ) ) )
19 18 biimp3a ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → 𝐿 ∈ ( 0 ... ( 𝑁 − 0 ) ) )
20 pfxswrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ... 𝑁 ) ) → ( 𝐿 ∈ ( 0 ... ( 𝑁 − 0 ) ) → ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , ( 0 + 𝐿 ) ⟩ ) ) )
21 12 19 20 sylc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , ( 0 + 𝐿 ) ⟩ ) )
22 elfznn0 ⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → 𝐿 ∈ ℕ0 )
23 22 nn0cnd ⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → 𝐿 ∈ ℂ )
24 23 addid2d ⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → ( 0 + 𝐿 ) = 𝐿 )
25 24 opeq2d ⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → ⟨ 0 , ( 0 + 𝐿 ) ⟩ = ⟨ 0 , 𝐿 ⟩ )
26 25 oveq2d ⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → ( 𝑊 substr ⟨ 0 , ( 0 + 𝐿 ) ⟩ ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
27 26 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 substr ⟨ 0 , ( 0 + 𝐿 ) ⟩ ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
28 22 anim2i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) )
29 28 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) )
30 pfxval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
31 29 30 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
32 27 31 eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 substr ⟨ 0 , ( 0 + 𝐿 ) ⟩ ) = ( 𝑊 prefix 𝐿 ) )
33 6 21 32 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) prefix 𝐿 ) = ( 𝑊 prefix 𝐿 ) )