Metamath Proof Explorer

Theorem swrdrn3

Description: Express the range of a subword. Stronger version of swrdrn2 . (Contributed by Thierry Arnoux, 13-Dec-2023)

Ref Expression
Assertion swrdrn3 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
2 fzssz ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℤ
3 simpl3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 2 3 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ℤ )
5 fzssz ⊢ ( 0 ... 𝑁 ) ⊆ ℤ
6 simpl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
7 5 6 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℤ )
8 fzoaddel2 ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
9 1 4 7 8 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
10 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) )
11 simpl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
12 5 11 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℤ )
13 12 zcnd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℂ )
14 simpl3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
15 2 14 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
16 15 zcnd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℂ )
17 13 16 pncan3d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 + ( 𝑁 − 𝑀 ) ) = 𝑁 )
18 17 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ..^ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) = ( 𝑀 ..^ 𝑁 ) )
19 10 18 eleqtrrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ( 𝑀 ..^ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
20 15 12 zsubcld ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
21 fzosubel3 ⊢ ( ( 𝑗 ∈ ( 𝑀 ..^ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ) → ( 𝑗 − 𝑀 ) ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
22 19 20 21 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗 − 𝑀 ) ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
23 simpr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑖 = ( 𝑗 − 𝑀 ) ) → 𝑖 = ( 𝑗 − 𝑀 ) )
24 23 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑖 = ( 𝑗 − 𝑀 ) ) → ( 𝑖 + 𝑀 ) = ( ( 𝑗 − 𝑀 ) + 𝑀 ) )
25 24 eqeq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑖 = ( 𝑗 − 𝑀 ) ) → ( 𝑗 = ( 𝑖 + 𝑀 ) ↔ 𝑗 = ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) )
26 fzossz ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ℤ
27 26 10 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ℤ )
28 27 zcnd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ℂ )
29 28 13 npcand ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑗 − 𝑀 ) + 𝑀 ) = 𝑗 )
30 29 eqcomd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 = ( ( 𝑗 − 𝑀 ) + 𝑀 ) )
31 22 25 30 rspcedvd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) 𝑗 = ( 𝑖 + 𝑀 ) )
32 eqcom ⊢ ( 𝑦 = ( 𝑊 ‘ 𝑗 ) ↔ ( 𝑊 ‘ 𝑗 ) = 𝑦 )
33 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 = ( 𝑖 + 𝑀 ) ) → 𝑗 = ( 𝑖 + 𝑀 ) )
34 33 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 = ( 𝑖 + 𝑀 ) ) → ( 𝑊 ‘ 𝑗 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
35 34 eqeq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 = ( 𝑖 + 𝑀 ) ) → ( 𝑦 = ( 𝑊 ‘ 𝑗 ) ↔ 𝑦 = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
36 32 35 bitr3id ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 = ( 𝑖 + 𝑀 ) ) → ( ( 𝑊 ‘ 𝑗 ) = 𝑦 ↔ 𝑦 = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
37 9 31 36 rexxfrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ∃ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑗 ) = 𝑦 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) 𝑦 = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
38 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
39 fvex ⊢ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ∈ V
40 38 39 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) 𝑦 = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
41 37 40 bitr4di ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ∃ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑗 ) = 𝑦 ↔ 𝑦 ∈ ran ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) ) )
42 wrdf ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
43 42 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
44 43 ffnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
45 elfzuz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
46 45 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
47 fzoss1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
48 46 47 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
49 elfzuz3 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
50 49 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
51 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
52 50 51 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
53 48 52 sstrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
54 44 53 fvelimabd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑦 ∈ ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ↔ ∃ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑊 ‘ 𝑗 ) = 𝑦 ) )
55 swrdval2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
56 55 rneqd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ran ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
57 56 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑦 ∈ ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ 𝑦 ∈ ran ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) ) )
58 41 54 57 3bitr4rd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑦 ∈ ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ 𝑦 ∈ ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ) )
59 58 eqrdv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) )