Metamath Proof Explorer

Theorem swrdwrdsymb

Description: A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022)

Ref Expression
Assertion swrdwrdsymb 
|- ( S e. Word A -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 swrdval2 
 |-  ( ( S e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. M , N >. ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) )
2 1 3expb 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. M , N >. ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) )
3 wrdf 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> A )
4 3 ffund 
 |-  ( S e. Word A -> Fun S )
5 4 adantr 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> Fun S )
6 5 adantr 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> Fun S )
7 wrddm 
 |-  ( S e. Word A -> dom S = ( 0 ..^ ( # ` S ) ) )
8 elfzodifsumelfzo 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) -> ( x + M ) e. ( 0 ..^ ( # ` S ) ) ) )
9 8 imp 
 |-  ( ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ ( # ` S ) ) )
10 9 adantl 
 |-  ( ( dom S = ( 0 ..^ ( # ` S ) ) /\ ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) ) -> ( x + M ) e. ( 0 ..^ ( # ` S ) ) )
11 eleq2 
 |-  ( dom S = ( 0 ..^ ( # ` S ) ) -> ( ( x + M ) e. dom S <-> ( x + M ) e. ( 0 ..^ ( # ` S ) ) ) )
12 11 adantr 
 |-  ( ( dom S = ( 0 ..^ ( # ` S ) ) /\ ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( x + M ) e. dom S <-> ( x + M ) e. ( 0 ..^ ( # ` S ) ) ) )
13 10 12 mpbird 
 |-  ( ( dom S = ( 0 ..^ ( # ` S ) ) /\ ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) ) -> ( x + M ) e. dom S )
14 13 exp32 
 |-  ( dom S = ( 0 ..^ ( # ` S ) ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) -> ( x + M ) e. dom S ) ) )
15 7 14 syl 
 |-  ( S e. Word A -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) -> ( x + M ) e. dom S ) ) )
16 15 imp31 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. dom S )
17 simpr 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> x e. ( 0 ..^ ( N - M ) ) )
18 elfzelz 
 |-  ( N e. ( 0 ... ( # ` S ) ) -> N e. ZZ )
19 18 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> N e. ZZ )
20 19 adantl 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> N e. ZZ )
21 20 adantr 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> N e. ZZ )
22 elfzelz 
 |-  ( M e. ( 0 ... N ) -> M e. ZZ )
23 22 ad2antrl 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> M e. ZZ )
24 23 adantr 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ZZ )
25 fzoaddel2 
 |-  ( ( x e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( x + M ) e. ( M ..^ N ) )
26 17 21 24 25 syl3anc 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( M ..^ N ) )
27 funfvima 
 |-  ( ( Fun S /\ ( x + M ) e. dom S ) -> ( ( x + M ) e. ( M ..^ N ) -> ( S ` ( x + M ) ) e. ( S " ( M ..^ N ) ) ) )
28 27 imp 
 |-  ( ( ( Fun S /\ ( x + M ) e. dom S ) /\ ( x + M ) e. ( M ..^ N ) ) -> ( S ` ( x + M ) ) e. ( S " ( M ..^ N ) ) )
29 6 16 26 28 syl21anc 
 |-  ( ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( S ` ( x + M ) ) e. ( S " ( M ..^ N ) ) )
30 29 fmpttd 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( N - M ) ) --> ( S " ( M ..^ N ) ) )
31 fvex 
 |-  ( S ` ( x + M ) ) e. _V
32 eqid 
 |-  ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) )
33 31 32 fnmpti 
 |-  ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) Fn ( 0 ..^ ( N - M ) )
34 hashfn 
 |-  ( ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) Fn ( 0 ..^ ( N - M ) ) -> ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) = ( # ` ( 0 ..^ ( N - M ) ) ) )
35 33 34 mp1i 
 |-  ( M e. ( 0 ... N ) -> ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) = ( # ` ( 0 ..^ ( N - M ) ) ) )
36 fznn0sub 
 |-  ( M e. ( 0 ... N ) -> ( N - M ) e. NN0 )
37 hashfzo0 
 |-  ( ( N - M ) e. NN0 -> ( # ` ( 0 ..^ ( N - M ) ) ) = ( N - M ) )
38 36 37 syl 
 |-  ( M e. ( 0 ... N ) -> ( # ` ( 0 ..^ ( N - M ) ) ) = ( N - M ) )
39 35 38 eqtrd 
 |-  ( M e. ( 0 ... N ) -> ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) = ( N - M ) )
40 39 oveq2d 
 |-  ( M e. ( 0 ... N ) -> ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) ) = ( 0 ..^ ( N - M ) ) )
41 40 feq2d 
 |-  ( M e. ( 0 ... N ) -> ( ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) ) --> ( S " ( M ..^ N ) ) <-> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( N - M ) ) --> ( S " ( M ..^ N ) ) ) )
42 41 ad2antrl 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) ) --> ( S " ( M ..^ N ) ) <-> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( N - M ) ) --> ( S " ( M ..^ N ) ) ) )
43 30 42 mpbird 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) ) --> ( S " ( M ..^ N ) ) )
44 iswrdb 
 |-  ( ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) e. Word ( S " ( M ..^ N ) ) <-> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) ) ) --> ( S " ( M ..^ N ) ) )
45 43 44 sylibr 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( S ` ( x + M ) ) ) e. Word ( S " ( M ..^ N ) ) )
46 2 45 eqeltrd 
 |-  ( ( S e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) )
47 46 expcom 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( S e. Word A -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) ) )
48 swrdnd0 
 |-  ( S e. Word A -> ( -. ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. M , N >. ) = (/) ) )
49 wrd0 
 |-  (/) e. Word ( S " ( M ..^ N ) )
50 eleq1 
 |-  ( ( S substr <. M , N >. ) = (/) -> ( ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) <-> (/) e. Word ( S " ( M ..^ N ) ) ) )
51 49 50 mpbiri 
 |-  ( ( S substr <. M , N >. ) = (/) -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) )
52 48 51 syl6com 
 |-  ( -. ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` S ) ) ) -> ( S e. Word A -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) ) )
53 47 52 pm2.61i 
 |-  ( S e. Word A -> ( S substr <. M , N >. ) e. Word ( S " ( M ..^ N ) ) )