Theorem swrd00

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

	Ref	Expression
Assertion	swrd00	⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) ↔ ( 𝑆 ∈ V ∧ ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ) )
2		opelxp	⊢ ( ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) )
3		swrdval	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) )
4		fzo0	⊢ ( 𝑋 ..^ 𝑋 ) = ∅
5		0ss	⊢ ∅ ⊆ dom 𝑆
6	4 5	eqsstri	⊢ ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆
7	6	iftruei	⊢ if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
8		zcn	⊢ ( 𝑋 ∈ ℤ → 𝑋 ∈ ℂ )
9	8	subidd	⊢ ( 𝑋 ∈ ℤ → ( 𝑋 − 𝑋 ) = 0 )
10	9	oveq2d	⊢ ( 𝑋 ∈ ℤ → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ( 0 ..^ 0 ) )
11	10	3ad2ant2	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ( 0 ..^ 0 ) )
12		fzo0	⊢ ( 0 ..^ 0 ) = ∅
13	11 12	eqtrdi	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ∅ )
14	13	mpteq1d	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) )
15		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ∅
16	14 15	eqtrdi	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ∅ )
17	7 16	eqtrid	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) = ∅ )
18	3 17	eqtrd	⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
19	18	3expb	⊢ ( ( 𝑆 ∈ V ∧ ( 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
20	2 19	sylan2b	⊢ ( ( 𝑆 ∈ V ∧ ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
21	1 20	sylbi	⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
22		df-substr	⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
23		ovex	⊢ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ∈ V
24	23	mptex	⊢ ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) ∈ V
25		0ex	⊢ ∅ ∈ V
26	24 25	ifex	⊢ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ∈ V
27	22 26	dmmpo	⊢ dom substr = ( V × ( ℤ × ℤ ) )
28	21 27	eleq2s	⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
29		df-ov	⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ( substr ‘ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ )
30		ndmfv	⊢ ( ¬ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( substr ‘ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ) = ∅ )
31	29 30	eqtrid	⊢ ( ¬ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
32	28 31	pm2.61i	⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅