---

Step * 1 2 1 2 of Lemma zero_ideal_wf


1. r : CRng
2. 0 = 0 ∈ |r|
3. ∀a:|r|. ((a = 0 ∈ |r|) ⇒ ((-r a) = 0 ∈ |r|))
4. a : |r|
5. b : |r|
6. a = 0 ∈ |r|
7. b = 0 ∈ |r|
⊢ (a +r b) = 0 ∈ |r|
BY
{ ((HypSubst' -1 0 THEN HypSubst' -2 0) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  0  =  0
3.  \mforall{}a:|r|.  ((a  =  0)  {}\mRightarrow{}  ((-r  a)  =  0))
4.  a  :  |r|
5.  b  :  |r|
6.  a  =  0
7.  b  =  0
\mvdash{}  (a  +r  b)  =  0


By

---

Latex:
((HypSubst'  -1  0  THEN  HypSubst'  -2  0)  THEN  Auto)

---

Home Index