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 ccat2s1fst
Description: The first symbol of the concatenation of a word with two single symbols.
(Contributed by Alexander van der Vekens , 22-Sep-2018) (Revised by AV , 28-Jan-2024)
Ref
Expression
Assertion
ccat2s1fst ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
Proof
Step
Hyp
Ref
Expression
1
0nn0 ⊢ 0 ∈ ℕ0
2
ccat2s1fvw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
3
1 2
mp3an2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )