---

Step * 1 1 of Lemma rng_times_sum_l


1. r : Rng
2. a : ℤ
3. b : {a...}
4. ∀[j:{a..b-}]. ∀[E:{a..j-} ⟶ |r|]. ∀[u:|r|].  ((u * (Σ(r) a ≤ j < j. E[j])) = (Σ(r) a ≤ j < j. u * E[j]) ∈ |r|)
5. E : {a..b-} ⟶ |r|
6. u : |r|
⊢ (u * (Σ(r) a ≤ j < b. E[j])) = (Σ(r) a ≤ j < b. u * E[j]) ∈ |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|].
          ((u  *  (\mSigma{}(r)  a  \mleq{}  j  <  j.  E[j]))  =  (\mSigma{}(r)  a  \mleq{}  j  <  j.  u  *  E[j]))
5.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  |r|
6.  u  :  |r|
\mvdash{}  (u  *  (\mSigma{}(r)  a  \mleq{}  j  <  b.  E[j]))  =  (\mSigma{}(r)  a  \mleq{}  j  <  b.  u  *  E[j])


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)]
)

---

Home Index