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	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = W (I)$

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ass	$⊢ W \in Word V \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
2	1	3ad2ant1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
3	2	fveq1d	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I)$
4		simp1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to W \in Word V$
5		s1cli	$⊢ ⟨“ X ”⟩ \in Word V$
6		ccatws1clv	$⊢ ⟨“ X ”⟩ \in Word V \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
7	5 6	mp1i	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
8		simp2	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in ℕ_{0}$
9		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
10	9	3ad2ant1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to \|W\| \in ℕ_{0}$
11		nn0ge0	$⊢ I \in ℕ_{0} \to 0 \leq I$
12	11	adantl	$⊢ (W \in Word V \land I \in ℕ_{0}) \to 0 \leq I$
13		0red	$⊢ (W \in Word V \land I \in ℕ_{0}) \to 0 \in ℝ$
14		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
15	14	adantl	$⊢ (W \in Word V \land I \in ℕ_{0}) \to I \in ℝ$
16	9	nn0red	$⊢ W \in Word V \to \|W\| \in ℝ$
17	16	adantr	$⊢ (W \in Word V \land I \in ℕ_{0}) \to \|W\| \in ℝ$
18		lelttr	$⊢ (0 \in ℝ \land I \in ℝ \land \|W\| \in ℝ) \to ((0 \leq I \land I < \|W\|) \to 0 < \|W\|)$
19	13 15 17 18	syl3anc	$⊢ (W \in Word V \land I \in ℕ_{0}) \to ((0 \leq I \land I < \|W\|) \to 0 < \|W\|)$
20	12 19	mpand	$⊢ (W \in Word V \land I \in ℕ_{0}) \to (I < \|W\| \to 0 < \|W\|)$
21	20	3impia	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to 0 < \|W\|$
22		elnnnn0b	$⊢ \|W\| \in ℕ \leftrightarrow (\|W\| \in ℕ_{0} \land 0 < \|W\|)$
23	10 21 22	sylanbrc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to \|W\| \in ℕ$
24		simp3	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I < \|W\|$
25		elfzo0	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|)$
26	8 23 24 25	syl3anbrc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in (0 ..^\|W\|)$
27		ccatval1	$⊢ (W \in Word V \land ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V \land I \in (0 ..^\|W\|)) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I) = W (I)$
28	4 7 26 27	syl3anc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I) = W (I)$
29	3 28	eqtrd	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = W (I)$

Metamath Proof Explorer

Theorem ccat2s1fvw

Proof