Metamath Proof Explorer


Theorem cshimadifsn

Description: The image of a cyclically shifted word under its domain without its left 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 cshimadifsn ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 wrdfn ( 𝐹 ∈ Word 𝑆𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
2 fnfun ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → Fun 𝐹 )
3 1 2 syl ( 𝐹 ∈ Word 𝑆 → Fun 𝐹 )
4 3 3ad2ant1 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → Fun 𝐹 )
5 wrddm ( 𝐹 ∈ Word 𝑆 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6 difssd ( ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∖ { 𝐽 } ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
7 oveq2 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
8 7 difeq1d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) = ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∖ { 𝐽 } ) )
9 8 adantl ( ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) = ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∖ { 𝐽 } ) )
10 simpl ( ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ) → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
11 6 9 10 3sstr4d ( ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 )
12 11 a1d ( ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 = ( ♯ ‘ 𝐹 ) ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 ) )
13 12 ex ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 ) ) )
14 5 13 syl ( 𝐹 ∈ Word 𝑆 → ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 ) ) )
15 14 3imp ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 )
16 4 15 jca ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( Fun 𝐹 ∧ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 ) )
17 dfimafn ( ( Fun 𝐹 ∧ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ⊆ dom 𝐹 ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ( 𝐹𝑥 ) = 𝑧 } )
18 16 17 syl ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ( 𝐹𝑥 ) = 𝑧 } )
19 modsumfzodifsn ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) )
20 19 3ad2antl3 ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) )
21 oveq2 ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) )
22 21 eqcoms ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) )
23 22 eleq1d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ↔ ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) )
24 23 3ad2ant2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ↔ ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) )
25 24 adantr ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ↔ ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) )
26 20 25 mpbird ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) )
27 modfzo0difsn ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) )
28 27 3ad2antl3 ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) )
29 oveq2 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 𝑦 + 𝐽 ) mod 𝑁 ) = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) )
30 29 eqcomd ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) )
31 30 eqeq2d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ↔ 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ) )
32 31 rexbidv ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ↔ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ) )
33 32 3ad2ant2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ↔ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ) )
34 33 adantr ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ↔ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod 𝑁 ) ) )
35 28 34 mpbird ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) )
36 fveq2 ( 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
37 36 3ad2ant3 ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
38 simpl1 ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝐹 ∈ Word 𝑆 )
39 elfzoelz ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
40 39 3ad2ant3 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → 𝐽 ∈ ℤ )
41 40 adantr ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝐽 ∈ ℤ )
42 oveq2 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 1 ..^ 𝑁 ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
43 42 eleq2d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑦 ∈ ( 1 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
44 fzo0ss1 ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
45 44 sseli ( 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
46 43 45 syl6bi ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
47 46 3ad2ant2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
48 47 imp ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
49 cshwidxmod ( ( 𝐹 ∈ Word 𝑆𝐽 ∈ ℤ ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) )
50 49 eqcomd ( ( 𝐹 ∈ Word 𝑆𝐽 ∈ ℤ ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) )
51 38 41 48 50 syl3anc ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) )
52 51 3adant3 ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) )
53 37 52 eqtrd ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹𝑥 ) = ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) )
54 53 eqeq1d ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 = ( ( 𝑦 + 𝐽 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹𝑥 ) = 𝑧 ↔ ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = 𝑧 ) )
55 26 35 54 rexxfrd2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ∃ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ( 𝐹𝑥 ) = 𝑧 ↔ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = 𝑧 ) )
56 55 abbidv ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ( 𝐹𝑥 ) = 𝑧 } = { 𝑧 ∣ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = 𝑧 } )
57 39 anim2i ( ( 𝐹 ∈ Word 𝑆𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆𝐽 ∈ ℤ ) )
58 57 3adant2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ∈ Word 𝑆𝐽 ∈ ℤ ) )
59 cshwfn ( ( 𝐹 ∈ Word 𝑆𝐽 ∈ ℤ ) → ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
60 58 59 syl ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
61 fnfun ( ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → Fun ( 𝐹 cyclShift 𝐽 ) )
62 61 adantl ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun ( 𝐹 cyclShift 𝐽 ) )
63 42 44 eqsstrdi ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
64 63 3ad2ant2 ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
65 64 adantr ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
66 fndm ( ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → dom ( 𝐹 cyclShift 𝐽 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
67 66 adantl ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom ( 𝐹 cyclShift 𝐽 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
68 65 67 sseqtrrd ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) )
69 62 68 jca ( ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐹 cyclShift 𝐽 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) )
70 60 69 mpdan ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) )
71 dfimafn ( ( Fun ( 𝐹 cyclShift 𝐽 ) ∧ ( 1 ..^ 𝑁 ) ⊆ dom ( 𝐹 cyclShift 𝐽 ) ) → ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = 𝑧 } )
72 70 71 syl ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) ( ( 𝐹 cyclShift 𝐽 ) ‘ 𝑦 ) = 𝑧 } )
73 56 72 eqtr4d ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ( 𝐹𝑥 ) = 𝑧 } = ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) )
74 18 73 eqtrd ( ( 𝐹 ∈ Word 𝑆𝑁 = ( ♯ ‘ 𝐹 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) = ( ( 𝐹 cyclShift 𝐽 ) “ ( 1 ..^ 𝑁 ) ) )