---

Step * 1 1 of Lemma rng_times_zero

.....assertion..... 
1. r : Rng
2. a : |r|
⊢ (((0 +r 0) * a) = (0 * a) ∈ |r|) ∧ ((a * (0 +r 0)) = (a * 0) ∈ |r|)
BY
{ (Auto THEN EqCD THEN Auto THEN RW RngPlusGrpNormC 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  Rng
2.  a  :  |r|
\mvdash{}  (((0  +r  0)  *  a)  =  (0  *  a))  \mwedge{}  ((a  *  (0  +r  0))  =  (a  *  0))


By

---

Latex:
(Auto  THEN  EqCD  THEN  Auto  THEN  RW  RngPlusGrpNormC  0  THEN  Auto)

---

Home Index