Metamath Proof Explorer

Theorem cshco

Description: Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018)

Ref Expression
Assertion cshco ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) = ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2 1 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 Fn 𝐴 )
3 cshwfn ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4 3 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 cshwrn ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝐴 )
6 5 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝐴 )
7 fnco ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝐴 ) → ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8 2 4 6 7 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 wrdco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
10 9 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
11 simp2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑁 ∈ ℤ )
12 cshwfn ⊢ ( ( ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
13 10 11 12 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
14 lenco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
15 14 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
16 15 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 16 fneq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ↔ ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
18 13 17 mpbid ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19 15 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
20 19 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) = ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
21 20 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) = ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
22 21 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
23 wrdfn ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
24 23 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
25 24 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
26 elfzoelz ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑖 ∈ ℤ )
27 zaddcl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 + 𝑁 ) ∈ ℤ )
28 26 11 27 syl2anr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑖 + 𝑁 ) ∈ ℤ )
29 elfzo0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝑊 ) ) )
30 29 simp2bi ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
31 30 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
32 zmodfzo ⊢ ( ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
33 28 31 32 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
34 15 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) = ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
35 34 eleq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
36 35 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
37 33 36 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 fvco2 ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
39 25 37 38 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
40 simpl1 ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝐴 )
41 11 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
42 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
43 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
44 43 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
45 40 41 42 44 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
46 22 39 45 3eqtr4rd ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
47 fvco2 ⊢ ( ( ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) ) )
48 4 47 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑖 ) ) )
49 10 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
50 15 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) )
51 50 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
52 51 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
53 52 biimpa ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
54 cshwidxmod ⊢ ( ( ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) → ( ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
55 49 41 53 54 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
56 46 48 55 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) ‘ 𝑖 ) = ( ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) ‘ 𝑖 ) )
57 8 18 56 eqfnfvd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 cyclShift 𝑁 ) ) = ( ( 𝐹 ∘ 𝑊 ) cyclShift 𝑁 ) )