Metamath Proof Explorer


Theorem pfxsuffeqwrdeq

Description: Two words are equal if and only if they have the same prefix and the same suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018) (Revised by AV, 5-May-2020)

Ref Expression
Assertion pfxsuffeqwrdeq
|- ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqwrd
 |-  ( ( W e. Word V /\ S e. Word V ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) ) )
2 1 3adant3
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) ) )
3 elfzofz
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ( 0 ... ( # ` W ) ) )
4 fzosplit
 |-  ( I e. ( 0 ... ( # ` W ) ) -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) )
5 3 4 syl
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) )
6 5 3ad2ant3
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) )
7 6 adantr
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) )
8 7 raleqdv
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) <-> A. i e. ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) ( W ` i ) = ( S ` i ) ) )
9 ralunb
 |-  ( A. i e. ( ( 0 ..^ I ) u. ( I ..^ ( # ` W ) ) ) ( W ` i ) = ( S ` i ) <-> ( A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) /\ A. i e. ( I ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) )
10 8 9 bitrdi
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) <-> ( A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) /\ A. i e. ( I ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) ) )
11 eqidd
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> I = I )
12 3simpa
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W e. Word V /\ S e. Word V ) )
13 12 adantr
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( W e. Word V /\ S e. Word V ) )
14 elfzonn0
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. NN0 )
15 14 14 jca
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I e. NN0 /\ I e. NN0 ) )
16 15 3ad2ant3
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( I e. NN0 /\ I e. NN0 ) )
17 16 adantr
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( I e. NN0 /\ I e. NN0 ) )
18 elfzo0le
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I <_ ( # ` W ) )
19 18 3ad2ant3
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I <_ ( # ` W ) )
20 19 adantr
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> I <_ ( # ` W ) )
21 breq2
 |-  ( ( # ` W ) = ( # ` S ) -> ( I <_ ( # ` W ) <-> I <_ ( # ` S ) ) )
22 21 adantl
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( I <_ ( # ` W ) <-> I <_ ( # ` S ) ) )
23 20 22 mpbid
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> I <_ ( # ` S ) )
24 pfxeq
 |-  ( ( ( W e. Word V /\ S e. Word V ) /\ ( I e. NN0 /\ I e. NN0 ) /\ ( I <_ ( # ` W ) /\ I <_ ( # ` S ) ) ) -> ( ( W prefix I ) = ( S prefix I ) <-> ( I = I /\ A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) ) ) )
25 13 17 20 23 24 syl112anc
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( ( W prefix I ) = ( S prefix I ) <-> ( I = I /\ A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) ) ) )
26 11 25 mpbirand
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( ( W prefix I ) = ( S prefix I ) <-> A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) ) )
27 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
28 27 14 anim12ci
 |-  ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( I e. NN0 /\ ( # ` W ) e. NN0 ) )
29 28 3adant2
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( I e. NN0 /\ ( # ` W ) e. NN0 ) )
30 29 adantr
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( I e. NN0 /\ ( # ` W ) e. NN0 ) )
31 27 nn0red
 |-  ( W e. Word V -> ( # ` W ) e. RR )
32 31 leidd
 |-  ( W e. Word V -> ( # ` W ) <_ ( # ` W ) )
33 32 adantr
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` S ) ) -> ( # ` W ) <_ ( # ` W ) )
34 eqle
 |-  ( ( ( # ` W ) e. RR /\ ( # ` W ) = ( # ` S ) ) -> ( # ` W ) <_ ( # ` S ) )
35 31 34 sylan
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` S ) ) -> ( # ` W ) <_ ( # ` S ) )
36 33 35 jca
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` S ) ) -> ( ( # ` W ) <_ ( # ` W ) /\ ( # ` W ) <_ ( # ` S ) ) )
37 36 3ad2antl1
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( ( # ` W ) <_ ( # ` W ) /\ ( # ` W ) <_ ( # ` S ) ) )
38 swrdspsleq
 |-  ( ( ( W e. Word V /\ S e. Word V ) /\ ( I e. NN0 /\ ( # ` W ) e. NN0 ) /\ ( ( # ` W ) <_ ( # ` W ) /\ ( # ` W ) <_ ( # ` S ) ) ) -> ( ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) <-> A. i e. ( I ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) )
39 13 30 37 38 syl3anc
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) <-> A. i e. ( I ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) )
40 26 39 anbi12d
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) <-> ( A. i e. ( 0 ..^ I ) ( W ` i ) = ( S ` i ) /\ A. i e. ( I ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) ) )
41 10 40 bitr4d
 |-  ( ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ ( # ` W ) = ( # ` S ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) <-> ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) )
42 41 pm5.32da
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) = ( # ` S ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( S ` i ) ) <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )
43 2 42 bitrd
 |-  ( ( W e. Word V /\ S e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )