Metamath Proof Explorer

Theorem redwlklem

Description: Lemma for redwlk . (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

		Ref	Expression
	Assertion	redwlklem	$⊢ (F \in Word S \land 1 \leq \|F\| \land P : (0 \dots \|F\|) ⟶ V) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ V$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((F \in Word S \land 1 \leq \|F\|) \land P : (0 \dots \|F\|) ⟶ V) \to P : (0 \dots \|F\|) ⟶ V$
2		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
3		fssres	$⊢ (P : (0 \dots \|F\|) ⟶ V \land (0 ..^\|F\|) \subseteq (0 \dots \|F\|)) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 ..^\|F\|) ⟶ V$
4	1 2 3	sylancl	$⊢ ((F \in Word S \land 1 \leq \|F\|) \land P : (0 \dots \|F\|) ⟶ V) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 ..^\|F\|) ⟶ V$
5	4	ex	$⊢ (F \in Word S \land 1 \leq \|F\|) \to (P : (0 \dots \|F\|) ⟶ V \to ({P ↾}_{(0 ..^\|F\|)}) : (0 ..^\|F\|) ⟶ V)$
6		lencl	$⊢ F \in Word S \to \|F\| \in ℕ_{0}$
7	6	nn0zd	$⊢ F \in Word S \to \|F\| \in ℤ$
8		fzoval	$⊢ \|F\| \in ℤ \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
9	7 8	syl	$⊢ F \in Word S \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
10	9	adantr	$⊢ (F \in Word S \land 1 \leq \|F\|) \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
11		wrdred1hash	$⊢ (F \in Word S \land 1 \leq \|F\|) \to \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1$
12		oveq2	$⊢ \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1 \to (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) = (0 \dots \|F\| - 1)$
13	12	eqeq2d	$⊢ \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1 \to ((0 ..^\|F\|) = (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) \leftrightarrow (0 ..^\|F\|) = (0 \dots \|F\| - 1))$
14	11 13	syl	$⊢ (F \in Word S \land 1 \leq \|F\|) \to ((0 ..^\|F\|) = (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) \leftrightarrow (0 ..^\|F\|) = (0 \dots \|F\| - 1))$
15	10 14	mpbird	$⊢ (F \in Word S \land 1 \leq \|F\|) \to (0 ..^\|F\|) = (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|)$
16	15	feq2d	$⊢ (F \in Word S \land 1 \leq \|F\|) \to (({P ↾}_{(0 ..^\|F\|)}) : (0 ..^\|F\|) ⟶ V \leftrightarrow ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ V)$
17	5 16	sylibd	$⊢ (F \in Word S \land 1 \leq \|F\|) \to (P : (0 \dots \|F\|) ⟶ V \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ V)$
18	17	3impia	$⊢ (F \in Word S \land 1 \leq \|F\| \land P : (0 \dots \|F\|) ⟶ V) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ V$