---

Step * 1 of Lemma rng_times_sum_r


1. r : Rng
2. a : ℤ
⊢ ∀[b:ℤ]
    ∀[E:{a..b-} ⟶ |r|]. ∀[u:|r|].  (((Σ(r) a ≤ j < b. E[j]) * u) = (Σ(r) a ≤ j < b. E[j] * u) ∈ |r|) supposing a ≤ b
BY
{ ((BLemma `int_le_to_int_upper_uniform`) THENA Auto) 
THEN ((BLemma `int_upper_ind_uniform`) THENA Auto) 
THEN ((UnivCD) THENA Auto) }

1
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|

---

Latex:

---

Latex:

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


By

---

Latex:
((BLemma  `int\_le\_to\_int\_upper\_uniform`)  THENA  Auto) 
THEN  ((BLemma  `int\_upper\_ind\_uniform`)  THENA  Auto) 
THEN  ((UnivCD)  THENA  Auto)

---

Home Index