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	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ∃ 𝑣 ∈ Word 𝑆 𝑊 = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		swrdcl	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑆 )
2		simpr	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
3		elfzuz2	⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) )
4		eluzfz2	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
5	2 3 4	3syl	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
6		ccatpfx	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
7	5 6	mpd3an3	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
8		pfxres	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝑁 ) = ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) )
9	8	oveq1d	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
10		pfxid	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
11	10	adantr	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
12	7 9 11	3eqtr3rd	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
13		oveq2	⊢ ( 𝑣 = ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) → ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑣 ) = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
14	13	rspceeqv	⊢ ( ( ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑆 ∧ 𝑊 = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ ( 𝑊 substr ⟨ 𝑁 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) → ∃ 𝑣 ∈ Word 𝑆 𝑊 = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑣 ) )
15	1 12 14	syl2an2r	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ∃ 𝑣 ∈ Word 𝑆 𝑊 = ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑣 ) )