wrdsplex

Description: Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018) (Proof shortened by AV, 3-Nov-2022)

		Ref	Expression
	Assertion	wrdsplex	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to \exists v \in Word S W = ({W ↾}_{(0 ..^N)}) ++ v$

Step	Hyp	Ref	Expression
1		swrdcl	$⊢ W \in Word S \to W substr ⟨N, \|W\|⟩ \in Word S$
2		simpr	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to N \in (0 \dots \|W\|)$
3		elfzuz2	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq 0}$
4		eluzfz2	$⊢ \|W\| \in ℤ_{\geq 0} \to \|W\| \in (0 \dots \|W\|)$
5	2 3 4	3syl	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to \|W\| \in (0 \dots \|W\|)$
6		ccatpfx	$⊢ (W \in Word S \land N \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to (W prefix N) ++ (W substr ⟨N, \|W\|⟩) = W prefix \|W\|$
7	5 6	mpd3an3	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to (W prefix N) ++ (W substr ⟨N, \|W\|⟩) = W prefix \|W\|$
8		pfxres	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to W prefix N = {W ↾}_{(0 ..^N)}$
9	8	oveq1d	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to (W prefix N) ++ (W substr ⟨N, \|W\|⟩) = ({W ↾}_{(0 ..^N)}) ++ (W substr ⟨N, \|W\|⟩)$
10		pfxid	$⊢ W \in Word S \to W prefix \|W\| = W$
11	10	adantr	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to W prefix \|W\| = W$
12	7 9 11	3eqtr3rd	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to W = ({W ↾}_{(0 ..^N)}) ++ (W substr ⟨N, \|W\|⟩)$
13		oveq2	$⊢ v = W substr ⟨N, \|W\|⟩ \to ({W ↾}_{(0 ..^N)}) ++ v = ({W ↾}_{(0 ..^N)}) ++ (W substr ⟨N, \|W\|⟩)$
14	13	rspceeqv	$⊢ (W substr ⟨N, \|W\|⟩ \in Word S \land W = ({W ↾}_{(0 ..^N)}) ++ (W substr ⟨N, \|W\|⟩)) \to \exists v \in Word S W = ({W ↾}_{(0 ..^N)}) ++ v$
15	1 12 14	syl2an2r	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to \exists v \in Word S W = ({W ↾}_{(0 ..^N)}) ++ v$

Metamath Proof Explorer