Theorem cats1fv

Description: A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
	cats1cli.2	⊢ 𝑆 ∈ Word V
	cats1fvn.3	⊢ ( ♯ ‘ 𝑆 ) = 𝑀
	cats1fv.4	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑆 ‘ 𝑁 ) = 𝑌 )
	cats1fv.5	⊢ 𝑁 ∈ ℕ0
	cats1fv.6	⊢ 𝑁 < 𝑀
Assertion	cats1fv	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑇 ‘ 𝑁 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2		cats1cli.2	⊢ 𝑆 ∈ Word V
3		cats1fvn.3	⊢ ( ♯ ‘ 𝑆 ) = 𝑀
4		cats1fv.4	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑆 ‘ 𝑁 ) = 𝑌 )
5		cats1fv.5	⊢ 𝑁 ∈ ℕ0
6		cats1fv.6	⊢ 𝑁 < 𝑀
7	1	fveq1i	⊢ ( 𝑇 ‘ 𝑁 ) = ( ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 )
8		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
9		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10	5 9	eleqtri	⊢ 𝑁 ∈ ( ℤ≥ ‘ 0 )
11		lencl	⊢ ( 𝑆 ∈ Word V → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
12		nn0z	⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
13	2 11 12	mp2b	⊢ ( ♯ ‘ 𝑆 ) ∈ ℤ
14	6 3	breqtrri	⊢ 𝑁 < ( ♯ ‘ 𝑆 )
15		elfzo2	⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ∧ 𝑁 < ( ♯ ‘ 𝑆 ) ) )
16	10 13 14 15	mpbir3an	⊢ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) )
17		ccatval1	⊢ ( ( 𝑆 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 ) )
18	2 8 16 17	mp3an	⊢ ( ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 )
19	7 18	eqtri	⊢ ( 𝑇 ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 )
20	19 4	syl5eq	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑇 ‘ 𝑁 ) = 𝑌 )