ccat2s1fvwOLD

Description: Obsolete version of ccat2s1fvw as of 28-Jan-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	ccat2s1fvwOLD	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = W (I)$

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1assOLD	$⊢ (W \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
2	1	3expb	$⊢ (W \in Word V \land (X \in V \land Y \in V)) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
3	2	3ad2antl1	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
4	3	fveq1d	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I)$
5		simpl1	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to W \in Word V$
6		ccat2s1cl	$⊢ (X \in V \land Y \in V) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
7	6	adantl	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \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	26	adantr	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to I \in (0 ..^\|W\|)$
28		ccatval1	$⊢ (W \in Word V \land ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V \land I \in (0 ..^\|W\|)) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I) = W (I)$
29	5 7 27 28	syl3anc	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) (I) = W (I)$
30	4 29	eqtrd	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = W (I)$

Metamath Proof Explorer

Theorem ccat2s1fvwOLD

Proof