---

Step * 1 of Lemma rng_times_sum_l


1. r : Rng
2. a : ℤ
⊢ ∀[b:ℤ]
    ∀[E:{a..b-} ⟶ |r|]. ∀[u:|r|].  ((u * (Σ(r) a ≤ j < b. E[j])) = (Σ(r) a ≤ j < b. u * E[j]) ∈ |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|].  ((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|

---

Latex:

---

Latex:

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