Metamath Proof Explorer


Theorem swrdsbslen

Description: Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020)

Ref Expression
Assertion 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 >. ) ) )

Proof

Step Hyp Ref Expression
1 simpr1
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( W e. Word V /\ U e. Word V ) )
2 simpr2
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( M e. NN0 /\ N e. NN0 ) )
3 simpl
 |-  ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> N <_ M )
4 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 >. ) )
5 1 2 3 4 syl3anc
 |-  ( ( 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 >. ) )
6 5 fveq2d
 |-  ( ( 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 >. ) ) )
7 nn0re
 |-  ( M e. NN0 -> M e. RR )
8 nn0re
 |-  ( N e. NN0 -> N e. RR )
9 ltnle
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> -. N <_ M ) )
10 ltle
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N -> M <_ N ) )
11 9 10 sylbird
 |-  ( ( M e. RR /\ N e. RR ) -> ( -. N <_ M -> M <_ N ) )
12 7 8 11 syl2an
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. N <_ M -> M <_ N ) )
13 12 3ad2ant2
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> M <_ N ) )
14 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 )
15 simpl2l
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> M e. NN0 )
16 nn0z
 |-  ( M e. NN0 -> M e. ZZ )
17 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
18 16 17 anim12i
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. ZZ /\ N e. ZZ ) )
19 18 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 ) )
20 19 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 ) )
21 df-3an
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ M <_ N ) )
22 20 21 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 ) )
23 eluz2
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
24 22 23 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 ) )
25 simpl3l
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` W ) )
26 swrdlen2
 |-  ( ( W e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` W ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
27 14 15 24 25 26 syl121anc
 |-  ( ( ( ( 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 ) )
28 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 )
29 simpl3r
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` U ) )
30 swrdlen2
 |-  ( ( U e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` U ) ) -> ( # ` ( U substr <. M , N >. ) ) = ( N - M ) )
31 28 15 24 29 30 syl121anc
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( U substr <. M , N >. ) ) = ( N - M ) )
32 27 31 eqtr4d
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) )
33 32 ex
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M <_ N -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) )
34 13 33 syld
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) )
35 34 impcom
 |-  ( ( -. 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 >. ) ) )
36 6 35 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 >. ) ) )