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

Metamath Proof Explorer

Theorem cats1len

Description: The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
cats1cli.2 ⊢ S ∈ Word V
cats1fvn.3 ⊢ S = M
cats1len.4 ⊢ M + 1 = N
Assertion cats1len ⊢ T = N

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cli.2 ⊢ S ∈ Word V
3 cats1fvn.3 ⊢ S = M
4 cats1len.4 ⊢ M + 1 = N
5 1 fveq2i ⊢ T = S ++ ⟨“ X ”⟩
6 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
7 ccatlen ⊢ S ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → S ++ ⟨“ X ”⟩ = S + ⟨“ X ”⟩
8 2 6 7 mp2an ⊢ S ++ ⟨“ X ”⟩ = S + ⟨“ X ”⟩
9 s1len ⊢ ⟨“ X ”⟩ = 1
10 3 9 oveq12i ⊢ S + ⟨“ X ”⟩ = M + 1
11 8 10 eqtri ⊢ S ++ ⟨“ X ”⟩ = M + 1
12 11 4 eqtri ⊢ S ++ ⟨“ X ”⟩ = N
13 5 12 eqtri ⊢ T = N