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