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∈WordV∧U∈WordV∧0<W→W=U↔W=U∧WprefixW−1=UprefixW−1∧lastS⁡W=lastS⁡U

Proof

Step Hyp Ref Expression
1 hashgt0n0 ⊢W∈WordV∧0<W→W≠∅
2 lennncl ⊢W∈WordV∧W≠∅→W∈ℕ
3 1 2 syldan ⊢W∈WordV∧0<W→W∈ℕ
4 3 3adant2 ⊢W∈WordV∧U∈WordV∧0<W→W∈ℕ
5 fzo0end ⊢W∈ℕ→W−1∈0..^W
6 4 5 syl ⊢W∈WordV∧U∈WordV∧0<W→W−1∈0..^W
7 pfxsuffeqwrdeq ⊢W∈WordV∧U∈WordV∧W−1∈0..^W→W=U↔W=U∧WprefixW−1=UprefixW−1∧WsubstrW−1W=UsubstrW−1W
8 6 7 syld3an3 ⊢W∈WordV∧U∈WordV∧0<W→W=U↔W=U∧WprefixW−1=UprefixW−1∧WsubstrW−1W=UsubstrW−1W
9 hashneq0 ⊢W∈WordV→0<W↔W≠∅
10 9 biimpd ⊢W∈WordV→0<W→W≠∅
11 10 imdistani ⊢W∈WordV∧0<W→W∈WordV∧W≠∅
12 11 3adant2 ⊢W∈WordV∧U∈WordV∧0<W→W∈WordV∧W≠∅
13 12 adantr ⊢W∈WordV∧U∈WordV∧0<W∧W=U→W∈WordV∧W≠∅
14 swrdlsw ⊢W∈WordV∧W≠∅→WsubstrW−1W=⟨“lastS⁡W”⟩
15 13 14 syl ⊢W∈WordV∧U∈WordV∧0<W∧W=U→WsubstrW−1W=⟨“lastS⁡W”⟩
16 breq2 ⊢W=U→0<W↔0<U
17 16 3anbi3d ⊢W=U→W∈WordV∧U∈WordV∧0<W↔W∈WordV∧U∈WordV∧0<U
18 hashneq0 ⊢U∈WordV→0<U↔U≠∅
19 18 biimpd ⊢U∈WordV→0<U→U≠∅
20 19 imdistani ⊢U∈WordV∧0<U→U∈WordV∧U≠∅
21 20 3adant1 ⊢W∈WordV∧U∈WordV∧0<U→U∈WordV∧U≠∅
22 swrdlsw ⊢U∈WordV∧U≠∅→UsubstrU−1U=⟨“lastS⁡U”⟩
23 21 22 syl ⊢W∈WordV∧U∈WordV∧0<U→UsubstrU−1U=⟨“lastS⁡U”⟩
24 17 23 syl6bi ⊢W=U→W∈WordV∧U∈WordV∧0<W→UsubstrU−1U=⟨“lastS⁡U”⟩
25 24 impcom ⊢W∈WordV∧U∈WordV∧0<W∧W=U→UsubstrU−1U=⟨“lastS⁡U”⟩
26 oveq1 ⊢W=U→W−1=U−1
27 id ⊢W=U→W=U
28 26 27 opeq12d ⊢W=U→W−1W=U−1U
29 28 oveq2d ⊢W=U→UsubstrW−1W=UsubstrU−1U
30 29 eqeq1d ⊢W=U→UsubstrW−1W=⟨“lastS⁡U”⟩↔UsubstrU−1U=⟨“lastS⁡U”⟩
31 30 adantl ⊢W∈WordV∧U∈WordV∧0<W∧W=U→UsubstrW−1W=⟨“lastS⁡U”⟩↔UsubstrU−1U=⟨“lastS⁡U”⟩
32 25 31 mpbird ⊢W∈WordV∧U∈WordV∧0<W∧W=U→UsubstrW−1W=⟨“lastS⁡U”⟩
33 15 32 eqeq12d ⊢W∈WordV∧U∈WordV∧0<W∧W=U→WsubstrW−1W=UsubstrW−1W↔⟨“lastS⁡W”⟩=⟨“lastS⁡U”⟩
34 fvexd ⊢W∈WordV∧U∈WordV∧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∈WordV∧U∈WordV∧0<W∧W=U→⟨“lastS⁡W”⟩=⟨“lastS⁡U”⟩↔lastS⁡W=lastS⁡U
38 33 37 bitrd ⊢W∈WordV∧U∈WordV∧0<W∧W=U→WsubstrW−1W=UsubstrW−1W↔lastS⁡W=lastS⁡U
39 38 anbi2d ⊢W∈WordV∧U∈WordV∧0<W∧W=U→WprefixW−1=UprefixW−1∧WsubstrW−1W=UsubstrW−1W↔WprefixW−1=UprefixW−1∧lastS⁡W=lastS⁡U
40 39 pm5.32da ⊢W∈WordV∧U∈WordV∧0<W→W=U∧WprefixW−1=UprefixW−1∧WsubstrW−1W=UsubstrW−1W↔W=U∧WprefixW−1=UprefixW−1∧lastS⁡W=lastS⁡U
41 8 40 bitrd ⊢W∈WordV∧U∈WordV∧0<W→W=U↔W=U∧WprefixW−1=UprefixW−1∧lastS⁡W=lastS⁡U