Metamath Proof Explorer


Theorem swrd00

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

Ref Expression
Assertion swrd00 S substr X X =

Proof

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