---

Step * 1 1 2 1 of Lemma rng_lsum-partition


1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. m : ℤ
8. 0 < m
9. m < k
10. f[u] = (Σ(r) 0 ≤ i < k. if (m - 1 =z i) then f[u] else 0 fi ) ∈ |r|
⊢ f[u] = (Σ(r) 0 ≤ i < k. if (m =z i) then f[u] else 0 fi ) ∈ |r|
BY
{ (InstLemma `rng_sum_shift`  [⌜r⌝;⌜0⌝;⌜k⌝;⌜λ2i.if (m - 1 =z i) then f[u] else 0 fi ⌝;⌜1⌝]⋅ THENA Auto) }

1
1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. m : ℤ
8. 0 < m
9. m < k
10. f[u] = (Σ(r) 0 ≤ i < k. if (m - 1 =z i) then f[u] else 0 fi ) ∈ |r|
11. (Σ(r) 0 
          ≤ j 
          < k
      if (m - 1 =z j) then f[u] else 0 fi )
= (Σ(r) 0 + 1 
        ≤ j 
        < k + 1
    if (m - 1 =z j - 1) then f[u] else 0 fi )
∈ |r|
⊢ f[u] = (Σ(r) 0 ≤ i < k. if (m =z i) then f[u] else 0 fi ) ∈ |r|

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbN{}k
4.  r  :  Rng
5.  f  :  A  {}\mrightarrow{}  |r|
6.  u  :  A
7.  m  :  \mBbbZ{}
8.  0  <  m
9.  m  <  k
10.  f[u]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  (m  -  1  =\msubz{}  i)  then  f[u]  else  0  fi  )
\mvdash{}  f[u]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  (m  =\msubz{}  i)  then  f[u]  else  0  fi  )


By

---

Latex:
(InstLemma  `rng\_sum\_shift` 
  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.if  (m  -  1  =\msubz{}  i)  then  f[u]  else  0  fi  \mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index