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 ⊢ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
2 s1cli ⊢ ⟨“ Y ”⟩ ∈ Word V
3 ccatlen ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = ⟨“ X ”⟩ + ⟨“ Y ”⟩
4 s1len ⊢ ⟨“ X ”⟩ = 1
5 s1len ⊢ ⟨“ Y ”⟩ = 1
6 4 5 oveq12i ⊢ ⟨“ X ”⟩ + ⟨“ Y ”⟩ = 1 + 1
7 1p1e2 ⊢ 1 + 1 = 2
8 6 7 eqtri ⊢ ⟨“ X ”⟩ + ⟨“ Y ”⟩ = 2
9 3 8 eqtrdi ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2
10 1 2 9 mp2an ⊢ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2