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 ∈ Word V ∧ S ∈ Word V ∧ I ∈ 0 ..^ W → W = S ↔ W = S ∧ W prefix I = S prefix I ∧ W substr I W = S substr I W

Proof

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