swrdlen

Description: Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015)

		Ref	Expression
	Assertion	swrdlen	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|S substr ⟨F, L⟩\| = L - F$

Step	Hyp	Ref	Expression
1		fvex	$⊢ S (x + F) \in V$
2		eqid	$⊢ (x \in (0 ..^L - F) ⟼ S (x + F)) = (x \in (0 ..^L - F) ⟼ S (x + F))$
3	1 2	fnmpti	$⊢ (x \in (0 ..^L - F) ⟼ S (x + F)) Fn (0 ..^L - F)$
4		swrdval2	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = (x \in (0 ..^L - F) ⟼ S (x + F))$
5	4	fneq1d	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to ((S substr ⟨F, L⟩) Fn (0 ..^L - F) \leftrightarrow (x \in (0 ..^L - F) ⟼ S (x + F)) Fn (0 ..^L - F))$
6	3 5	mpbiri	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to (S substr ⟨F, L⟩) Fn (0 ..^L - F)$
7		hashfn	$⊢ (S substr ⟨F, L⟩) Fn (0 ..^L - F) \to \|S substr ⟨F, L⟩\| = \|(0 ..^L - F)\|$
8	6 7	syl	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|S substr ⟨F, L⟩\| = \|(0 ..^L - F)\|$
9		fznn0sub	$⊢ F \in (0 \dots L) \to L - F \in ℕ_{0}$
10	9	3ad2ant2	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to L - F \in ℕ_{0}$
11		hashfzo0	$⊢ L - F \in ℕ_{0} \to \|(0 ..^L - F)\| = L - F$
12	10 11	syl	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|(0 ..^L - F)\| = L - F$
13	8 12	eqtrd	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|S substr ⟨F, L⟩\| = L - F$

Metamath Proof Explorer