This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxval

Description: Value of a prefix operation. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxval ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )

Proof

Step Hyp Ref Expression
1 df-pfx ⊢ prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )
2 1 a1i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) ) )
3 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑙 = 𝐿 ) → 𝑠 = 𝑆 )
4 opeq2 ⊢ ( 𝑙 = 𝐿 → ⟨ 0 , 𝑙 ⟩ = ⟨ 0 , 𝐿 ⟩ )
5 4 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑙 = 𝐿 ) → ⟨ 0 , 𝑙 ⟩ = ⟨ 0 , 𝐿 ⟩ )
6 3 5 oveq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑙 = 𝐿 ) → ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
7 6 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑙 = 𝐿 ) ) → ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
8 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
9 8 adantr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → 𝑆 ∈ V )
10 simpr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ0 )
11 ovexd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) ∈ V )
12 2 7 9 10 11 ovmpod ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )