Metamath Proof Explorer

Theorem swrdspsleq

Description: Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Proof shortened by AV, 7-May-2020)

Ref Expression
Assertion swrdspsleq ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 swrdsb0eq ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
2 1 3expa ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
3 2 ancoms ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
4 3 3adantr3 ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
5 ral0 ⊢ ∀ 𝑖 ∈ ∅ ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 )
6 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
7 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
8 fzon ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
9 6 7 8 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
10 9 biimpa ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
11 10 raleqdv ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
12 5 11 mpbiri ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) )
13 12 ex ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑀 → ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
14 13 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑁 ≤ 𝑀 → ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
15 14 impcom ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) )
16 4 15 2thd ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
17 swrdcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 )
18 swrdcl ⊢ ( 𝑈 ∈ Word 𝑉 → ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 )
19 eqwrd ⊢ ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 ∧ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) ) )
20 17 18 19 syl2an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) ) )
21 20 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) ) )
22 21 adantl ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) ) )
23 swrdsbslen ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
24 23 adantl ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
25 24 biantrurd ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) ) )
26 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
27 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
28 ltnle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀 ) )
29 ltle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
30 28 29 sylbird ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
31 26 27 30 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
32 31 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
33 simpl1l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑊 ∈ Word 𝑉 )
34 simpl2l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
35 6 7 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
36 35 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
37 36 anim1i ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) )
38 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) )
39 37 38 sylibr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
40 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
41 39 40 sylibr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
42 34 41 jca ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
43 simpl3l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ≤ ( ♯ ‘ 𝑊 ) )
44 swrdlen2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
45 33 42 43 44 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
46 45 oveq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) = ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
47 46 raleqdv ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
48 0zd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 0 ∈ ℤ )
49 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
50 7 6 49 syl2anr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
51 50 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
52 6 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
53 52 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 𝑀 ∈ ℤ )
54 fzoshftral ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
55 48 51 53 54 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
56 55 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
57 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
58 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
59 addid2 ⊢ ( 𝑀 ∈ ℂ → ( 0 + 𝑀 ) = 𝑀 )
60 59 adantl ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 0 + 𝑀 ) = 𝑀 )
61 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 )
62 60 61 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ..^ 𝑁 ) )
63 57 58 62 syl2anr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ..^ 𝑁 ) )
64 63 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ..^ 𝑁 ) )
65 64 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ..^ 𝑁 ) )
66 65 raleqdv ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑖 ∈ ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
67 ovex ⊢ ( 𝑖 − 𝑀 ) ∈ V
68 sbceqg ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ( [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) )
69 csbfv2g ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ 𝑗 ) )
70 csbvarg ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ 𝑗 = ( 𝑖 − 𝑀 ) )
71 70 fveq2d ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ 𝑗 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) )
72 69 71 eqtrd ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) )
73 csbfv2g ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ 𝑗 ) )
74 70 fveq2d ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) )
75 73 74 eqtrd ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) )
76 72 75 eqeq12d ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ( ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ⦋ ( 𝑖 − 𝑀 ) / 𝑗 ⦌ ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) ) )
77 68 76 bitrd ⊢ ( ( 𝑖 − 𝑀 ) ∈ V → ( [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) ) )
78 67 77 mp1i ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) ) )
79 33 42 43 3jca ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) )
80 swrdfv2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( 𝑊 ‘ 𝑖 ) )
81 79 80 sylan ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( 𝑊 ‘ 𝑖 ) )
82 simpl1r ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑈 ∈ Word 𝑉 )
83 simpl3r ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ≤ ( ♯ ‘ 𝑈 ) )
84 82 42 83 3jca ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) )
85 swrdfv2 ⊢ ( ( ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( 𝑈 ‘ 𝑖 ) )
86 84 85 sylan ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( 𝑈 ‘ 𝑖 ) )
87 81 86 eqeq12d ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ ( 𝑖 − 𝑀 ) ) ↔ ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
88 78 87 bitrd ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
89 88 ralbidva ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
90 66 89 bitrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑖 ∈ ( ( 0 + 𝑀 ) ..^ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) [ ( 𝑖 − 𝑀 ) / 𝑗 ] ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
91 47 56 90 3bitrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
92 91 ex ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑀 ≤ 𝑁 → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
93 32 92 syld ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ¬ 𝑁 ≤ 𝑀 → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
94 93 impcom ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
95 22 25 94 3bitr2d ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
96 16 95 pm2.61ian ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ∀ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )