Metamath Proof Explorer

Theorem swrdf

Description: A subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 13-Nov-2018)

		Ref	Expression
	Assertion	swrdf	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ V$

Proof

Step	Hyp	Ref	Expression
1		swrdcl	$⊢ W \in Word V \to W substr ⟨M, N⟩ \in Word V$
2		wrdf	$⊢ W substr ⟨M, N⟩ \in Word V \to (W substr ⟨M, N⟩) : (0 ..^\|W substr ⟨M, N⟩\|) ⟶ V$
3	1 2	syl	$⊢ W \in Word V \to (W substr ⟨M, N⟩) : (0 ..^\|W substr ⟨M, N⟩\|) ⟶ V$
4	3	3ad2ant1	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) : (0 ..^\|W substr ⟨M, N⟩\|) ⟶ V$
5		swrdlen	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \|W substr ⟨M, N⟩\| = N - M$
6	5	oveq2d	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (0 ..^\|W substr ⟨M, N⟩\|) = (0 ..^N - M)$
7	6	feq2d	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ((W substr ⟨M, N⟩) : (0 ..^\|W substr ⟨M, N⟩\|) ⟶ V \leftrightarrow (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ V)$
8	4 7	mpbid	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ V$