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

Metamath Proof Explorer

Theorem swrdsb0eq

Description: Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> W e. Word V )
2 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
3 2 ad2antrl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> M e. ZZ )
4 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
5 4 ad2antll 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> N e. ZZ )
6 swrdlend 
 |-  ( ( W e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( N <_ M -> ( W substr <. M , N >. ) = (/) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ M -> ( W substr <. M , N >. ) = (/) ) )
8 7 3impia 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( W substr <. M , N >. ) = (/) )
9 simplr 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> U e. Word V )
10 swrdlend 
 |-  ( ( U e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( N <_ M -> ( U substr <. M , N >. ) = (/) ) )
11 9 3 5 10 syl3anc 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ M -> ( U substr <. M , N >. ) = (/) ) )
12 11 3impia 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( U substr <. M , N >. ) = (/) )
13 8 12 eqtr4d 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) )