Metamath Proof Explorer

Theorem ccatw2s1p2

Description: Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020)

		Ref	Expression
	Assertion	ccatw2s1p2	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N + 1) = Y$

Proof

Step	Hyp	Ref	Expression
1		ccatws1cl	$⊢ (W \in Word V \land X \in V) \to W ++ ⟨“ X ”⟩ \in Word V$
2	1	ad2ant2r	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to W ++ ⟨“ X ”⟩ \in Word V$
3		simprr	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to Y \in V$
4		ccatws1len	$⊢ W \in Word V \to \|W ++ ⟨“ X ”⟩\| = \|W\| + 1$
5	4	ad2antrr	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to \|W ++ ⟨“ X ”⟩\| = \|W\| + 1$
6		oveq1	$⊢ \|W\| = N \to \|W\| + 1 = N + 1$
7	6	ad2antlr	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to \|W\| + 1 = N + 1$
8	5 7	eqtr2d	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to N + 1 = \|W ++ ⟨“ X ”⟩\|$
9		ccats1val2	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land Y \in V \land N + 1 = \|W ++ ⟨“ X ”⟩\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N + 1) = Y$
10	2 3 8 9	syl3anc	$⊢ ((W \in Word V \land \|W\| = N) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N + 1) = Y$