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 addid2i ( 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 ( 𝑋𝑉 → ( 𝑇𝑀 ) = 𝑋 )