---

Step * 1 of Lemma ring_triv


1. r : Rng
2. 1 = 0 ∈ |r|
3. a : |r|
⊢ a = 0 ∈ |r|
BY
{ ((ApFunToHypEquands `b' a * b |r| 2 
THENM RW RngNormC (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  1  =  0
3.  a  :  |r|
\mvdash{}  a  =  0


By

---

Latex:
((ApFunToHypEquands  `b'  a  *  b  |r|  2 
THENM  RW  RngNormC  (-1))  THEN  Auto)

---

Home Index