Theorem 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	⊢ ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) ↔ ( ∅ ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) )
2		opelxp	⊢ ( ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
3		swrdval	⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
4		fzonlt0	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ ( 𝐹 ..^ 𝐿 ) = ∅ ) )
5	4	biimprd	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 ..^ 𝐿 ) = ∅ → ¬ 𝐹 < 𝐿 ) )
6	5	con2d	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 𝐿 → ¬ ( 𝐹 ..^ 𝐿 ) = ∅ ) )
7	6	impcom	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) = ∅ )
8		ss0	⊢ ( ( 𝐹 ..^ 𝐿 ) ⊆ ∅ → ( 𝐹 ..^ 𝐿 ) = ∅ )
9	7 8	nsyl	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ∅ )
10		dm0	⊢ dom ∅ = ∅
11	10	a1i	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ∅ = ∅ )
12	11	sseq2d	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ ↔ ( 𝐹 ..^ 𝐿 ) ⊆ ∅ ) )
13	9 12	mtbird	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ )
14	13	iffalsed	⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
15		ssidd	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ∅ ⊆ ∅ )
16	4	biimpac	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐹 ..^ 𝐿 ) = ∅ )
17	10	a1i	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ∅ = ∅ )
18	15 16 17	3sstr4d	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ )
19	18	iftrued	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
20		zre	⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
21		zre	⊢ ( 𝐹 ∈ ℤ → 𝐹 ∈ ℝ )
22		lenlt	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( 𝐿 ≤ 𝐹 ↔ ¬ 𝐹 < 𝐿 ) )
23	22	bicomd	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( ¬ 𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹 ) )
24	20 21 23	syl2anr	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹 ) )
25		fzo0n	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 ↔ ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) )
26	24 25	bitrd	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) )
27	26	biimpac	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ )
28	27	mpteq1d	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
29	28	dmeqd	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
30		ral0	⊢ ∀ 𝑥 ∈ ∅ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ∈ V
31		dmmptg	⊢ ( ∀ 𝑥 ∈ ∅ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ∈ V → dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
32	30 31	mp1i	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
33	29 32	eqtrd	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
34		mptrel	⊢ Rel ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) )
35		reldm0	⊢ ( Rel ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ↔ dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ) )
36	34 35	mp1i	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ↔ dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ) )
37	33 36	mpbird	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
38	19 37	eqtrd	⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
39	14 38	pm2.61ian	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
40	39	3adant1	⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
41	3 40	eqtrd	⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
42	41	3expb	⊢ ( ( ∅ ∈ V ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
43	2 42	sylan2b	⊢ ( ( ∅ ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
44	1 43	sylbi	⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
45		df-substr	⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
46		ovex	⊢ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ∈ V
47	46	mptex	⊢ ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) ∈ V
48		0ex	⊢ ∅ ∈ V
49	47 48	ifex	⊢ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ∈ V
50	45 49	dmmpo	⊢ dom substr = ( V × ( ℤ × ℤ ) )
51	44 50	eleq2s	⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
52		df-ov	⊢ ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( substr ‘ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ )
53		ndmfv	⊢ ( ¬ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( substr ‘ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ) = ∅ )
54	52 53	eqtrid	⊢ ( ¬ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
55	51 54	pm2.61i	⊢ ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅