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

Metamath Proof Explorer

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 Word A \to S prefix L = S substr ⟨0, L⟩$

Proof

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