Metamath Proof Explorer

Theorem 2swrd2eqwrdeq

Description: Two words of length at least two are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018) (Revised by AV, 12-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
2 1z 
 |-  1 e. ZZ
3 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
4 zltp1le 
 |-  ( ( 1 e. ZZ /\ ( # ` W ) e. ZZ ) -> ( 1 < ( # ` W ) <-> ( 1 + 1 ) <_ ( # ` W ) ) )
5 2 3 4 sylancr 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) <-> ( 1 + 1 ) <_ ( # ` W ) ) )
6 1p1e2 
 |-  ( 1 + 1 ) = 2
7 6 a1i 
 |-  ( ( # ` W ) e. NN0 -> ( 1 + 1 ) = 2 )
8 7 breq1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( 1 + 1 ) <_ ( # ` W ) <-> 2 <_ ( # ` W ) ) )
9 8 biimpd 
 |-  ( ( # ` W ) e. NN0 -> ( ( 1 + 1 ) <_ ( # ` W ) -> 2 <_ ( # ` W ) ) )
10 5 9 sylbid 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) -> 2 <_ ( # ` W ) ) )
11 10 imp 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> 2 <_ ( # ` W ) )
12 2nn0 
 |-  2 e. NN0
13 simpl 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( # ` W ) e. NN0 )
14 nn0sub 
 |-  ( ( 2 e. NN0 /\ ( # ` W ) e. NN0 ) -> ( 2 <_ ( # ` W ) <-> ( ( # ` W ) - 2 ) e. NN0 ) )
15 12 13 14 sylancr 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( 2 <_ ( # ` W ) <-> ( ( # ` W ) - 2 ) e. NN0 ) )
16 11 15 mpbid 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. NN0 )
17 3 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( # ` W ) e. ZZ )
18 0red 
 |-  ( ( # ` W ) e. NN0 -> 0 e. RR )
19 1red 
 |-  ( ( # ` W ) e. NN0 -> 1 e. RR )
20 nn0re 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
21 18 19 20 3jca 
 |-  ( ( # ` W ) e. NN0 -> ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) )
22 0lt1 
 |-  0 < 1
23 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) -> ( ( 0 < 1 /\ 1 < ( # ` W ) ) -> 0 < ( # ` W ) ) )
24 23 expd 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) -> ( 0 < 1 -> ( 1 < ( # ` W ) -> 0 < ( # ` W ) ) ) )
25 21 22 24 mpisyl 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) -> 0 < ( # ` W ) ) )
26 25 imp 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> 0 < ( # ` W ) )
27 elnnz 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) )
28 17 26 27 sylanbrc 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( # ` W ) e. NN )
29 2rp 
 |-  2 e. RR+
30 29 a1i 
 |-  ( ( # ` W ) e. NN0 -> 2 e. RR+ )
31 20 30 ltsubrpd 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 2 ) < ( # ` W ) )
32 31 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) < ( # ` W ) )
33 elfzo0 
 |-  ( ( ( # ` W ) - 2 ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( ( # ` W ) - 2 ) e. NN0 /\ ( # ` W ) e. NN /\ ( ( # ` W ) - 2 ) < ( # ` W ) ) )
34 16 28 32 33 syl3anbrc 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. ( 0 ..^ ( # ` W ) ) )
35 1 34 sylan 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. ( 0 ..^ ( # ` W ) ) )
36 35 3adant2 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. ( 0 ..^ ( # ` W ) ) )
37 pfxsuffeqwrdeq 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( ( # ` W ) - 2 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) ) ) ) )
38 36 37 syld3an3 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) ) ) ) )
39 swrd2lsw 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
40 39 3adant2 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
41 40 adantr 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
42 breq2 
 |-  ( ( # ` W ) = ( # ` U ) -> ( 1 < ( # ` W ) <-> 1 < ( # ` U ) ) )
43 42 3anbi3d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) <-> ( W e. Word V /\ U e. Word V /\ 1 < ( # ` U ) ) ) )
44 swrd2lsw 
 |-  ( ( U e. Word V /\ 1 < ( # ` U ) ) -> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> )
45 44 3adant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` U ) ) -> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> )
46 43 45 syl6bi 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> ) )
47 46 impcom 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> )
48 oveq1 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( # ` W ) - 2 ) = ( ( # ` U ) - 2 ) )
49 id 
 |-  ( ( # ` W ) = ( # ` U ) -> ( # ` W ) = ( # ` U ) )
50 48 49 opeq12d 
 |-  ( ( # ` W ) = ( # ` U ) -> <. ( ( # ` W ) - 2 ) , ( # ` W ) >. = <. ( ( # ` U ) - 2 ) , ( # ` U ) >. )
51 50 oveq2d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) )
52 51 eqeq1d 
 |-  ( ( # ` W ) = ( # ` U ) -> ( ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> <-> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> ) )
53 52 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> <-> ( U substr <. ( ( # ` U ) - 2 ) , ( # ` U ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> ) )
54 47 53 mpbird 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> )
55 41 54 eqeq12d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) <-> <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> ) )
56 fvexd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( W ` ( ( # ` W ) - 2 ) ) e. _V )
57 fvexd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( lastS ` W ) e. _V )
58 fvexd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U ` ( ( # ` U ) - 2 ) ) e. _V )
59 fvexd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( lastS ` U ) e. _V )
60 s2eq2s1eq 
 |-  ( ( ( ( W ` ( ( # ` W ) - 2 ) ) e. _V /\ ( lastS ` W ) e. _V ) /\ ( ( U ` ( ( # ` U ) - 2 ) ) e. _V /\ ( lastS ` U ) e. _V ) ) -> ( <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> <-> ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> /\ <" ( lastS ` W ) "> = <" ( lastS ` U ) "> ) ) )
61 56 57 58 59 60 syl22anc 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) ( lastS ` U ) "> <-> ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> /\ <" ( lastS ` W ) "> = <" ( lastS ` U ) "> ) ) )
62 fvex 
 |-  ( W ` ( ( # ` W ) - 2 ) ) e. _V
63 s111 
 |-  ( ( ( W ` ( ( # ` W ) - 2 ) ) e. _V /\ ( U ` ( ( # ` U ) - 2 ) ) e. _V ) -> ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> <-> ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` U ) - 2 ) ) ) )
64 62 58 63 sylancr 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> <-> ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` U ) - 2 ) ) ) )
65 fvoveq1 
 |-  ( ( # ` U ) = ( # ` W ) -> ( U ` ( ( # ` U ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) )
66 65 eqcoms 
 |-  ( ( # ` W ) = ( # ` U ) -> ( U ` ( ( # ` U ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) )
67 66 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( U ` ( ( # ` U ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) )
68 67 eqeq2d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` U ) - 2 ) ) <-> ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) ) )
69 64 68 bitrd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> <-> ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) ) )
70 fvex 
 |-  ( lastS ` W ) e. _V
71 s111 
 |-  ( ( ( lastS ` W ) e. _V /\ ( lastS ` U ) e. _V ) -> ( <" ( lastS ` W ) "> = <" ( lastS ` U ) "> <-> ( lastS ` W ) = ( lastS ` U ) ) )
72 70 59 71 sylancr 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( <" ( lastS ` W ) "> = <" ( lastS ` U ) "> <-> ( lastS ` W ) = ( lastS ` U ) ) )
73 69 72 anbi12d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( <" ( W ` ( ( # ` W ) - 2 ) ) "> = <" ( U ` ( ( # ` U ) - 2 ) ) "> /\ <" ( lastS ` W ) "> = <" ( lastS ` U ) "> ) <-> ( ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) )
74 55 61 73 3bitrd 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) <-> ( ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) )
75 74 anbi2d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) ) <-> ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
76 3anass 
 |-  ( ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) <-> ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) )
77 75 76 bitr4di 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) /\ ( # ` W ) = ( # ` U ) ) -> ( ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) ) <-> ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) )
78 77 pm5.32da 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( U substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) ) ) <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
79 38 78 bitrd 
 |-  ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 2 ) ) = ( U prefix ( ( # ` W ) - 2 ) ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )