---

Step * 1 1 of Lemma rng_times_sum_r


1. r : Rng
2. a : ℤ
3. b : {a...}
4. ∀[j:{a..b-}]. ∀[E:{a..j-} ⟶ |r|]. ∀[u:|r|].  (((Σ(r) a ≤ j < j. E[j]) * u) = (Σ(r) a ≤ j < j. E[j] * u) ∈ |r|)
5. E : {a..b-} ⟶ |r|
6. u : |r|
⊢ ((Σ(r) a ≤ j < b. E[j]) * u) = (Σ(r) a ≤ j < b. E[j] * u) ∈ |r|
BY
{ ((Decide a = b ∈ ℤ THENA Auto)
   THENL [(((RWH (LemmaC `rng_sum_unroll_base`) 0) THENA Auto)   THEN ((RW RngNormC 0) THEN Auto))⋅
         ; ((RWH (LemmaC `rng_sum_unroll_hi`) 0) THENA Auto) 
         THEN ((RWH (RevHypC 4) 0) THENA Auto) 
         THEN ((RW RngNormC 0) THEN Auto)]
)⋅ }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  a  :  \mBbbZ{}
3.  b  :  \{a...\}
4.  \mforall{}[j:\{a..b\msupminus{}\}].  \mforall{}[E:\{a..j\msupminus{}\}  {}\mrightarrow{}  |r|].  \mforall{}[u:|r|].
          (((\mSigma{}(r)  a  \mleq{}  j  <  j.  E[j])  *  u)  =  (\mSigma{}(r)  a  \mleq{}  j  <  j.  E[j]  *  u))
5.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  |r|
6.  u  :  |r|
\mvdash{}  ((\mSigma{}(r)  a  \mleq{}  j  <  b.  E[j])  *  u)  =  (\mSigma{}(r)  a  \mleq{}  j  <  b.  E[j]  *  u)


By

---

Latex:
((Decide  a  =  b  THENA  Auto)
  THENL  [(((RWH  (LemmaC  `rng\_sum\_unroll\_base`)  0)  THENA  Auto)      THEN  ((RW  RngNormC  0)  THEN  Auto))\mcdot{}
              ;  ((RWH  (LemmaC  `rng\_sum\_unroll\_hi`)  0)  THENA  Auto) 
              THEN  ((RWH  (RevHypC  4)  0)  THENA  Auto) 
              THEN  ((RW  RngNormC  0)  THEN  Auto)]
)\mcdot{}

---

Home Index