Metamath Proof Explorer

Theorem cshfn

Description: Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018) (Revised by AV, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

Ref Expression
Assertion cshfn ⊢ W ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l ∧ N ∈ ℤ → W cyclShift N = if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ w = W → w = ∅ ↔ W = ∅
2 1 adantr ⊢ w = W ∧ n = N → w = ∅ ↔ W = ∅
3 simpl ⊢ w = W ∧ n = N → w = W
4 simpr ⊢ w = W ∧ n = N → n = N
5 fveq2 ⊢ w = W → w = W
6 5 adantr ⊢ w = W ∧ n = N → w = W
7 4 6 oveq12d ⊢ w = W ∧ n = N → n mod w = N mod W
8 7 6 opeq12d ⊢ w = W ∧ n = N → n mod w w = N mod W W
9 3 8 oveq12d ⊢ w = W ∧ n = N → w substr n mod w w = W substr N mod W W
10 3 7 oveq12d ⊢ w = W ∧ n = N → w prefix n mod w = W prefix N mod W
11 9 10 oveq12d ⊢ w = W ∧ n = N → w substr n mod w w ++ w prefix n mod w = W substr N mod W W ++ W prefix N mod W
12 2 11 ifbieq2d ⊢ w = W ∧ n = N → if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w = if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W
13 df-csh ⊢ cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
14 0ex ⊢ ∅ ∈ V
15 ovex ⊢ W substr N mod W W ++ W prefix N mod W ∈ V
16 14 15 ifex ⊢ if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W ∈ V
17 12 13 16 ovmpoa ⊢ W ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l ∧ N ∈ ℤ → W cyclShift N = if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W