swrdccatfn

Description: The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018)

		Ref	Expression
	Assertion	swrdccatfn	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$

Step	Hyp	Ref	Expression
1		ccatcl	$⊢ (A \in Word V \land B \in Word V) \to A ++ B \in Word V$
2	1	adantr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to A ++ B \in Word V$
3		simprl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to M \in (0 \dots N)$
4		ccatlen	$⊢ (A \in Word V \land B \in Word V) \to \|A ++ B\| = \|A\| + \|B\|$
5	4	oveq2d	$⊢ (A \in Word V \land B \in Word V) \to (0 \dots \|A ++ B\|) = (0 \dots \|A\| + \|B\|)$
6	5	eleq2d	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A ++ B\|) \leftrightarrow N \in (0 \dots \|A\| + \|B\|))$
7	6	biimpar	$⊢ ((A \in Word V \land B \in Word V) \land N \in (0 \dots \|A\| + \|B\|)) \to N \in (0 \dots \|A ++ B\|)$
8	7	adantrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to N \in (0 \dots \|A ++ B\|)$
9		swrdvalfn	$⊢ (A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|)) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
10	2 3 8 9	syl3anc	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$

Metamath Proof Explorer