This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Words over a set Concatenations with singleton words 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 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )