swrdwrdsymb

Description: A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022)

		Ref	Expression
	Assertion	swrdwrdsymb	$⊢ S \in Word A \to S substr ⟨M, N⟩ \in Word S [(M ..^N)]$

Proof

Step	Hyp	Ref	Expression
1		swrdval2	$⊢ (S \in Word A \land M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to S substr ⟨M, N⟩ = (x \in (0 ..^N - M) ⟼ S (x + M))$
2	1	3expb	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to S substr ⟨M, N⟩ = (x \in (0 ..^N - M) ⟼ S (x + M))$
3		wrdf	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ A$
4	3	ffund	$⊢ S \in Word A \to Fun S$
5	4	adantr	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to Fun S$
6	5	adantr	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to Fun S$
7		wrddm	$⊢ S \in Word A \to dom S = (0 ..^\|S\|)$
8		elfzodifsumelfzo	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to (x \in (0 ..^N - M) \to x + M \in (0 ..^\|S\|))$
9	8	imp	$⊢ ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \land x \in (0 ..^N - M)) \to x + M \in (0 ..^\|S\|)$
10	9	adantl	$⊢ (dom S = (0 ..^\|S\|) \land ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \land x \in (0 ..^N - M))) \to x + M \in (0 ..^\|S\|)$
11		eleq2	$⊢ dom S = (0 ..^\|S\|) \to (x + M \in dom S \leftrightarrow x + M \in (0 ..^\|S\|))$
12	11	adantr	$⊢ (dom S = (0 ..^\|S\|) \land ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \land x \in (0 ..^N - M))) \to (x + M \in dom S \leftrightarrow x + M \in (0 ..^\|S\|))$
13	10 12	mpbird	$⊢ (dom S = (0 ..^\|S\|) \land ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \land x \in (0 ..^N - M))) \to x + M \in dom S$
14	13	exp32	$⊢ dom S = (0 ..^\|S\|) \to ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to (x \in (0 ..^N - M) \to x + M \in dom S))$
15	7 14	syl	$⊢ S \in Word A \to ((M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to (x \in (0 ..^N - M) \to x + M \in dom S))$
16	15	imp31	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to x + M \in dom S$
17		simpr	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to x \in (0 ..^N - M)$
18		elfzelz	$⊢ N \in (0 \dots \|S\|) \to N \in ℤ$
19	18	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to N \in ℤ$
20	19	adantl	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to N \in ℤ$
21	20	adantr	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to N \in ℤ$
22		elfzelz	$⊢ M \in (0 \dots N) \to M \in ℤ$
23	22	ad2antrl	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to M \in ℤ$
24	23	adantr	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to M \in ℤ$
25		fzoaddel2	$⊢ (x \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to x + M \in (M ..^N)$
26	17 21 24 25	syl3anc	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to x + M \in (M ..^N)$
27		funfvima	$⊢ (Fun S \land x + M \in dom S) \to (x + M \in (M ..^N) \to S (x + M) \in S [(M ..^N)])$
28	27	imp	$⊢ ((Fun S \land x + M \in dom S) \land x + M \in (M ..^N)) \to S (x + M) \in S [(M ..^N)]$
29	6 16 26 28	syl21anc	$⊢ ((S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \land x \in (0 ..^N - M)) \to S (x + M) \in S [(M ..^N)]$
30	29	fmpttd	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to (x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^N - M) ⟶ S [(M ..^N)]$
31		fvex	$⊢ S (x + M) \in V$
32		eqid	$⊢ (x \in (0 ..^N - M) ⟼ S (x + M)) = (x \in (0 ..^N - M) ⟼ S (x + M))$
33	31 32	fnmpti	$⊢ (x \in (0 ..^N - M) ⟼ S (x + M)) Fn (0 ..^N - M)$
34		hashfn	$⊢ (x \in (0 ..^N - M) ⟼ S (x + M)) Fn (0 ..^N - M) \to \|(x \in (0 ..^N - M) ⟼ S (x + M))\| = \|(0 ..^N - M)\|$
35	33 34	mp1i	$⊢ M \in (0 \dots N) \to \|(x \in (0 ..^N - M) ⟼ S (x + M))\| = \|(0 ..^N - M)\|$
36		fznn0sub	$⊢ M \in (0 \dots N) \to N - M \in ℕ_{0}$
37		hashfzo0	$⊢ N - M \in ℕ_{0} \to \|(0 ..^N - M)\| = N - M$
38	36 37	syl	$⊢ M \in (0 \dots N) \to \|(0 ..^N - M)\| = N - M$
39	35 38	eqtrd	$⊢ M \in (0 \dots N) \to \|(x \in (0 ..^N - M) ⟼ S (x + M))\| = N - M$
40	39	oveq2d	$⊢ M \in (0 \dots N) \to (0 ..^\|(x \in (0 ..^N - M) ⟼ S (x + M))\|) = (0 ..^N - M)$
41	40	feq2d	$⊢ M \in (0 \dots N) \to ((x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^\|(x \in (0 ..^N - M) ⟼ S (x + M))\|) ⟶ S [(M ..^N)] \leftrightarrow (x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^N - M) ⟶ S [(M ..^N)])$
42	41	ad2antrl	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to ((x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^\|(x \in (0 ..^N - M) ⟼ S (x + M))\|) ⟶ S [(M ..^N)] \leftrightarrow (x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^N - M) ⟶ S [(M ..^N)])$
43	30 42	mpbird	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to (x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^\|(x \in (0 ..^N - M) ⟼ S (x + M))\|) ⟶ S [(M ..^N)]$
44		iswrdb	$⊢ (x \in (0 ..^N - M) ⟼ S (x + M)) \in Word S [(M ..^N)] \leftrightarrow (x \in (0 ..^N - M) ⟼ S (x + M)) : (0 ..^\|(x \in (0 ..^N - M) ⟼ S (x + M))\|) ⟶ S [(M ..^N)]$
45	43 44	sylibr	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to (x \in (0 ..^N - M) ⟼ S (x + M)) \in Word S [(M ..^N)]$
46	2 45	eqeltrd	$⊢ (S \in Word A \land (M \in (0 \dots N) \land N \in (0 \dots \|S\|))) \to S substr ⟨M, N⟩ \in Word S [(M ..^N)]$
47	46	expcom	$⊢ (M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to (S \in Word A \to S substr ⟨M, N⟩ \in Word S [(M ..^N)])$
48		swrdnd0	$⊢ S \in Word A \to (\neg (M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to S substr ⟨M, N⟩ = \emptyset)$
49		wrd0	$⊢ \emptyset \in Word S [(M ..^N)]$
50		eleq1	$⊢ S substr ⟨M, N⟩ = \emptyset \to (S substr ⟨M, N⟩ \in Word S [(M ..^N)] \leftrightarrow \emptyset \in Word S [(M ..^N)])$
51	49 50	mpbiri	$⊢ S substr ⟨M, N⟩ = \emptyset \to S substr ⟨M, N⟩ \in Word S [(M ..^N)]$
52	48 51	syl6com	$⊢ \neg (M \in (0 \dots N) \land N \in (0 \dots \|S\|)) \to (S \in Word A \to S substr ⟨M, N⟩ \in Word S [(M ..^N)])$
53	47 52	pm2.61i	$⊢ S \in Word A \to S substr ⟨M, N⟩ \in Word S [(M ..^N)]$

Metamath Proof Explorer

Theorem swrdwrdsymb

Proof