Metamath Proof Explorer


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 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = ( 𝑊𝐼 ) )