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 ⟨ 𝐼 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )