elfzelfzccat

Description: An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018)

		Ref	Expression
	Assertion	elfzelfzccat	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A\|) \to N \in (0 \dots \|A ++ B\|))$

Proof

Step	Hyp	Ref	Expression
1		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
2		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
3		elfz0add	$⊢ (\|A\| \in ℕ_{0} \land \|B\| \in ℕ_{0}) \to (N \in (0 \dots \|A\|) \to N \in (0 \dots \|A\| + \|B\|))$
4	1 2 3	syl2an	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A\|) \to N \in (0 \dots \|A\| + \|B\|))$
5		ccatlen	$⊢ (A \in Word V \land B \in Word V) \to \|A ++ B\| = \|A\| + \|B\|$
6	5	oveq2d	$⊢ (A \in Word V \land B \in Word V) \to (0 \dots \|A ++ B\|) = (0 \dots \|A\| + \|B\|)$
7	6	eleq2d	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A ++ B\|) \leftrightarrow N \in (0 \dots \|A\| + \|B\|))$
8	4 7	sylibrd	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A\|) \to N \in (0 \dots \|A ++ B\|))$

Metamath Proof Explorer

Theorem elfzelfzccat

Proof