---

Step * of Lemma oal_hgp_wf2

∀s:LOSet. ∀g:OGrp.  (oal_hgp(s;g) ∈ OCMon)
BY
{ (((RepD THENM BLemma `inj_into_ocmon`) THENA Auto) THEN Assert ⌜(g↓hgrp ∈ AbDMon) ∧ (g ∈ AbDMon)⌝⋅) }

1
.....assertion..... 
1. s : LOSet@i'
2. g : OGrp@i'
⊢ (g↓hgrp ∈ AbDMon) ∧ (g ∈ AbDMon)

2
1. s : LOSet@i'
2. g : OGrp@i'
3. (g↓hgrp ∈ AbDMon) ∧ (g ∈ AbDMon)
⊢ ∃h:OCMon
   ∃f:|oal_hgp(s;g)| ⟶ |h|
    (IsMonHomInj(oal_hgp(s;g);h;f)
    ∧ RelsIso(|oal_hgp(s;g)|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
    ∧ RelsIso(|oal_hgp(s;g)|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (oal\_hgp(s;g)  \mmember{}  OCMon)


By

---

Latex:
(((RepD  THENM  BLemma  `inj\_into\_ocmon`)  THENA  Auto)  THEN  Assert  \mkleeneopen{}(g\mdownarrow{}hgrp  \mmember{}  AbDMon)  \mwedge{}  (g  \mmember{}  AbDMon)\mkleeneclose{}\mcdot{})

---

Home Index