---

Step * of Lemma ideal_of_prime

∀r:CRng. ∀u:|r|.  (r-Prime(u) ⇐⇒ IsPrimeIdeal(r;(u)r))
BY
{ UnivCD 
THENM Unfold `prime_ideal_p` 0 
THENA Auto }

1
1. r : CRng@i'
2. u : |r|@i
⊢ r-Prime(u) ⇐⇒ (¬((u)r 1)) ∧ (∀a,b:|r|.  (((u)r (a * b)) ⇒ (((u)r a) ∨ ((u)r b))))

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}u:|r|.    (r-Prime(u)  \mLeftarrow{}{}\mRightarrow{}  IsPrimeIdeal(r;(u)r))


By

---

Latex:
UnivCD 
THENM  Unfold  `prime\_ideal\_p`  0 
THENA  Auto

---

Home Index