---

Step * 1 2 1 1 of Lemma rng_times_zero

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

---

Latex:

---

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


By

---

Latex:
(Assert  \mkleeneopen{}((0  *  a)  =  ((0  *  a)  +r  0))  \mwedge{}  ((a  *  0)  =  ((a  *  0)  +r  0))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RW  RngPlusGrpNormC  0  THEN  Auto\mcdot{})

---

Home Index