swrdfv2

Description: A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020)

		Ref	Expression
	Assertion	swrdfv2	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to (S substr ⟨F, L⟩) (X - F) = S (X)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to S \in Word V$
2		simpl	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \in ℕ_{0}$
3		eluznn0	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to L \in ℕ_{0}$
4		eluzle	$⊢ L \in ℤ_{\geq F} \to F \leq L$
5	4	adantl	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \leq L$
6	2 3 5	3jca	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
7	6	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
8		elfz2nn0	$⊢ F \in (0 \dots L) \leftrightarrow (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
9	7 8	sylibr	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to F \in (0 \dots L)$
10	3	anim1i	$⊢ ((F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (L \in ℕ_{0} \land L \leq \|S\|)$
11	10	3adant1	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (L \in ℕ_{0} \land L \leq \|S\|)$
12		lencl	$⊢ S \in Word V \to \|S\| \in ℕ_{0}$
13	12	3ad2ant1	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to \|S\| \in ℕ_{0}$
14		fznn0	$⊢ \|S\| \in ℕ_{0} \to (L \in (0 \dots \|S\|) \leftrightarrow (L \in ℕ_{0} \land L \leq \|S\|))$
15	13 14	syl	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (L \in (0 \dots \|S\|) \leftrightarrow (L \in ℕ_{0} \land L \leq \|S\|))$
16	11 15	mpbird	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L \in (0 \dots \|S\|)$
17	1 9 16	3jca	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (S \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|S\|))$
18	17	adantr	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to (S \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|S\|))$
19		nn0cn	$⊢ F \in ℕ_{0} \to F \in ℂ$
20		eluzelcn	$⊢ L \in ℤ_{\geq F} \to L \in ℂ$
21		pncan3	$⊢ (F \in ℂ \land L \in ℂ) \to F + L - F = L$
22	19 20 21	syl2an	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F + L - F = L$
23	22	eqcomd	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to L = F + L - F$
24	23	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L = F + L - F$
25	24	oveq2d	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (F ..^L) = (F ..^F + L - F)$
26	25	eleq2d	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (X \in (F ..^L) \leftrightarrow X \in (F ..^F + L - F))$
27	26	biimpa	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to X \in (F ..^F + L - F)$
28		eluzelz	$⊢ L \in ℤ_{\geq F} \to L \in ℤ$
29	28	adantl	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to L \in ℤ$
30		nn0z	$⊢ F \in ℕ_{0} \to F \in ℤ$
31	30	adantr	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \in ℤ$
32	29 31	zsubcld	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to L - F \in ℤ$
33	32	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L - F \in ℤ$
34	33	adantr	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to L - F \in ℤ$
35		fzosubel3	$⊢ (X \in (F ..^F + L - F) \land L - F \in ℤ) \to X - F \in (0 ..^L - F)$
36	27 34 35	syl2anc	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to X - F \in (0 ..^L - F)$
37		swrdfv	$⊢ ((S \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \land X - F \in (0 ..^L - F)) \to (S substr ⟨F, L⟩) (X - F) = S (X - F + F)$
38	18 36 37	syl2anc	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to (S substr ⟨F, L⟩) (X - F) = S (X - F + F)$
39		elfzoelz	$⊢ X \in (F ..^L) \to X \in ℤ$
40	39	zcnd	$⊢ X \in (F ..^L) \to X \in ℂ$
41	19	adantr	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \in ℂ$
42	41	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to F \in ℂ$
43		npcan	$⊢ (X \in ℂ \land F \in ℂ) \to X - F + F = X$
44	40 42 43	syl2anr	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to X - F + F = X$
45	44	fveq2d	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to S (X - F + F) = S (X)$
46	38 45	eqtrd	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \land X \in (F ..^L)) \to (S substr ⟨F, L⟩) (X - F) = S (X)$

Metamath Proof Explorer

Theorem swrdfv2

Proof