This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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