Metamath Proof Explorer

Theorem pfxsuff1eqwrdeq

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

Ref Expression
Assertion pfxsuff1eqwrdeq 
|- ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hashgt0n0 
 |-  ( ( W e. Word V /\ 0 < ( # ` W ) ) -> W =/= (/) )
2 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
3 1 2 syldan 
 |-  ( ( W e. Word V /\ 0 < ( # ` W ) ) -> ( # ` W ) e. NN )
4 3 3adant2 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( # ` W ) e. NN )
5 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
6 4 5 syl 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
7 pfxsuffeqwrdeq 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) ) ) )
8 6 7 syld3an3 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) ) ) )
9 hashneq0 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
10 9 biimpd 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) -> W =/= (/) ) )
11 10 imdistani 
 |-  ( ( W e. Word V /\ 0 < ( # ` W ) ) -> ( W e. Word V /\ W =/= (/) ) )
12 11 3adant2 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W e. Word V /\ W =/= (/) ) )
13 12 adantr 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( W e. Word V /\ W =/= (/) ) )
14 swrdlsw 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )
15 13 14 syl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )
16 breq2 
 |-  ( ( # ` W ) = ( # ` U ) -> ( 0 < ( # ` W ) <-> 0 < ( # ` U ) ) )
17 16 3anbi3d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) <-> ( W e. Word V /\ U e. Word V /\ 0 < ( # ` U ) ) ) )
18 hashneq0 
 |-  ( U e. Word V -> ( 0 < ( # ` U ) <-> U =/= (/) ) )
19 18 biimpd 
 |-  ( U e. Word V -> ( 0 < ( # ` U ) -> U =/= (/) ) )
20 19 imdistani 
 |-  ( ( U e. Word V /\ 0 < ( # ` U ) ) -> ( U e. Word V /\ U =/= (/) ) )
21 20 3adant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` U ) ) -> ( U e. Word V /\ U =/= (/) ) )
22 swrdlsw 
 |-  ( ( U e. Word V /\ U =/= (/) ) -> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> )
23 21 22 syl 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` U ) ) -> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> )
24 17 23 syl6bi 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> ) )
25 24 impcom 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> )
26 oveq1 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( # ` W ) - 1 ) = ( ( # ` U ) - 1 ) )
27 id 
 |-  ( ( # ` W ) = ( # ` U ) -> ( # ` W ) = ( # ` U ) )
28 26 27 opeq12d 
 |-  ( ( # ` W ) = ( # ` U ) -> <. ( ( # ` W ) - 1 ) , ( # ` W ) >. = <. ( ( # ` U ) - 1 ) , ( # ` U ) >. )
29 28 oveq2d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) )
30 29 eqeq1d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` U ) "> <-> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> ) )
31 30 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` U ) "> <-> ( U substr <. ( ( # ` U ) - 1 ) , ( # ` U ) >. ) = <" ( lastS ` U ) "> ) )
32 25 31 mpbird 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` U ) "> )
33 15 32 eqeq12d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) <-> <" ( lastS ` W ) "> = <" ( lastS ` U ) "> ) )
34 fvexd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( lastS ` W ) e. _V )
35 fvex 
 |-  ( lastS ` U ) e. _V
36 s111 
 |-  ( ( ( lastS ` W ) e. _V /\ ( lastS ` U ) e. _V ) -> ( <" ( lastS ` W ) "> = <" ( lastS ` U ) "> <-> ( lastS ` W ) = ( lastS ` U ) ) )
37 34 35 36 sylancl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( <" ( lastS ` W ) "> = <" ( lastS ` U ) "> <-> ( lastS ` W ) = ( lastS ` U ) ) )
38 33 37 bitrd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) <-> ( lastS ` W ) = ( lastS ` U ) ) )
39 38 anbi2d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) <-> ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) )
40 39 pm5.32da 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) ) <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
41 8 40 bitrd 
 |-  ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )