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 biimtrdi ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑦 ∈ ( 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 ..^ 𝑁 ) ) )