Theorem addlenrevpfx

Description: The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 3-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		swrdrlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝑀 ) )
2		pfxlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 )
3	1 2	oveq12d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) = ( ( ( ♯ ‘ 𝑊 ) − 𝑀 ) + 𝑀 ) )
4		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5		elfzelz	⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑀 ∈ ℤ )
6		nn0cn	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
7		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8		npcan	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑀 ) + 𝑀 ) = ( ♯ ‘ 𝑊 ) )
9	6 7 8	syl2an	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑀 ) + 𝑀 ) = ( ♯ ‘ 𝑊 ) )
10	4 5 9	syl2an	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑀 ) + 𝑀 ) = ( ♯ ‘ 𝑊 ) )
11	3 10	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) = ( ♯ ‘ 𝑊 ) )