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