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 , 𝐿 ⟩ ) )