Theorem pfxcctswrd

Description: The concatenation of the prefix of a word and the rest of the word yields the word itself. (Contributed by AV, 21-Oct-2018) (Revised by AV, 9-May-2020)

	Ref	Expression
Assertion	pfxcctswrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑀 ) ++ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
2		nn0fz0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
3	1 2	sylib	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4	3	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
5		ccatpfx	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑀 ) ++ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
6	4 5	mpd3an3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑀 ) ++ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) )
7		pfxid	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
8	7	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
9	6 8	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑀 ) ++ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )