---

Step * 2 of Lemma omral_minus_wf


1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
⊢ --ps ∈ |oal(g↓set;r↓+gp)|
BY
{ (Assert r↓+gp ∈ AbDGrp BY
         (DVar `r' THEN MemTypeCD THEN Auto)) }

1
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. r↓+gp ∈ AbDGrp
⊢ --ps ∈ |oal(g↓set;r↓+gp)|

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
\mvdash{}  --ps  \mmember{}  |oal(g\mdownarrow{}set;r\mdownarrow{}+gp)|


By

---

Latex:
(Assert  r\mdownarrow{}+gp  \mmember{}  AbDGrp  BY
              (DVar  `r'  THEN  MemTypeCD  THEN  Auto))

---

Home Index