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