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 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W prefix L ⁡ I = W ⁡ I

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ L ∈ 0 … W → L ∈ ℕ 0
2 pfxval ⊢ W ∈ Word V ∧ L ∈ ℕ 0 → W prefix L = W substr 0 L
3 1 2 sylan2 ⊢ W ∈ Word V ∧ L ∈ 0 … W → W prefix L = W substr 0 L
4 3 3adant3 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W prefix L = W substr 0 L
5 4 fveq1d ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W prefix L ⁡ I = W substr 0 L ⁡ I
6 simp1 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W ∈ Word V
7 0elfz ⊢ L ∈ ℕ 0 → 0 ∈ 0 … L
8 1 7 syl ⊢ L ∈ 0 … W → 0 ∈ 0 … L
9 8 3ad2ant2 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → 0 ∈ 0 … L
10 simp2 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → L ∈ 0 … W
11 1 nn0cnd ⊢ L ∈ 0 … W → L ∈ ℂ
12 11 subid1d ⊢ L ∈ 0 … W → L − 0 = L
13 12 eqcomd ⊢ L ∈ 0 … W → L = L − 0
14 13 oveq2d ⊢ L ∈ 0 … W → 0 ..^ L = 0 ..^ L − 0
15 14 eleq2d ⊢ L ∈ 0 … W → I ∈ 0 ..^ L ↔ I ∈ 0 ..^ L − 0
16 15 biimpd ⊢ L ∈ 0 … W → I ∈ 0 ..^ L → I ∈ 0 ..^ L − 0
17 16 a1i ⊢ W ∈ Word V → L ∈ 0 … W → I ∈ 0 ..^ L → I ∈ 0 ..^ L − 0
18 17 3imp ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → I ∈ 0 ..^ L − 0
19 swrdfv ⊢ W ∈ Word V ∧ 0 ∈ 0 … L ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L − 0 → W substr 0 L ⁡ I = W ⁡ I + 0
20 6 9 10 18 19 syl31anc ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W substr 0 L ⁡ I = W ⁡ I + 0
21 elfzoelz ⊢ I ∈ 0 ..^ L → I ∈ ℤ
22 21 zcnd ⊢ I ∈ 0 ..^ L → I ∈ ℂ
23 22 addridd ⊢ I ∈ 0 ..^ L → I + 0 = I
24 23 3ad2ant3 ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → I + 0 = I
25 24 fveq2d ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W ⁡ I + 0 = W ⁡ I
26 5 20 25 3eqtrd ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ I ∈ 0 ..^ L → W prefix L ⁡ I = W ⁡ I