---

Step * of Lemma det_ideal_ap_elim

∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a).  ((∀w:|r|. SqStable(a w)) ⇒ (∀v:|r|. (↑(d v) ⇐⇒ a v)))
BY
{ (UnivCD THENA Auto THEN Auto THEN D 3 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}a:Ideal(r)\{i\}.  \mforall{}d:detach\_fun(|r|;a).
    ((\mforall{}w:|r|.  SqStable(a  w))  {}\mRightarrow{}  (\mforall{}v:|r|.  (\muparrow{}(d  v)  \mLeftarrow{}{}\mRightarrow{}  a  v)))


By

---

Latex:
(UnivCD  THENA  Auto  THEN  Auto  THEN  D  3  THEN  Auto)

---

Home Index