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 ⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
cats1cli.2 ⊢ 𝑆 ∈ Word V
cats1fvn.3 ⊢ ( ♯ ‘ 𝑆 ) = 𝑀
Assertion cats1fvn ( 𝑋 ∈ 𝑉 → ( 𝑇 ‘ 𝑀 ) = 𝑋 )

Proof

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