# Metamath Proof Explorer

## Theorem swrd00

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

Ref Expression
Assertion swrd00 ${⊢}{S}\mathrm{substr}⟨{X},{X}⟩=\varnothing$

### Proof

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