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 ccatws1len
Description: The length of the concatenation of a word with a singleton word.
(Contributed by Alexander van der Vekens , 22-Sep-2018) (Revised by AV , 4-Mar-2022)
Ref
Expression
Assertion
ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1
Proof
Step
Hyp
Ref
Expression
1
s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
2
ccatlen ⊢ W ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → W ++ ⟨“ X ”⟩ = W + ⟨“ X ”⟩
3
1 2
mpan2 ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + ⟨“ X ”⟩
4
s1len ⊢ ⟨“ X ”⟩ = 1
5
4
oveq2i ⊢ W + ⟨“ X ”⟩ = W + 1
6
3 5
eqtrdi ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1