This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-csh

Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words w e. Word S or at least functions over half-open ranges of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018) (Revised by Mario Carneiro/Alexander van der Vekens/ Gerard Lang, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

Ref Expression
Assertion df-csh cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccsh ⊢ cyclShift
1 vw ⊢ 𝑤
2 vf ⊢ 𝑓
3 vl ⊢ 𝑙
4 cn0 ⊢ ℕ0
5 2 cv ⊢ 𝑓
6 cc0 ⊢ 0
7 cfzo ⊢ ..^
8 3 cv ⊢ 𝑙
9 6 8 7 co ⊢ ( 0 ..^ 𝑙 )
10 5 9 wfn ⊢ 𝑓 Fn ( 0 ..^ 𝑙 )
11 10 3 4 wrex ⊢ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 )
12 11 2 cab ⊢ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) }
13 vn ⊢ 𝑛
14 cz ⊢ ℤ
15 1 cv ⊢ 𝑤
16 c0 ⊢ ∅
17 15 16 wceq ⊢ 𝑤 = ∅
18 csubstr ⊢ substr
19 13 cv ⊢ 𝑛
20 cmo ⊢ mod
21 chash ⊢ ♯
22 15 21 cfv ⊢ ( ♯ ‘ 𝑤 )
23 19 22 20 co ⊢ ( 𝑛 mod ( ♯ ‘ 𝑤 ) )
24 23 22 cop ⊢ ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩
25 15 24 18 co ⊢ ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ )
26 cconcat ⊢ ++
27 cpfx ⊢ prefix
28 15 23 27 co ⊢ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) )
29 25 28 26 co ⊢ ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) )
30 17 16 29 cif ⊢ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) )
31 1 13 12 14 30 cmpo ⊢ ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
32 0 31 wceq ⊢ cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )