---

Step * 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 +r (-r 0)))) ∧ (∀u,v:|r|.  ((¬(p (v +r (-r 0)))) ⇒ (p ((u * v) +r (-r 0))) ⇒ (p (u +r (-r 0)))))
BY
{ ((RW RngNormC 0) 
   THENA (Try (Complete (Auto))
          THEN Try (((RW RngNormC (-1)) THENA Auto))
          THEN Try (((RW RngNormC 0) THENA Auto))
          THEN Try (Trivial))
   )⋅ }

1
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)))

---

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


By

---

Latex:
((RW  RngNormC  0) 
  THENA  (Try  (Complete  (Auto))
                THEN  Try  (((RW  RngNormC  (-1))  THENA  Auto))
                THEN  Try  (((RW  RngNormC  0)  THENA  Auto))
                THEN  Try  (Trivial))
  )\mcdot{}

---

Home Index