Metamath Proof Explorer

Theorem 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 ∈ Word S ∧ N ∈ 0 … W → ∃ v ∈ Word S W = W ↾ 0 ..^ N ++ v

Proof

Step Hyp Ref Expression
1 swrdcl ⊢ W ∈ Word S → W substr N W ∈ Word S
2 simpr ⊢ W ∈ Word S ∧ N ∈ 0 … W → N ∈ 0 … W
3 elfzuz2 ⊢ N ∈ 0 … W → W ∈ ℤ ≥ 0
4 eluzfz2 ⊢ W ∈ ℤ ≥ 0 → W ∈ 0 … W
5 2 3 4 3syl ⊢ W ∈ Word S ∧ N ∈ 0 … W → W ∈ 0 … W
6 ccatpfx ⊢ W ∈ Word S ∧ N ∈ 0 … W ∧ W ∈ 0 … W → W prefix N ++ W substr N W = W prefix W
7 5 6 mpd3an3 ⊢ W ∈ Word S ∧ N ∈ 0 … W → W prefix N ++ W substr N W = W prefix W
8 pfxres ⊢ W ∈ Word S ∧ N ∈ 0 … W → W prefix N = W ↾ 0 ..^ N
9 8 oveq1d ⊢ W ∈ Word S ∧ N ∈ 0 … W → W prefix N ++ W substr N W = W ↾ 0 ..^ N ++ W substr N W
10 pfxid ⊢ W ∈ Word S → W prefix W = W
11 10 adantr ⊢ W ∈ Word S ∧ N ∈ 0 … W → W prefix W = W
12 7 9 11 3eqtr3rd ⊢ W ∈ Word S ∧ N ∈ 0 … W → W = W ↾ 0 ..^ N ++ W substr N W
13 oveq2 ⊢ v = W substr N W → W ↾ 0 ..^ N ++ v = W ↾ 0 ..^ N ++ W substr N W
14 13 rspceeqv ⊢ W substr N W ∈ Word S ∧ W = W ↾ 0 ..^ N ++ W substr N W → ∃ v ∈ Word S W = W ↾ 0 ..^ N ++ v
15 1 12 14 syl2an2r ⊢ W ∈ Word S ∧ N ∈ 0 … W → ∃ v ∈ Word S W = W ↾ 0 ..^ N ++ v