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 ∈ Word V ∧ U ∈ 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 ∈ Word V → W ∈ ℕ 0
2 1z ⊢ 1 ∈ ℤ
3 nn0z ⊢ W ∈ ℕ 0 → W ∈ ℤ
4 zltp1le ⊢ 1 ∈ ℤ ∧ W ∈ ℤ → 1 < W ↔ 1 + 1 ≤ W
5 2 3 4 sylancr ⊢ W ∈ ℕ 0 → 1 < W ↔ 1 + 1 ≤ W
6 1p1e2 ⊢ 1 + 1 = 2
7 6 a1i ⊢ W ∈ ℕ 0 → 1 + 1 = 2
8 7 breq1d ⊢ W ∈ ℕ 0 → 1 + 1 ≤ W ↔ 2 ≤ W
9 8 biimpd ⊢ W ∈ ℕ 0 → 1 + 1 ≤ W → 2 ≤ W
10 5 9 sylbid ⊢ W ∈ ℕ 0 → 1 < W → 2 ≤ W
11 10 imp ⊢ W ∈ ℕ 0 ∧ 1 < W → 2 ≤ W
12 2nn0 ⊢ 2 ∈ ℕ 0
13 simpl ⊢ W ∈ ℕ 0 ∧ 1 < W → W ∈ ℕ 0
14 nn0sub ⊢ 2 ∈ ℕ 0 ∧ W ∈ ℕ 0 → 2 ≤ W ↔ W − 2 ∈ ℕ 0
15 12 13 14 sylancr ⊢ W ∈ ℕ 0 ∧ 1 < W → 2 ≤ W ↔ W − 2 ∈ ℕ 0
16 11 15 mpbid ⊢ W ∈ ℕ 0 ∧ 1 < W → W − 2 ∈ ℕ 0
17 3 adantr ⊢ W ∈ ℕ 0 ∧ 1 < W → W ∈ ℤ
18 0red ⊢ W ∈ ℕ 0 → 0 ∈ ℝ
19 1red ⊢ W ∈ ℕ 0 → 1 ∈ ℝ
20 nn0re ⊢ W ∈ ℕ 0 → W ∈ ℝ
21 18 19 20 3jca ⊢ W ∈ ℕ 0 → 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ
22 0lt1 ⊢ 0 < 1
23 lttr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ → 0 < 1 ∧ 1 < W → 0 < W
24 23 expd ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ → 0 < 1 → 1 < W → 0 < W
25 21 22 24 mpisyl ⊢ W ∈ ℕ 0 → 1 < W → 0 < W
26 25 imp ⊢ W ∈ ℕ 0 ∧ 1 < W → 0 < W
27 elnnz ⊢ W ∈ ℕ ↔ W ∈ ℤ ∧ 0 < W
28 17 26 27 sylanbrc ⊢ W ∈ ℕ 0 ∧ 1 < W → W ∈ ℕ
29 2rp ⊢ 2 ∈ ℝ +
30 29 a1i ⊢ W ∈ ℕ 0 → 2 ∈ ℝ +
31 20 30 ltsubrpd ⊢ W ∈ ℕ 0 → W − 2 < W
32 31 adantr ⊢ W ∈ ℕ 0 ∧ 1 < W → W − 2 < W
33 elfzo0 ⊢ W − 2 ∈ 0 ..^ W ↔ W − 2 ∈ ℕ 0 ∧ W ∈ ℕ ∧ W − 2 < W
34 16 28 32 33 syl3anbrc ⊢ W ∈ ℕ 0 ∧ 1 < W → W − 2 ∈ 0 ..^ W
35 1 34 sylan ⊢ W ∈ Word V ∧ 1 < W → W − 2 ∈ 0 ..^ W
36 35 3adant2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W → W − 2 ∈ 0 ..^ W
37 pfxsuffeqwrdeq ⊢ W ∈ Word V ∧ U ∈ Word V ∧ W − 2 ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ 1 < W → W substr W − 2 W = ⟨“ W ⁡ W − 2 lastS ⁡ W ”⟩
40 39 3adant2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W → W substr W − 2 W = ⟨“ W ⁡ W − 2 lastS ⁡ W ”⟩
41 40 adantr ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 1 < W ↔ W ∈ Word V ∧ U ∈ Word V ∧ 1 < U
44 swrd2lsw ⊢ U ∈ Word V ∧ 1 < U → U substr U − 2 U = ⟨“ U ⁡ U − 2 lastS ⁡ U ”⟩
45 44 3adant1 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < U → U substr U − 2 U = ⟨“ U ⁡ U − 2 lastS ⁡ U ”⟩
46 43 45 biimtrdi ⊢ W = U → W ∈ Word V ∧ U ∈ Word V ∧ 1 < W → U substr U − 2 U = ⟨“ U ⁡ U − 2 lastS ⁡ U ”⟩
47 46 impcom ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → U substr W − 2 W = ⟨“ U ⁡ U − 2 lastS ⁡ U ”⟩
55 41 54 eqeq12d ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → W ⁡ W − 2 ∈ V
57 fvexd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → lastS ⁡ W ∈ V
58 fvexd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → U ⁡ U − 2 ∈ V
59 fvexd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → lastS ⁡ U ∈ V
60 s2eq2s1eq ⊢ W ⁡ W − 2 ∈ V ∧ lastS ⁡ W ∈ V ∧ U ⁡ U − 2 ∈ V ∧ lastS ⁡ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ V
63 s111 ⊢ W ⁡ W − 2 ∈ V ∧ U ⁡ U − 2 ∈ V → ⟨“ W ⁡ W − 2 ”⟩ = ⟨“ U ⁡ U − 2 ”⟩ ↔ W ⁡ W − 2 = U ⁡ U − 2
64 62 58 63 sylancr ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → U ⁡ U − 2 = U ⁡ W − 2
68 67 eqeq2d ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → W ⁡ W − 2 = U ⁡ U − 2 ↔ W ⁡ W − 2 = U ⁡ W − 2
69 64 68 bitrd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → ⟨“ W ⁡ W − 2 ”⟩ = ⟨“ U ⁡ U − 2 ”⟩ ↔ W ⁡ W − 2 = U ⁡ W − 2
70 fvex ⊢ lastS ⁡ W ∈ V
71 s111 ⊢ lastS ⁡ W ∈ V ∧ lastS ⁡ U ∈ V → ⟨“ lastS ⁡ W ”⟩ = ⟨“ lastS ⁡ U ”⟩ ↔ lastS ⁡ W = lastS ⁡ U
72 70 59 71 sylancr ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 1 < W ∧ W = U → ⟨“ lastS ⁡ W ”⟩ = ⟨“ lastS ⁡ U ”⟩ ↔ lastS ⁡ W = lastS ⁡ U
73 69 72 anbi12d ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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