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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hashgt0n0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )
2 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
3 1 2 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
4 3 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
5 fzo0end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 4 5 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 pfxsuffeqwrdeq ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
8 6 7 syld3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
9 hashneq0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
10 9 biimpd ⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) → 𝑊 ≠ ∅ ) )
11 10 imdistani ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
12 11 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
13 12 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
14 swrdlsw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑊 ) ”⟩ )
15 13 14 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑊 ) ”⟩ )
16 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( ♯ ‘ 𝑈 ) ) )
17 16 3anbi3d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑈 ) ) ) )
18 hashneq0 ⊢ ( 𝑈 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 𝑈 ≠ ∅ ) )
19 18 biimpd ⊢ ( 𝑈 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑈 ) → 𝑈 ≠ ∅ ) )
20 19 imdistani ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑈 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅ ) )
21 20 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑈 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅ ) )
22 swrdlsw ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅ ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ )
23 21 22 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ )
24 17 23 syl6bi ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
25 24 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ )
26 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
27 id ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )
28 26 27 opeq12d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ = ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ )
29 28 oveq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) )
30 29 eqeq1d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
31 30 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑈 ) − 1 ) , ( ♯ ‘ 𝑈 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
32 25 31 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ )
33 15 32 eqeq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
34 fvexd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( lastS ‘ 𝑊 ) ∈ V )
35 fvex ⊢ ( lastS ‘ 𝑈 ) ∈ V
36 s111 ⊢ ( ( ( lastS ‘ 𝑊 ) ∈ V ∧ ( lastS ‘ 𝑈 ) ∈ V ) → ( ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) )
37 34 35 36 sylancl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ↔ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) )
38 33 37 bitrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) )
39 38 anbi2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ↔ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) )
40 39 pm5.32da ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑈 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )
41 8 40 bitrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = 𝑈 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∧ ( lastS ‘ 𝑊 ) = ( lastS ‘ 𝑈 ) ) ) ) )