---

Step * 1 2 of Lemma rng_times_zero


1. r : Rng
2. a : |r|
3. (((0 +r 0) * a) = (0 * a) ∈ |r|) ∧ ((a * (0 +r 0)) = (a * 0) ∈ |r|)
⊢ ((0 * a) = 0 ∈ |r|) ∧ ((a * 0) = 0 ∈ |r|)
BY
{ ((RWH (GenLemmaC 1 `rng_times_over_plus`  
     ORELSEC GenLemmaC 2 `rng_times_over_plus`) 3) THENA Auto) }

1
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) = 0 ∈ |r|) ∧ ((a * 0) = 0 ∈ |r|)

---

Latex:

---

Latex:

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


By

---

Latex:
((RWH  (GenLemmaC  1  `rng\_times\_over\_plus`   
          ORELSEC  GenLemmaC  2  `rng\_times\_over\_plus`)  3)  THENA  Auto)

---

Home Index