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

Metamath Proof Explorer

Theorem cats1fvn

Description: The last symbol of a 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
Assertion cats1fvn ⊢ X ∈ V → T ⁡ M = X

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cli.2 ⊢ S ∈ Word V
3 cats1fvn.3 ⊢ S = M
4 3 oveq2i ⊢ 0 + S = 0 + M
5 lencl ⊢ S ∈ Word V → S ∈ ℕ 0
6 2 5 ax-mp ⊢ S ∈ ℕ 0
7 3 6 eqeltrri ⊢ M ∈ ℕ 0
8 7 nn0cni ⊢ M ∈ ℂ
9 8 addlidi ⊢ 0 + M = M
10 4 9 eqtr2i ⊢ M = 0 + S
11 1 10 fveq12i ⊢ T ⁡ M = S ++ ⟨“ X ”⟩ ⁡ 0 + S
12 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
13 s1len ⊢ ⟨“ X ”⟩ = 1
14 1nn ⊢ 1 ∈ ℕ
15 13 14 eqeltri ⊢ ⟨“ X ”⟩ ∈ ℕ
16 lbfzo0 ⊢ 0 ∈ 0 ..^ ⟨“ X ”⟩ ↔ ⟨“ X ”⟩ ∈ ℕ
17 15 16 mpbir ⊢ 0 ∈ 0 ..^ ⟨“ X ”⟩
18 ccatval3 ⊢ S ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V ∧ 0 ∈ 0 ..^ ⟨“ X ”⟩ → S ++ ⟨“ X ”⟩ ⁡ 0 + S = ⟨“ X ”⟩ ⁡ 0
19 2 12 17 18 mp3an ⊢ S ++ ⟨“ X ”⟩ ⁡ 0 + S = ⟨“ X ”⟩ ⁡ 0
20 11 19 eqtri ⊢ T ⁡ M = ⟨“ X ”⟩ ⁡ 0
21 s1fv ⊢ X ∈ V → ⟨“ X ”⟩ ⁡ 0 = X
22 20 21 eqtrid ⊢ X ∈ V → T ⁡ M = X