---

Step * 2 of Lemma oal_hgp_wf2


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))
BY
{ ((InstConcl [oal_grp(s;g);λz.z]) THENA Try  (Complete Auto)) }

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

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  (g\mdownarrow{}hgrp  \mmember{}  AbDMon)  \mwedge{}  (g  \mmember{}  AbDMon)
\mvdash{}  \mexists{}h:OCMon
      \mexists{}f:|oal\_hgp(s;g)|  {}\mrightarrow{}  |h|
        (IsMonHomInj(oal\_hgp(s;g);h;f)
        \mwedge{}  RelsIso(|oal\_hgp(s;g)|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
        \mwedge{}  RelsIso(|oal\_hgp(s;g)|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f))


By

---

Latex:
((InstConcl  [oal\_grp(s;g);\mlambda{}z.z])  THENA  Try    (Complete  Auto))

---

Home Index