Metamath Proof Explorer

Theorem cshimadifsn0

Description: The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021)

Ref Expression
Assertion cshimadifsn0 ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) “ ( 0 ..^ ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 cshimadifsn ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) )
2 elfzoel2 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
3 elfzom1elp1fzo1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) )
4 3 ex ⊢ ( 𝑁 ∈ ℤ → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) ) )
5 2 4 syl ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) ) )
6 5 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) ) )
7 6 imp ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) )
8 elfzo1elm1fzo0 ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑁 ) → ( 𝑥 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
9 8 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑥 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
10 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( 𝑦 + 1 ) = ( ( 𝑥 − 1 ) + 1 ) )
11 10 eqeq2d ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( 𝑥 = ( 𝑦 + 1 ) ↔ 𝑥 = ( ( 𝑥 − 1 ) + 1 ) ) )
12 11 adantl ⊢ ( ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) ∧ 𝑦 = ( 𝑥 − 1 ) ) → ( 𝑥 = ( 𝑦 + 1 ) ↔ 𝑥 = ( ( 𝑥 − 1 ) + 1 ) ) )
13 elfzoelz ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
14 13 zcnd ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑁 ) → 𝑥 ∈ ℂ )
15 npcan1 ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 − 1 ) + 1 ) = 𝑥 )
16 14 15 syl ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑥 − 1 ) + 1 ) = 𝑥 )
17 16 eqcomd ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑁 ) → 𝑥 = ( ( 𝑥 − 1 ) + 1 ) )
18 17 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) → 𝑥 = ( ( 𝑥 − 1 ) + 1 ) )
19 9 12 18 rspcedvd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) → ∃ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) 𝑥 = ( 𝑦 + 1 ) )
20 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) )
21 20 3ad2ant3 ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) )
22 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
23 22 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑦 ∈ ℂ )
24 23 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℂ )
25 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
26 25 zcnd ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℂ )
27 26 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → 𝐽 ∈ ℂ )
28 27 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐽 ∈ ℂ )
29 1cnd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
30 add32r ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑦 + ( 𝐽 + 1 ) ) = ( ( 𝑦 + 1 ) + 𝐽 ) )
31 24 28 29 30 syl3anc ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + ( 𝐽 + 1 ) ) = ( ( 𝑦 + 1 ) + 𝐽 ) )
32 31 fvoveq1d ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑦 + ( 𝐽 + 1 ) ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( ( 𝑦 + 1 ) + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
33 simpl1 ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐹 ∈ Word 𝑆 )
34 25 peano2zd ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ℤ )
35 34 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐽 + 1 ) ∈ ℤ )
36 35 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐽 + 1 ) ∈ ℤ )
37 fzossrbm1 ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
38 2 37 syl ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
39 38 sseld ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) ) )
40 39 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) ) )
41 40 imp ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
42 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
43 42 eleq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
44 43 3ad2ant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
45 44 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
46 41 45 mpbid ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
47 cshwidxmod ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ ( 𝐽 + 1 ) ∈ ℤ ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑦 + ( 𝐽 + 1 ) ) mod ( ♯ ‘ 𝐹 ) ) ) )
48 33 36 46 47 syl3anc ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑦 + ( 𝐽 + 1 ) ) mod ( ♯ ‘ 𝐹 ) ) ) )
49 25 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → 𝐽 ∈ ℤ )
50 49 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐽 ∈ ℤ )
51 fzo0ss1 ⊢ ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 )
52 2 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
53 52 3 sylan ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 1 ..^ 𝑁 ) )
54 51 53 sselid ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
55 42 eleq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 𝑦 + 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑦 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
56 55 3ad2ant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 + 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑦 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
57 56 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑦 + 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑦 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
58 54 57 mpbid ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
59 cshwidxmod ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ‘ ( ( ( 𝑦 + 1 ) + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
60 33 50 58 59 syl3anc ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ‘ ( ( ( 𝑦 + 1 ) + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
61 32 48 60 3eqtr4rd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) )
62 61 3adant3 ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ ( 𝑦 + 1 ) ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) )
63 21 62 eqtrd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) )
64 63 eqeq1d ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = 𝑧 ↔ ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = 𝑧 ) )
65 7 19 64 rexxfrd2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ∃ 𝑥 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = 𝑧 ↔ ∃ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = 𝑧 ) )
66 65 abbidv ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = 𝑧 } = { 𝑧 ∣ ∃ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = 𝑧 } )
67 25 anim2i ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ) )
68 67 3adant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ) )
69 cshwfn ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ) → ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
70 68 69 syl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
71 fnfun ⊢ ( ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → Fun ( 𝐹 cyclShift 𝐽 ) )
72 71 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun ( 𝐹 cyclShift 𝐽 ) )
73 42 3ad2ant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
74 51 73 sseqtrid ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
75 74 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
76 fndm ⊢ ( ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → dom ( 𝐹 cyclShift 𝐽 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
77 76 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom ( 𝐹 cyclShift 𝐽 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
78 75 77 sseqtrrd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) )
79 72 78 jca ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) )
80 70 79 mpdan ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) )
81 dfimafn ⊢ ( ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) → ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = 𝑧 } )
82 80 81 syl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑥 ) = 𝑧 } )
83 34 anim2i ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆 ∧ ( 𝐽 + 1 ) ∈ ℤ ) )
84 83 3adant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆 ∧ ( 𝐽 + 1 ) ∈ ℤ ) )
85 cshwfn ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ ( 𝐽 + 1 ) ∈ ℤ ) → ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
86 84 85 syl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
87 fnfun ⊢ ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → Fun ( 𝐹 cyclShift ( 𝐽 + 1 ) ) )
88 87 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun ( 𝐹 cyclShift ( 𝐽 + 1 ) ) )
89 38 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
90 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 ) )
91 90 eqcoms ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 ) )
92 91 3ad2ant2 ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 ) )
93 89 92 sseqtrrd ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
94 93 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
95 fndm ⊢ ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
96 95 adantl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
97 94 96 sseqtrrd ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) )
98 88 97 jca ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift ( 𝐽 + 1 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( Fun ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ∧ ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ) )
99 86 98 mpdan ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( Fun ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ∧ ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ) )
100 dfimafn ⊢ ( ( Fun ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ∧ ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ dom ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ) → ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) “ ( 0 ..^ ( 𝑁 − 1 ) ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = 𝑧 } )
101 99 100 syl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) “ ( 0 ..^ ( 𝑁 − 1 ) ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) ‘ 𝑦 ) = 𝑧 } )
102 66 82 101 3eqtr4d ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) “ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
103 1 102 eqtrd ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = ( ( 𝐹 cyclShift ( 𝐽 + 1 ) ) “ ( 0 ..^ ( 𝑁 − 1 ) ) ) )