---

Step * 1 2 of Lemma princ_ideal_mem_cond


1. r : CRng
2. u : |r|
3. v : |r|
4. ∃b:|r|. (u = (v * b) ∈ |r|)
⊢ ∃c:|r|. ((c * v) = u ∈ |r|)
BY
{ (ParallelLast THEN D 1 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  u  :  |r|
3.  v  :  |r|
4.  \mexists{}b:|r|.  (u  =  (v  *  b))
\mvdash{}  \mexists{}c:|r|.  ((c  *  v)  =  u)


By

---

Latex:
(ParallelLast  THEN  D  1  THEN  Auto)

---

Home Index