Theorem ccats1val1

Description: Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by JJ, 20-Jan-2024)

	Ref	Expression
Assertion	ccats1val1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		s1cli	⊢ ⟨“ 𝑆 ”⟩ ∈ Word V
2		ccatval1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word V ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
3	1 2	mp3an2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )