ccat2s1fvwALTOLD

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

		Ref	Expression
	Assertion	ccat2s1fvwALTOLD	$⊢ ((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		simp1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to W \in Word V$
2	1	anim1i	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to (W \in Word V \land (X \in V \land Y \in V))$
3		3anass	$⊢ (W \in Word V \land X \in V \land Y \in V) \leftrightarrow (W \in Word V \land (X \in V \land Y \in V))$
4	2 3	sylibr	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to (W \in Word V \land X \in V \land Y \in V)$
5		ccatw2s1ccatws2OLD	$⊢ (W \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ ⟨“ X Y ”⟩$
6	5	fveq1d	$⊢ (W \in Word V \land X \in V \land Y \in V) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (I) = (W ++ ⟨“ X Y ”⟩) (I)$
7	4 6	syl	$⊢ ((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)$
8	1	adantr	$⊢ ((W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \land (X \in V \land Y \in V)) \to W \in Word V$
9		s2cl	$⊢ (X \in V \land Y \in V) \to ⟨“ X Y ”⟩ \in Word V$
10	9	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$
11		simp2	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in ℕ_{0}$
12		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
13	12	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
14	13	3ad2ant1	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to \|W\| \in ℤ$
15		simp3	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I < \|W\|$
16		elfzo0z	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℤ \land I < \|W\|)$
17	11 14 15 16	syl3anbrc	$⊢ (W \in Word V \land I \in ℕ_{0} \land I < \|W\|) \to I \in (0 ..^\|W\|)$
18	17	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\|)$
19		ccatval1	$⊢ (W \in Word V \land ⟨“ X Y ”⟩ \in Word V \land I \in (0 ..^\|W\|)) \to (W ++ ⟨“ X Y ”⟩) (I) = W (I)$
20	8 10 18 19	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)$
21	7 20	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 ccat2s1fvwALTOLD

Proof