Theorem pfxval0

Description: Value of a prefix operation. This theorem should only be used in proofs if L e. NN0 is not available. Otherwise (and usually), pfxval should be used. (Contributed by AV, 3-Dec-2022) (New usage is discouraged.)

	Ref	Expression
Assertion	pfxval0	$$⊢S\in \mathrm{Word}A\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$

Proof

Step	Hyp	Ref	Expression
1		pfxval	$$⊢\left(S\in \mathrm{Word}A\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$
2		simpr	$$⊢\left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to L\in {\mathbb{N}}_0$$
3	2	con3i	$$⊢\neg L\in {\mathbb{N}}_0\to \neg \left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)$$
4	3	adantl	$$⊢\left(S\in \mathrm{Word}A\wedge \neg L\in {\mathbb{N}}_0\right)\to \neg \left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)$$
5		pfxnndmnd	$$⊢\neg \left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=\varnothing$$
6	4 5	syl	$$⊢\left(S\in \mathrm{Word}A\wedge \neg L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=\varnothing$$
7		simpr	$$⊢\left(0\in {\mathbb{N}}_0\wedge L\in {\mathbb{N}}_0\right)\to L\in {\mathbb{N}}_0$$
8	7	con3i	$$⊢\neg L\in {\mathbb{N}}_0\to \neg \left(0\in {\mathbb{N}}_0\wedge L\in {\mathbb{N}}_0\right)$$
9		swrdnnn0nd	$$⊢\left(S\in \mathrm{Word}A\wedge \neg \left(0\in {\mathbb{N}}_0\wedge L\in {\mathbb{N}}_0\right)\right)\to S\mathrm{substr}⟨0,L⟩=\varnothing$$
10	8 9	sylan2	$$⊢\left(S\in \mathrm{Word}A\wedge \neg L\in {\mathbb{N}}_0\right)\to S\mathrm{substr}⟨0,L⟩=\varnothing$$
11	6 10	eqtr4d	$$⊢\left(S\in \mathrm{Word}A\wedge \neg L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$
12	1 11	pm2.61dan	$$⊢S\in \mathrm{Word}A\to S\mathrm{prefix}L=S\mathrm{substr}⟨0,L⟩$$