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 >. ) ) )