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 sseldi ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 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 sseldi ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ ℤ )
18 17 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑗 ∈ ℂ )
19 fzssz ⊢ ( 0 ... 𝑁 ) ⊆ ℤ
20 19 2 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
21 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ℤ )
22 21 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ℂ )
23 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
24 elfzuz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
25 fzoss1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
26 2 24 25 3syl ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
27 elfzuz3 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
28 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 3 27 28 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 26 29 sstrd ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32 elfzelz ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
33 3 32 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
34 33 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑁 ∈ ℤ )
35 fzoaddel2 ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
36 12 34 21 35 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
37 31 36 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 1 38 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 39 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
41 37 40 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) ∈ dom 𝑊 )
42 fzoaddel2 ⊢ ( ( 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑗 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
43 16 34 21 42 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
44 31 43 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
45 44 40 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑗 + 𝑀 ) ∈ dom 𝑊 )
46 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) )
47 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑊 ∈ Word 𝐷 )
48 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
49 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
50 swrdfv ⊢ ( ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
51 47 48 49 12 50 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
52 swrdfv ⊢ ( ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
53 47 48 49 16 52 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
54 46 51 53 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) )
55 f1veqaeq ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) ) → ( ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) ) )
56 55 anassrs ⊢ ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) → ( ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) ) )
57 56 imp ⊢ ( ( ( ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ ( 𝑖 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑗 + 𝑀 ) ∈ dom 𝑊 ) ∧ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) = ( 𝑊 ‘ ( 𝑗 + 𝑀 ) ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) )
58 23 41 45 54 57 syl1111anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → ( 𝑖 + 𝑀 ) = ( 𝑗 + 𝑀 ) )
59 14 18 22 58 addcan2ad ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) ) → 𝑖 = 𝑗 )
60 59 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) → ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
61 60 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∧ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) → ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
62 61 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∀ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
63 dff13 ⊢ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) –1-1→ 𝐷 ↔ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⟶ 𝐷 ∧ ∀ 𝑖 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∀ 𝑗 ∈ dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
64 7 62 63 sylanbrc ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : dom ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) –1-1→ 𝐷 )