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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑌 ∈ 𝑉 → ( 𝑇 ‘ 𝑁 ) = 𝑌 )