Metamath Proof Explorer


Theorem swrdf1

Description: Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023)

Ref Expression
Hypotheses swrdf1.w ( 𝜑𝑊 ∈ Word 𝐷 )
swrdf1.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
swrdf1.n ( 𝜑𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
swrdf1.1 ( 𝜑𝑊 : dom 𝑊1-1𝐷 )
Assertion swrdf1 ( 𝜑 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) –1-1𝐷 )

Proof

Step Hyp Ref Expression
1 swrdf1.w ( 𝜑𝑊 ∈ Word 𝐷 )
2 swrdf1.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
3 swrdf1.n ( 𝜑𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 swrdf1.1 ( 𝜑𝑊 : dom 𝑊1-1𝐷 )
5 swrdf ( ( 𝑊 ∈ Word 𝐷𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁𝑀 ) ) ⟶ 𝐷 )
6 1 2 3 5 syl3anc ( 𝜑 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁𝑀 ) ) ⟶ 𝐷 )
7 6 ffdmd ( 𝜑 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⟶ 𝐷 )
8 fzossz ( 0 ..^ ( 𝑁𝑀 ) ) ⊆ ℤ
9 simpllr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
10 6 fdmd ( 𝜑 → dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 0 ..^ ( 𝑁𝑀 ) ) )
11 10 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 0 ..^ ( 𝑁𝑀 ) ) )
12 9 11 eleqtrd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) )
13 8 12 sselid ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 ∈ ℤ )
14 13 zcnd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 ∈ ℂ )
15 simplr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
16 15 11 eleqtrd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) )
17 8 16 sselid ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ ℤ )
18 17 zcnd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ ℂ )
19 2 elfzelzd ( 𝜑𝑀 ∈ ℤ )
20 19 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ℤ )
21 20 zcnd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ℂ )
22 4 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑊 : dom 𝑊1-1𝐷 )
23 elfzuz ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ( ℤ ‘ 0 ) )
24 fzoss1 ( 𝑀 ∈ ( ℤ ‘ 0 ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
25 2 23 24 3syl ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
26 elfzuz3 ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝑁 ) )
27 fzoss2 ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
28 3 26 27 3syl ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 25 28 sstrd ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 29 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 3 elfzelzd ( 𝜑𝑁 ∈ ℤ )
32 31 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑁 ∈ ℤ )
33 fzoaddel2 ( ( 𝑖 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
34 12 32 20 33 syl3anc ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
35 30 34 sseldd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36 wrddm ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37 1 36 syl ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 37 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 35 38 eleqtrrd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ dom 𝑊 )
40 fzoaddel2 ( ( 𝑗 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑗 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
41 16 32 20 40 syl3anc ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
42 30 41 sseldd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
43 42 38 eleqtrrd ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ dom 𝑊 )
44 simpr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) )
45 1 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑊 ∈ Word 𝐷 )
46 2 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
47 3 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
48 swrdfv ( ( ( 𝑊 ∈ Word 𝐷𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
49 45 46 47 12 48 syl31anc ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
50 swrdfv ( ( ( 𝑊 ∈ Word 𝐷𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
51 45 46 47 16 50 syl31anc ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
52 44 49 51 3eqtr3d ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
53 f1veqaeq ( ( 𝑊 : dom 𝑊1-1𝐷 ∧ ( ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) ) → ( ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) ) )
54 53 anassrs ( ( ( 𝑊 : dom 𝑊1-1𝐷 ∧ ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) → ( ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) ) )
55 54 imp ( ( ( ( 𝑊 : dom 𝑊1-1𝐷 ∧ ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) )
56 22 39 43 52 55 syl1111anc ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) )
57 14 18 21 56 addcan2ad ( ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 = 𝑗 )
58 57 ex ( ( ( 𝜑𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
59 58 anasss ( ( 𝜑 ∧ ( 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) → ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
60 59 ralrimivva ( 𝜑 → ∀ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∀ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
61 dff13 ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) –1-1𝐷 ↔ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⟶ 𝐷 ∧ ∀ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∀ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
62 7 60 61 sylanbrc ( 𝜑 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) –1-1𝐷 )