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 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