This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdspsleq

Description: Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Proof shortened by AV, 7-May-2020)

Ref Expression
Assertion swrdspsleq 
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )

Proof

Step Hyp Ref Expression
1 swrdsb0eq 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )
2 1 3expa 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) /\ N <_ M ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )
3 2 ancoms 
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )
4 3 3adantr3 
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )
5 ral0 
 |-  A. i e. (/) ( W ` i ) = ( U ` i )
6 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
7 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
8 fzon 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
9 6 7 8 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
10 9 biimpa 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( M ..^ N ) = (/) )
11 10 raleqdv 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) <-> A. i e. (/) ( W ` i ) = ( U ` i ) ) )
12 5 11 mpbiri 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) )
13 12 ex 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ M -> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
14 13 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( N <_ M -> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
15 14 impcom 
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) )
16 4 15 2thd 
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
17 swrdcl 
 |-  ( W e. Word V -> ( W substr <. M , N >. ) e. Word V )
18 swrdcl 
 |-  ( U e. Word V -> ( U substr <. M , N >. ) e. Word V )
19 eqwrd 
 |-  ( ( ( W substr <. M , N >. ) e. Word V /\ ( U substr <. M , N >. ) e. Word V ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> ( ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) /\ A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) ) )
20 17 18 19 syl2an 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> ( ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) /\ A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) ) )
21 20 3ad2ant1 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> ( ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) /\ A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) ) )
22 21 adantl 
 |-  ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> ( ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) /\ A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) ) )
23 swrdsbslen 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) )
24 23 adantl 
 |-  ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) )
25 24 biantrurd 
 |-  ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> ( ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) /\ A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) ) )
26 nn0re 
 |-  ( M e. NN0 -> M e. RR )
27 nn0re 
 |-  ( N e. NN0 -> N e. RR )
28 ltnle 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> -. N <_ M ) )
29 ltle 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N -> M <_ N ) )
30 28 29 sylbird 
 |-  ( ( M e. RR /\ N e. RR ) -> ( -. N <_ M -> M <_ N ) )
31 26 27 30 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. N <_ M -> M <_ N ) )
32 31 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> M <_ N ) )
33 simpl1l 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> W e. Word V )
34 simpl2l 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> M e. NN0 )
35 6 7 anim12i 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. ZZ /\ N e. ZZ ) )
36 35 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
37 36 anim1i 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( ( M e. ZZ /\ N e. ZZ ) /\ M <_ N ) )
38 df-3an 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ M <_ N ) )
39 37 38 sylibr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
40 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
41 39 40 sylibr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N e. ( ZZ>= ` M ) )
42 34 41 jca 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) )
43 simpl3l 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` W ) )
44 swrdlen2 
 |-  ( ( W e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` W ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
45 33 42 43 44 syl3anc 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
46 45 oveq2d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) = ( 0 ..^ ( N - M ) ) )
47 46 raleqdv 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. j e. ( 0 ..^ ( N - M ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) )
48 0zd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> 0 e. ZZ )
49 zsubcl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
50 7 6 49 syl2anr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N - M ) e. ZZ )
51 50 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( N - M ) e. ZZ )
52 6 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. ZZ )
53 52 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> M e. ZZ )
54 fzoshftral 
 |-  ( ( 0 e. ZZ /\ ( N - M ) e. ZZ /\ M e. ZZ ) -> ( A. j e. ( 0 ..^ ( N - M ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) )
55 48 51 53 54 syl3anc 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( A. j e. ( 0 ..^ ( N - M ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) )
56 55 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. j e. ( 0 ..^ ( N - M ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) )
57 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
58 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
59 addlid 
 |-  ( M e. CC -> ( 0 + M ) = M )
60 59 adantl 
 |-  ( ( N e. CC /\ M e. CC ) -> ( 0 + M ) = M )
61 npcan 
 |-  ( ( N e. CC /\ M e. CC ) -> ( ( N - M ) + M ) = N )
62 60 61 oveq12d 
 |-  ( ( N e. CC /\ M e. CC ) -> ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) = ( M ..^ N ) )
63 57 58 62 syl2anr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) = ( M ..^ N ) )
64 63 3ad2ant2 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) = ( M ..^ N ) )
65 64 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) = ( M ..^ N ) )
66 65 raleqdv 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. i e. ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) ) )
67 ovex 
 |-  ( i - M ) e. _V
68 sbceqg 
 |-  ( ( i - M ) e. _V -> ( [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> [_ ( i - M ) / j ]_ ( ( W substr <. M , N >. ) ` j ) = [_ ( i - M ) / j ]_ ( ( U substr <. M , N >. ) ` j ) ) )
69 csbfv2g 
 |-  ( ( i - M ) e. _V -> [_ ( i - M ) / j ]_ ( ( W substr <. M , N >. ) ` j ) = ( ( W substr <. M , N >. ) ` [_ ( i - M ) / j ]_ j ) )
70 csbvarg 
 |-  ( ( i - M ) e. _V -> [_ ( i - M ) / j ]_ j = ( i - M ) )
71 70 fveq2d 
 |-  ( ( i - M ) e. _V -> ( ( W substr <. M , N >. ) ` [_ ( i - M ) / j ]_ j ) = ( ( W substr <. M , N >. ) ` ( i - M ) ) )
72 69 71 eqtrd 
 |-  ( ( i - M ) e. _V -> [_ ( i - M ) / j ]_ ( ( W substr <. M , N >. ) ` j ) = ( ( W substr <. M , N >. ) ` ( i - M ) ) )
73 csbfv2g 
 |-  ( ( i - M ) e. _V -> [_ ( i - M ) / j ]_ ( ( U substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` [_ ( i - M ) / j ]_ j ) )
74 70 fveq2d 
 |-  ( ( i - M ) e. _V -> ( ( U substr <. M , N >. ) ` [_ ( i - M ) / j ]_ j ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) )
75 73 74 eqtrd 
 |-  ( ( i - M ) e. _V -> [_ ( i - M ) / j ]_ ( ( U substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) )
76 72 75 eqeq12d 
 |-  ( ( i - M ) e. _V -> ( [_ ( i - M ) / j ]_ ( ( W substr <. M , N >. ) ` j ) = [_ ( i - M ) / j ]_ ( ( U substr <. M , N >. ) ` j ) <-> ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) ) )
77 68 76 bitrd 
 |-  ( ( i - M ) e. _V -> ( [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) ) )
78 67 77 mp1i 
 |-  ( ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) /\ i e. ( M ..^ N ) ) -> ( [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) ) )
79 33 42 43 3jca 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( W e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` W ) ) )
80 swrdfv2 
 |-  ( ( ( W e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` W ) ) /\ i e. ( M ..^ N ) ) -> ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( W ` i ) )
81 79 80 sylan 
 |-  ( ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) /\ i e. ( M ..^ N ) ) -> ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( W ` i ) )
82 simpl1r 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> U e. Word V )
83 simpl3r 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` U ) )
84 82 42 83 3jca 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( U e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` U ) ) )
85 swrdfv2 
 |-  ( ( ( U e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` U ) ) /\ i e. ( M ..^ N ) ) -> ( ( U substr <. M , N >. ) ` ( i - M ) ) = ( U ` i ) )
86 84 85 sylan 
 |-  ( ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) /\ i e. ( M ..^ N ) ) -> ( ( U substr <. M , N >. ) ` ( i - M ) ) = ( U ` i ) )
87 81 86 eqeq12d 
 |-  ( ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) /\ i e. ( M ..^ N ) ) -> ( ( ( W substr <. M , N >. ) ` ( i - M ) ) = ( ( U substr <. M , N >. ) ` ( i - M ) ) <-> ( W ` i ) = ( U ` i ) ) )
88 78 87 bitrd 
 |-  ( ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) /\ i e. ( M ..^ N ) ) -> ( [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> ( W ` i ) = ( U ` i ) ) )
89 88 ralbidva 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. i e. ( M ..^ N ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
90 66 89 bitrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. i e. ( ( 0 + M ) ..^ ( ( N - M ) + M ) ) [. ( i - M ) / j ]. ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
91 47 56 90 3bitrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
92 91 ex 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M <_ N -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) ) )
93 32 92 syld 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) ) )
94 93 impcom 
 |-  ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( A. j e. ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) ( ( W substr <. M , N >. ) ` j ) = ( ( U substr <. M , N >. ) ` j ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
95 22 25 94 3bitr2d 
 |-  ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )
96 16 95 pm2.61ian 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W substr <. M , N >. ) = ( U substr <. M , N >. ) <-> A. i e. ( M ..^ N ) ( W ` i ) = ( U ` i ) ) )