Metamath Proof Explorer

Theorem pfxsuffeqwrdeq

Description: Two words are equal if and only if they have the same prefix and the same suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018) (Revised by AV, 5-May-2020)

Ref Expression
Assertion pfxsuffeqwrdeq ⊢W∈WordV∧S∈WordV∧I∈0..^W→W=S↔W=S∧WprefixI=SprefixI∧WsubstrIW=SsubstrIW

Proof

Step Hyp Ref Expression
1 eqwrd ⊢W∈WordV∧S∈WordV→W=S↔W=S∧∀i∈0..^WW⁡i=S⁡i
2 1 3adant3 ⊢W∈WordV∧S∈WordV∧I∈0..^W→W=S↔W=S∧∀i∈0..^WW⁡i=S⁡i
3 elfzofz ⊢I∈0..^W→I∈0…W
4 fzosplit ⊢I∈0…W→0..^W=0..^I∪I..^W
5 3 4 syl ⊢I∈0..^W→0..^W=0..^I∪I..^W
6 5 3ad2ant3 ⊢W∈WordV∧S∈WordV∧I∈0..^W→0..^W=0..^I∪I..^W
7 6 adantr ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→0..^W=0..^I∪I..^W
8 7 raleqdv ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→∀i∈0..^WW⁡i=S⁡i↔∀i∈0..^I∪I..^WW⁡i=S⁡i
9 ralunb ⊢∀i∈0..^I∪I..^WW⁡i=S⁡i↔∀i∈0..^IW⁡i=S⁡i∧∀i∈I..^WW⁡i=S⁡i
10 8 9 bitrdi ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→∀i∈0..^WW⁡i=S⁡i↔∀i∈0..^IW⁡i=S⁡i∧∀i∈I..^WW⁡i=S⁡i
11 eqidd ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I=I
12 3simpa ⊢W∈WordV∧S∈WordV∧I∈0..^W→W∈WordV∧S∈WordV
13 12 adantr ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→W∈WordV∧S∈WordV
14 elfzonn0 ⊢I∈0..^W→I∈ℕ0
15 14 14 jca ⊢I∈0..^W→I∈ℕ0∧I∈ℕ0
16 15 3ad2ant3 ⊢W∈WordV∧S∈WordV∧I∈0..^W→I∈ℕ0∧I∈ℕ0
17 16 adantr ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I∈ℕ0∧I∈ℕ0
18 elfzo0le ⊢I∈0..^W→I≤W
19 18 3ad2ant3 ⊢W∈WordV∧S∈WordV∧I∈0..^W→I≤W
20 19 adantr ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I≤W
21 breq2 ⊢W=S→I≤W↔I≤S
22 21 adantl ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I≤W↔I≤S
23 20 22 mpbid ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I≤S
24 pfxeq ⊢W∈WordV∧S∈WordV∧I∈ℕ0∧I∈ℕ0∧I≤W∧I≤S→WprefixI=SprefixI↔I=I∧∀i∈0..^IW⁡i=S⁡i
25 13 17 20 23 24 syl112anc ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→WprefixI=SprefixI↔I=I∧∀i∈0..^IW⁡i=S⁡i
26 11 25 mpbirand ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→WprefixI=SprefixI↔∀i∈0..^IW⁡i=S⁡i
27 lencl ⊢W∈WordV→W∈ℕ0
28 27 14 anim12ci ⊢W∈WordV∧I∈0..^W→I∈ℕ0∧W∈ℕ0
29 28 3adant2 ⊢W∈WordV∧S∈WordV∧I∈0..^W→I∈ℕ0∧W∈ℕ0
30 29 adantr ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→I∈ℕ0∧W∈ℕ0
31 27 nn0red ⊢W∈WordV→W∈ℝ
32 31 leidd ⊢W∈WordV→W≤W
33 32 adantr ⊢W∈WordV∧W=S→W≤W
34 eqle ⊢W∈ℝ∧W=S→W≤S
35 31 34 sylan ⊢W∈WordV∧W=S→W≤S
36 33 35 jca ⊢W∈WordV∧W=S→W≤W∧W≤S
37 36 3ad2antl1 ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→W≤W∧W≤S
38 swrdspsleq ⊢W∈WordV∧S∈WordV∧I∈ℕ0∧W∈ℕ0∧W≤W∧W≤S→WsubstrIW=SsubstrIW↔∀i∈I..^WW⁡i=S⁡i
39 13 30 37 38 syl3anc ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→WsubstrIW=SsubstrIW↔∀i∈I..^WW⁡i=S⁡i
40 26 39 anbi12d ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→WprefixI=SprefixI∧WsubstrIW=SsubstrIW↔∀i∈0..^IW⁡i=S⁡i∧∀i∈I..^WW⁡i=S⁡i
41 10 40 bitr4d ⊢W∈WordV∧S∈WordV∧I∈0..^W∧W=S→∀i∈0..^WW⁡i=S⁡i↔WprefixI=SprefixI∧WsubstrIW=SsubstrIW
42 41 pm5.32da ⊢W∈WordV∧S∈WordV∧I∈0..^W→W=S∧∀i∈0..^WW⁡i=S⁡i↔W=S∧WprefixI=SprefixI∧WsubstrIW=SsubstrIW
43 2 42 bitrd ⊢W∈WordV∧S∈WordV∧I∈0..^W→W=S↔W=S∧WprefixI=SprefixI∧WsubstrIW=SsubstrIW