---

Step * 1 1 1 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) ⇐⇒ (¬(p 1)) ∧ (∀u,v:|r|.  ((¬(p v)) ⇒ (p (u * v)) ⇒ (p u)))
BY
{ Assert ⌜(¬(p 1)) ∧ (∀u,v:|r|.  ((¬(p v)) ⇒ (p (u * v)) ⇒ (p u)))
          ⇐⇒ (¬(p 1)) ∧ (∀u,v:|r|.  ((p (u * v)) ⇒ ((p u) ∨ (p v))))⌝⋅ }

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

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

---

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{}  (\mneg{}(p  1))  \mwedge{}  (\mforall{}u,v:|r|.    ((\mneg{}(p  v))  {}\mRightarrow{}  (p  (u  *  v))  {}\mRightarrow{}  (p  u)))


By

---

Latex:
Assert  \mkleeneopen{}(\mneg{}(p  1))  \mwedge{}  (\mforall{}u,v:|r|.    ((\mneg{}(p  v))  {}\mRightarrow{}  (p  (u  *  v))  {}\mRightarrow{}  (p  u)))
                \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(p  1))  \mwedge{}  (\mforall{}u,v:|r|.    ((p  (u  *  v))  {}\mRightarrow{}  ((p  u)  \mvee{}  (p  v))))\mkleeneclose{}\mcdot{}

---

Home Index