swrd0

Description: A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018) (Revised by AV, 20-Oct-2018) (Proof shortened by AV, 2-May-2020)

		Ref	Expression
	Assertion	swrd0	$⊢ \emptyset substr ⟨F, L⟩ = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨\emptyset, ⟨F, L⟩⟩ \in (V \times (ℤ \times ℤ)) \leftrightarrow (\emptyset \in V \land ⟨F, L⟩ \in (ℤ \times ℤ))$
2		opelxp	$⊢ ⟨F, L⟩ \in (ℤ \times ℤ) \leftrightarrow (F \in ℤ \land L \in ℤ)$
3		swrdval	$⊢ (\emptyset \in V \land F \in ℤ \land L \in ℤ) \to \emptyset substr ⟨F, L⟩ = if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset)$
4		fzonlt0	$⊢ (F \in ℤ \land L \in ℤ) \to (\neg F < L \leftrightarrow (F ..^L) = \emptyset)$
5	4	biimprd	$⊢ (F \in ℤ \land L \in ℤ) \to ((F ..^L) = \emptyset \to \neg F < L)$
6	5	con2d	$⊢ (F \in ℤ \land L \in ℤ) \to (F < L \to \neg (F ..^L) = \emptyset)$
7	6	impcom	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to \neg (F ..^L) = \emptyset$
8		ss0	$⊢ (F ..^L) \subseteq \emptyset \to (F ..^L) = \emptyset$
9	7 8	nsyl	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to \neg (F ..^L) \subseteq \emptyset$
10		dm0	$⊢ dom \emptyset = \emptyset$
11	10	a1i	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to dom \emptyset = \emptyset$
12	11	sseq2d	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to ((F ..^L) \subseteq dom \emptyset \leftrightarrow (F ..^L) \subseteq \emptyset)$
13	9 12	mtbird	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to \neg (F ..^L) \subseteq dom \emptyset$
14	13	iffalsed	$⊢ (F < L \land (F \in ℤ \land L \in ℤ)) \to if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset) = \emptyset$
15		ssidd	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to \emptyset \subseteq \emptyset$
16	4	biimpac	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to (F ..^L) = \emptyset$
17	10	a1i	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to dom \emptyset = \emptyset$
18	15 16 17	3sstr4d	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to (F ..^L) \subseteq dom \emptyset$
19	18	iftrued	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset) = (x \in (0 ..^L - F) ⟼ \emptyset (x + F))$
20		zre	$⊢ L \in ℤ \to L \in ℝ$
21		zre	$⊢ F \in ℤ \to F \in ℝ$
22		lenlt	$⊢ (L \in ℝ \land F \in ℝ) \to (L \leq F \leftrightarrow \neg F < L)$
23	22	bicomd	$⊢ (L \in ℝ \land F \in ℝ) \to (\neg F < L \leftrightarrow L \leq F)$
24	20 21 23	syl2anr	$⊢ (F \in ℤ \land L \in ℤ) \to (\neg F < L \leftrightarrow L \leq F)$
25		fzo0n	$⊢ (F \in ℤ \land L \in ℤ) \to (L \leq F \leftrightarrow (0 ..^L - F) = \emptyset)$
26	24 25	bitrd	$⊢ (F \in ℤ \land L \in ℤ) \to (\neg F < L \leftrightarrow (0 ..^L - F) = \emptyset)$
27	26	biimpac	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to (0 ..^L - F) = \emptyset$
28	27	mpteq1d	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = (x \in \emptyset ⟼ \emptyset (x + F))$
29	28	dmeqd	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to dom (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = dom (x \in \emptyset ⟼ \emptyset (x + F))$
30		ral0	$⊢ \forall x \in \emptyset \emptyset (x + F) \in V$
31		dmmptg	$⊢ \forall x \in \emptyset \emptyset (x + F) \in V \to dom (x \in \emptyset ⟼ \emptyset (x + F)) = \emptyset$
32	30 31	mp1i	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to dom (x \in \emptyset ⟼ \emptyset (x + F)) = \emptyset$
33	29 32	eqtrd	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to dom (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset$
34		mptrel	$⊢ Rel (x \in (0 ..^L - F) ⟼ \emptyset (x + F))$
35		reldm0	$⊢ Rel (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) \to ((x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset \leftrightarrow dom (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset)$
36	34 35	mp1i	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to ((x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset \leftrightarrow dom (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset)$
37	33 36	mpbird	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to (x \in (0 ..^L - F) ⟼ \emptyset (x + F)) = \emptyset$
38	19 37	eqtrd	$⊢ (\neg F < L \land (F \in ℤ \land L \in ℤ)) \to if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset) = \emptyset$
39	14 38	pm2.61ian	$⊢ (F \in ℤ \land L \in ℤ) \to if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset) = \emptyset$
40	39	3adant1	$⊢ (\emptyset \in V \land F \in ℤ \land L \in ℤ) \to if ((F ..^L) \subseteq dom \emptyset, (x \in (0 ..^L - F) ⟼ \emptyset (x + F)), \emptyset) = \emptyset$
41	3 40	eqtrd	$⊢ (\emptyset \in V \land F \in ℤ \land L \in ℤ) \to \emptyset substr ⟨F, L⟩ = \emptyset$
42	41	3expb	$⊢ (\emptyset \in V \land (F \in ℤ \land L \in ℤ)) \to \emptyset substr ⟨F, L⟩ = \emptyset$
43	2 42	sylan2b	$⊢ (\emptyset \in V \land ⟨F, L⟩ \in (ℤ \times ℤ)) \to \emptyset substr ⟨F, L⟩ = \emptyset$
44	1 43	sylbi	$⊢ ⟨\emptyset, ⟨F, L⟩⟩ \in (V \times (ℤ \times ℤ)) \to \emptyset substr ⟨F, L⟩ = \emptyset$
45		df-substr	$⊢ substr = (s \in V, b \in (ℤ \times ℤ) ⟼ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (z \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (z + 1^{st} (b))), \emptyset))$
46		ovex	$⊢ (0 ..^2^{nd} (b) - 1^{st} (b)) \in V$
47	46	mptex	$⊢ (z \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (z + 1^{st} (b))) \in V$
48		0ex	$⊢ \emptyset \in V$
49	47 48	ifex	$⊢ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (z \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (z + 1^{st} (b))), \emptyset) \in V$
50	45 49	dmmpo	$⊢ dom substr = V \times (ℤ \times ℤ)$
51	44 50	eleq2s	$⊢ ⟨\emptyset, ⟨F, L⟩⟩ \in dom substr \to \emptyset substr ⟨F, L⟩ = \emptyset$
52		df-ov	$⊢ \emptyset substr ⟨F, L⟩ = substr (⟨\emptyset, ⟨F, L⟩⟩)$
53		ndmfv	$⊢ \neg ⟨\emptyset, ⟨F, L⟩⟩ \in dom substr \to substr (⟨\emptyset, ⟨F, L⟩⟩) = \emptyset$
54	52 53	eqtrid	$⊢ \neg ⟨\emptyset, ⟨F, L⟩⟩ \in dom substr \to \emptyset substr ⟨F, L⟩ = \emptyset$
55	51 54	pm2.61i	$⊢ \emptyset substr ⟨F, L⟩ = \emptyset$

Metamath Proof Explorer

Theorem swrd0

Proof