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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ 0 < W → W ≠ ∅
2 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
3 1 2 syldan ⊢ W ∈ Word V ∧ 0 < W → W ∈ ℕ
4 3 3adant2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W → W ∈ ℕ
5 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
6 4 5 syl ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W → W − 1 ∈ 0 ..^ W
7 pfxsuffeqwrdeq ⊢ W ∈ Word V ∧ U ∈ Word V ∧ W − 1 ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V → 0 < W ↔ W ≠ ∅
10 9 biimpd ⊢ W ∈ Word V → 0 < W → W ≠ ∅
11 10 imdistani ⊢ W ∈ Word V ∧ 0 < W → W ∈ Word V ∧ W ≠ ∅
12 11 3adant2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W → W ∈ Word V ∧ W ≠ ∅
13 12 adantr ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → W ∈ Word V ∧ W ≠ ∅
14 swrdlsw ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W = ⟨“ lastS ⁡ W ”⟩
15 13 14 syl ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 0 < W ↔ W ∈ Word V ∧ U ∈ Word V ∧ 0 < U
18 hashneq0 ⊢ U ∈ Word V → 0 < U ↔ U ≠ ∅
19 18 biimpd ⊢ U ∈ Word V → 0 < U → U ≠ ∅
20 19 imdistani ⊢ U ∈ Word V ∧ 0 < U → U ∈ Word V ∧ U ≠ ∅
21 20 3adant1 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < U → U ∈ Word V ∧ U ≠ ∅
22 swrdlsw ⊢ U ∈ Word V ∧ U ≠ ∅ → U substr U − 1 U = ⟨“ lastS ⁡ U ”⟩
23 21 22 syl ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < U → U substr U − 1 U = ⟨“ lastS ⁡ U ”⟩
24 17 23 biimtrdi ⊢ W = U → W ∈ Word V ∧ U ∈ Word V ∧ 0 < W → U substr U − 1 U = ⟨“ lastS ⁡ U ”⟩
25 24 impcom ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → U substr W − 1 W = ⟨“ lastS ⁡ U ”⟩
33 15 32 eqeq12d ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → W substr W − 1 W = U substr W − 1 W ↔ ⟨“ lastS ⁡ W ”⟩ = ⟨“ lastS ⁡ U ”⟩
34 fvexd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → lastS ⁡ W ∈ V
35 fvex ⊢ lastS ⁡ U ∈ V
36 s111 ⊢ lastS ⁡ W ∈ V ∧ lastS ⁡ U ∈ V → ⟨“ lastS ⁡ W ”⟩ = ⟨“ lastS ⁡ U ”⟩ ↔ lastS ⁡ W = lastS ⁡ U
37 34 35 36 sylancl ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → ⟨“ lastS ⁡ W ”⟩ = ⟨“ lastS ⁡ U ”⟩ ↔ lastS ⁡ W = lastS ⁡ U
38 33 37 bitrd ⊢ W ∈ Word V ∧ U ∈ Word V ∧ 0 < W ∧ W = U → W substr W − 1 W = U substr W − 1 W ↔ lastS ⁡ W = lastS ⁡ U
39 38 anbi2d ⊢ W ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ 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 ∈ Word V ∧ U ∈ Word V ∧ 0 < W → W = U ↔ W = U ∧ W prefix W − 1 = U prefix W − 1 ∧ lastS ⁡ W = lastS ⁡ U