Theorem ccats1val1OLD

Description: Obsolete version of ccats1val1 as of 20-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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