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

Metamath Proof Explorer

Theorem ccat2s1fvw

Description: Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018) (Revised by AV, 13-Jan-2020) (Proof shortened by AV, 1-May-2020) (Revised by AV, 28-Jan-2024)

Ref Expression
Assertion ccat2s1fvw ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 ccatw2s1ass ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
2 1 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
3 2 fveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) ‘ 𝐼 ) )
4 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑉 )
5 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
6 ccatws1clv ⊢ ( ⟨“ 𝑋 ”⟩ ∈ Word V → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word V )
7 5 6 mp1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word V )
8 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℕ0 )
9 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10 9 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
11 nn0ge0 ⊢ ( 𝐼 ∈ ℕ0 → 0 ≤ 𝐼 )
12 11 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 0 ≤ 𝐼 )
13 0red ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 0 ∈ ℝ )
14 nn0re ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
15 14 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℝ )
16 9 nn0red ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
18 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 0 ≤ 𝐼 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) )
19 13 15 17 18 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( ( 0 ≤ 𝐼 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) )
20 12 19 mpand ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 < ( ♯ ‘ 𝑊 ) → 0 < ( ♯ ‘ 𝑊 ) ) )
21 20 3impia ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
22 elnnnn0b ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
23 10 21 22 sylanbrc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
24 simp3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 < ( ♯ ‘ 𝑊 ) )
25 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
26 8 23 24 25 syl3anbrc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 ccatval1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word V ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
28 4 7 26 27 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
29 3 28 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )