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 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = 𝑆 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ∧ ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqwrd ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉 ) → ( 𝑊 = 𝑆 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
2 1 3adant3 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = 𝑆 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
3 elfzofz ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 fzosplit ( 𝐼 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) )
5 3 4 syl ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) )
6 5 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) )
7 6 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) )
8 7 raleqdv ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) )
9 ralunb ( ∀ 𝑖 ∈ ( ( 0 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ∧ ∀ 𝑖 ∈ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) )
10 8 9 bitrdi ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ∧ ∀ 𝑖 ∈ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
11 eqidd ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → 𝐼 = 𝐼 )
12 3simpa ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉 ) )
13 12 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉 ) )
14 elfzonn0 ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℕ0 )
15 14 14 jca ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ∈ ℕ0𝐼 ∈ ℕ0 ) )
16 15 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 ∈ ℕ0𝐼 ∈ ℕ0 ) )
17 16 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( 𝐼 ∈ ℕ0𝐼 ∈ ℕ0 ) )
18 elfzo0le ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ≤ ( ♯ ‘ 𝑊 ) )
19 18 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ≤ ( ♯ ‘ 𝑊 ) )
20 19 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → 𝐼 ≤ ( ♯ ‘ 𝑊 ) )
21 breq2 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) → ( 𝐼 ≤ ( ♯ ‘ 𝑊 ) ↔ 𝐼 ≤ ( ♯ ‘ 𝑆 ) ) )
22 21 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( 𝐼 ≤ ( ♯ ‘ 𝑊 ) ↔ 𝐼 ≤ ( ♯ ‘ 𝑆 ) ) )
23 20 22 mpbid ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → 𝐼 ≤ ( ♯ ‘ 𝑆 ) )
24 pfxeq ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉 ) ∧ ( 𝐼 ∈ ℕ0𝐼 ∈ ℕ0 ) ∧ ( 𝐼 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝐼 ≤ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ↔ ( 𝐼 = 𝐼 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
25 13 17 20 23 24 syl112anc ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ↔ ( 𝐼 = 𝐼 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
26 11 25 mpbirand ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) )
27 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
28 27 14 anim12ci ( ( 𝑊 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
29 28 3adant2 ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
30 29 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
31 27 nn0red ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
32 31 leidd ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑊 ) )
33 32 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑊 ) )
34 eqle ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑆 ) )
35 31 34 sylan ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑆 ) )
36 33 35 jca ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑊 ) ∧ ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑆 ) ) )
37 36 3ad2antl1 ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑊 ) ∧ ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑆 ) ) )
38 swrdspsleq ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉 ) ∧ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑊 ) ∧ ( ♯ ‘ 𝑊 ) ≤ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) )
39 13 30 37 38 syl3anc ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) )
40 26 39 anbi12d ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ∧ ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 𝐼 ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ∧ ∀ 𝑖 ∈ ( 𝐼 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ) )
41 10 40 bitr4d ( ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ↔ ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ∧ ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
42 41 pm5.32da ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑆𝑖 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ∧ ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
43 2 42 bitrd ( ( 𝑊 ∈ Word 𝑉𝑆 ∈ Word 𝑉𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = 𝑆 ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑆 ) ∧ ( ( 𝑊 prefix 𝐼 ) = ( 𝑆 prefix 𝐼 ) ∧ ( 𝑊 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑆 substr ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )