Metamath Proof Explorer

Theorem pfxfv

Description: A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxfv ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ0 )
2 pfxval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
3 1 2 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
4 3 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) )
5 4 fveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 𝐼 ) = ( ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) ‘ 𝐼 ) )
6 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → 𝑊 ∈ Word 𝑉 )
7 0elfz ⊢ ( 𝐿 ∈ ℕ0 → 0 ∈ ( 0 ... 𝐿 ) )
8 1 7 syl ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ... 𝐿 ) )
9 8 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → 0 ∈ ( 0 ... 𝐿 ) )
10 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
11 1 nn0cnd ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℂ )
12 11 subid1d ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐿 − 0 ) = 𝐿 )
13 12 eqcomd ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 = ( 𝐿 − 0 ) )
14 13 oveq2d ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ 𝐿 ) = ( 0 ..^ ( 𝐿 − 0 ) ) )
15 14 eleq2d ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝐿 ) ↔ 𝐼 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ) )
16 15 biimpd ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝐿 ) → 𝐼 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ) )
17 16 a1i ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝐿 ) → 𝐼 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ) ) )
18 17 3imp ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → 𝐼 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) )
19 swrdfv ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐼 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ) → ( ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ ( 𝐼 + 0 ) ) )
20 6 9 10 18 19 syl31anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 substr ⟨ 0 , 𝐿 ⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ ( 𝐼 + 0 ) ) )
21 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐿 ) → 𝐼 ∈ ℤ )
22 21 zcnd ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐿 ) → 𝐼 ∈ ℂ )
23 22 addid1d ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐿 ) → ( 𝐼 + 0 ) = 𝐼 )
24 23 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝐼 + 0 ) = 𝐼 )
25 24 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑊 ‘ ( 𝐼 + 0 ) ) = ( 𝑊 ‘ 𝐼 ) )
26 5 20 25 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )