ccat2s1fvwALT

Description: Alternate proof of ccat2s1fvw using words of length 2, see df-s2 . A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 28-Jan-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ccatws2	$⊢ W \in Word V \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ ⟨“ X Y ”⟩$
2	1	fveq1d	$⊢ W \in Word V \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = (W ++ ⟨“ X Y ”⟩) (I)$
3	2	3ad2ant1	$⊢ (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		s2cli	$⊢ ⟨“ X Y ”⟩ \in Word V$
6	5	a1i	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ⟨“ X Y ”⟩ \in Word V$
7		simp2	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in ℕ_{0}$
8		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
9	8	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
10	9	3ad2ant1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to \|W\| \in ℤ$
11		simp3	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I < \|W\|$
12		elfzo0z	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℤ \land I < \|W\|)$
13	7 10 11 12	syl3anbrc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in (0 ..^\|W\|)$
14		ccatval1	$⊢ (W \in Word V \land ⟨“ X Y ”⟩ \in Word V \land I \in (0 ..^\|W\|)) \to (W ++ ⟨“ X Y ”⟩) (I) = W (I)$
15	4 6 13 14	syl3anc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to (W ++ ⟨“ X Y ”⟩) (I) = W (I)$
16	3 15	eqtrd	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = W (I)$

Metamath Proof Explorer

Theorem ccat2s1fvwALT

Proof