---

Step * of Lemma ringeq-iff-rsub-is-0

No Annotations
∀[r:Rng]. ∀[a,b:|r|].  uiff(a = b ∈ |r|;(a +r (-r b)) = 0 ∈ |r|)
BY
{ Auto }

1
1. r : Rng
2. a : |r|
3. b : |r|
4. (a +r (-r b)) = 0 ∈ |r|
⊢ a = b ∈ |r|

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].    uiff(a  =  b;(a  +r  (-r  b))  =  0)


By

---

Latex:
Auto

---

Home Index