swrd00

Description: A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015)

		Ref	Expression
	Assertion	swrd00	$⊢ S substr ⟨X, X⟩ = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨S, ⟨X, X⟩⟩ \in (V \times (ℤ \times ℤ)) \leftrightarrow (S \in V \land ⟨X, X⟩ \in (ℤ \times ℤ))$
2		opelxp	$⊢ ⟨X, X⟩ \in (ℤ \times ℤ) \leftrightarrow (X \in ℤ \land X \in ℤ)$
3		swrdval	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to S substr ⟨X, X⟩ = if ((X ..^X) \subseteq dom S, (x \in (0 ..^X - X) ⟼ S (x + X)), \emptyset)$
4		fzo0	$⊢ (X ..^X) = \emptyset$
5		0ss	$⊢ \emptyset \subseteq dom S$
6	4 5	eqsstri	$⊢ (X ..^X) \subseteq dom S$
7	6	iftruei	$⊢ if ((X ..^X) \subseteq dom S, (x \in (0 ..^X - X) ⟼ S (x + X)), \emptyset) = (x \in (0 ..^X - X) ⟼ S (x + X))$
8		zcn	$⊢ X \in ℤ \to X \in ℂ$
9	8	subidd	$⊢ X \in ℤ \to X - X = 0$
10	9	oveq2d	$⊢ X \in ℤ \to (0 ..^X - X) = (0 ..^0)$
11	10	3ad2ant2	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to (0 ..^X - X) = (0 ..^0)$
12		fzo0	$⊢ (0 ..^0) = \emptyset$
13	11 12	eqtrdi	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to (0 ..^X - X) = \emptyset$
14	13	mpteq1d	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to (x \in (0 ..^X - X) ⟼ S (x + X)) = (x \in \emptyset ⟼ S (x + X))$
15		mpt0	$⊢ (x \in \emptyset ⟼ S (x + X)) = \emptyset$
16	14 15	eqtrdi	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to (x \in (0 ..^X - X) ⟼ S (x + X)) = \emptyset$
17	7 16	eqtrid	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to if ((X ..^X) \subseteq dom S, (x \in (0 ..^X - X) ⟼ S (x + X)), \emptyset) = \emptyset$
18	3 17	eqtrd	$⊢ (S \in V \land X \in ℤ \land X \in ℤ) \to S substr ⟨X, X⟩ = \emptyset$
19	18	3expb	$⊢ (S \in V \land (X \in ℤ \land X \in ℤ)) \to S substr ⟨X, X⟩ = \emptyset$
20	2 19	sylan2b	$⊢ (S \in V \land ⟨X, X⟩ \in (ℤ \times ℤ)) \to S substr ⟨X, X⟩ = \emptyset$
21	1 20	sylbi	$⊢ ⟨S, ⟨X, X⟩⟩ \in (V \times (ℤ \times ℤ)) \to S substr ⟨X, X⟩ = \emptyset$
22		df-substr	$⊢ substr = (s \in V, b \in (ℤ \times ℤ) ⟼ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))), \emptyset))$
23		ovex	$⊢ (0 ..^2^{nd} (b) - 1^{st} (b)) \in V$
24	23	mptex	$⊢ (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))) \in V$
25		0ex	$⊢ \emptyset \in V$
26	24 25	ifex	$⊢ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))), \emptyset) \in V$
27	22 26	dmmpo	$⊢ dom substr = V \times (ℤ \times ℤ)$
28	21 27	eleq2s	$⊢ ⟨S, ⟨X, X⟩⟩ \in dom substr \to S substr ⟨X, X⟩ = \emptyset$
29		df-ov	$⊢ S substr ⟨X, X⟩ = substr (⟨S, ⟨X, X⟩⟩)$
30		ndmfv	$⊢ \neg ⟨S, ⟨X, X⟩⟩ \in dom substr \to substr (⟨S, ⟨X, X⟩⟩) = \emptyset$
31	29 30	eqtrid	$⊢ \neg ⟨S, ⟨X, X⟩⟩ \in dom substr \to S substr ⟨X, X⟩ = \emptyset$
32	28 31	pm2.61i	$⊢ S substr ⟨X, X⟩ = \emptyset$

Metamath Proof Explorer

Theorem swrd00

Proof