Metamath Proof Explorer


Theorem ccat2s1len

Description: The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 14-Jan-2024)

Ref Expression
Assertion ccat2s1len ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2

Proof

Step Hyp Ref Expression
1 s1cli ⟨“ 𝑋 ”⟩ ∈ Word V
2 s1cli ⟨“ 𝑌 ”⟩ ∈ Word V
3 ccatlen ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) )
4 s1len ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
5 s1len ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) = 1
6 4 5 oveq12i ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = ( 1 + 1 )
7 1p1e2 ( 1 + 1 ) = 2
8 6 7 eqtri ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = 2
9 3 8 eqtrdi ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2 )
10 1 2 9 mp2an ( ♯ ‘ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = 2