swrdfv0

Description: The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022)

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

Step	Hyp	Ref	Expression
1		elfzofz	$⊢ F \in (0 ..^L) \to F \in (0 \dots L)$
2	1	3anim2i	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|))$
3		fzonnsub	$⊢ F \in (0 ..^L) \to L - F \in ℕ$
4	3	3ad2ant2	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to L - F \in ℕ$
5		lbfzo0	$⊢ 0 \in (0 ..^L - F) \leftrightarrow L - F \in ℕ$
6	4 5	sylibr	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to 0 \in (0 ..^L - F)$
7		swrdfv	$⊢ ((S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \land 0 \in (0 ..^L - F)) \to (S substr ⟨F, L⟩) (0) = S (0 + F)$
8	2 6 7	syl2anc	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to (S substr ⟨F, L⟩) (0) = S (0 + F)$
9		elfzoelz	$⊢ F \in (0 ..^L) \to F \in ℤ$
10	9	zcnd	$⊢ F \in (0 ..^L) \to F \in ℂ$
11	10	addid2d	$⊢ F \in (0 ..^L) \to 0 + F = F$
12	11	fveq2d	$⊢ F \in (0 ..^L) \to S (0 + F) = S (F)$
13	12	3ad2ant2	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to S (0 + F) = S (F)$
14	8 13	eqtrd	$⊢ (S \in Word A \land F \in (0 ..^L) \land L \in (0 \dots \|S\|)) \to (S substr ⟨F, L⟩) (0) = S (F)$

Metamath Proof Explorer