---

Step * 1 of Lemma quot_by_prime_ideal


1. r : CRng
2. p : Ideal(r){i}
3. d : detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
⊢ IsPrimeIdeal(r;p) ⇐⇒ IsIntegDom(r / d)
BY
{ (Unfold `integ_dom_p` 0
   THEN Unfold `nequal` 0⋅
   THEN Assert ⌜IsPrimeIdeal(r;p)
                ⇐⇒ (¬(1 = 0 ∈ |r / d|))
                    ∧ (∀u,v:|r / d|.  ((¬(v = 0 ∈ |r / d|)) ⇒ ((u * v) = 0 ∈ |r / d|) ⇒ (u = 0 ∈ |r / d|)))⌝⋅) }

1
.....assertion..... 
1. r : CRng
2. p : Ideal(r){i}
3. d : detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
⊢ IsPrimeIdeal(r;p)
⇐⇒ (¬(1 = 0 ∈ |r / d|)) ∧ (∀u,v:|r / d|.  ((¬(v = 0 ∈ |r / d|)) ⇒ ((u * v) = 0 ∈ |r / d|) ⇒ (u = 0 ∈ |r / d|)))

2
1. r : CRng
2. p : Ideal(r){i}
3. d : detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
5. IsPrimeIdeal(r;p)
⇐⇒ (¬(1 = 0 ∈ |r / d|)) ∧ (∀u,v:|r / d|.  ((¬(v = 0 ∈ |r / d|)) ⇒ ((u * v) = 0 ∈ |r / d|) ⇒ (u = 0 ∈ |r / d|)))
⊢ IsPrimeIdeal(r;p)
⇐⇒ (¬(0 = 1 ∈ |r / d|)) ∧ (∀u,v:|r / d|.  ((¬(v = 0 ∈ |r / d|)) ⇒ ((u * v) = 0 ∈ |r / d|) ⇒ (u = 0 ∈ |r / d|)))

---

Latex:

---

Latex:

1.  r  :  CRng
2.  p  :  Ideal(r)\{i\}
3.  d  :  detach\_fun(|r|;p)
4.  \mforall{}u:|r|.  SqStable(p  u)
\mvdash{}  IsPrimeIdeal(r;p)  \mLeftarrow{}{}\mRightarrow{}  IsIntegDom(r  /  d)


By

---

Latex:
(Unfold  `integ\_dom\_p`  0
  THEN  Unfold  `nequal`  0\mcdot{}
  THEN  Assert  \mkleeneopen{}IsPrimeIdeal(r;p)
                            \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(1  =  0))  \mwedge{}  (\mforall{}u,v:|r  /  d|.    ((\mneg{}(v  =  0))  {}\mRightarrow{}  ((u  *  v)  =  0)  {}\mRightarrow{}  (u  =  0)))\mkleeneclose{}\mcdot{})

---

Home Index