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