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𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝐼 ) = ( 𝑊𝐼 ) )