---

Step * 1 1 of Lemma princ_ideal_mem_cond


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

1
1. r : CRng
2. u : |r|
3. v : |r|
4. c : |r|
5. (c * v) = u ∈ |r|
⊢ u = (v * c) ∈ |r|

---

Latex:

---

Latex:

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


By

---

Latex:
D  4  THEN  With  c  (D  0)  THENA  Auto

---

Home Index