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