Metamath Proof Explorer

Theorem pfxmpt

Description: Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxmpt ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑆 ‘ 𝑥 ) ) )

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 simpl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑆 ∈ Word 𝐴 )
5 1 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐿 ∈ ℕ0 )
6 0elfz ⊢ ( 𝐿 ∈ ℕ0 → 0 ∈ ( 0 ... 𝐿 ) )
7 5 6 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 0 ∈ ( 0 ... 𝐿 ) )
8 simpr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
9 swrdval2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 0 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 0 ) ) ) )
10 4 7 8 9 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 0 ) ) ) )
11 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
12 11 subid1d ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 − 0 ) = 𝐿 )
13 1 12 syl ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( 𝐿 − 0 ) = 𝐿 )
14 13 oveq2d ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( 0 ..^ ( 𝐿 − 0 ) ) = ( 0 ..^ 𝐿 ) )
15 14 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 0 ..^ ( 𝐿 − 0 ) ) = ( 0 ..^ 𝐿 ) )
16 elfzonn0 ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) → 𝑥 ∈ ℕ0 )
17 nn0cn ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
18 17 addid1d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 0 ) = 𝑥 )
19 16 18 syl ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) → ( 𝑥 + 0 ) = 𝑥 )
20 19 fveq2d ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) → ( 𝑆 ‘ ( 𝑥 + 0 ) ) = ( 𝑆 ‘ 𝑥 ) )
21 20 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ) → ( 𝑆 ‘ ( 𝑥 + 0 ) ) = ( 𝑆 ‘ 𝑥 ) )
22 15 21 mpteq12dva ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 0 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 0 ) ) ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑆 ‘ 𝑥 ) ) )
23 3 10 22 3eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑆 ‘ 𝑥 ) ) )