Theorem pfxval

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

	Ref	Expression
Assertion	pfxval	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$

Proof

Step	Hyp	Ref	Expression
1		df-pfx	$$⊢\mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$
2	1	a1i	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to \mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$
3		simpl	$$⊢\left(s=S\wedge l=L\right)\to s=S$$
4		opeq2	$$⊢l=L\to ⟨0,l⟩=⟨0,L⟩$$
5	4	adantl	$$⊢\left(s=S\wedge l=L\right)\to ⟨0,l⟩=⟨0,L⟩$$
6	3 5	oveq12d	$$⊢\left(s=S\wedge l=L\right)\to s\mathrm{substr}⟨0,l⟩=S\mathrm{substr}⟨0,L⟩$$
7	6	adantl	$$⊢\left(\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\wedge \left(s=S\wedge l=L\right)\right)\to s\mathrm{substr}⟨0,l⟩=S\mathrm{substr}⟨0,L⟩$$
8		elex	$$⊢S\in V\to S\in \mathrm{V}$$
9	8	adantr	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to S\in \mathrm{V}$$
10		simpr	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to L\in {\mathbb{N}}_0$$
11		ovexd	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{substr}⟨0,L⟩\in \mathrm{V}$$
12	2 7 9 10 11	ovmpod	$$⊢\left(S\in V\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$