---

Step * 2 2 1 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. r↓+gp ∈ AbDGrp
4. <|oal(g↓oset;r↓+gp)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.(--x)> ∈ Group{i}
5. IsMonoid(|oal(g↓oset;r↓+gp)|;λx,y. (x ++ y);00)
6. Inverse(|oal(g↓oset;r↓+gp)|;λx,y. (x ++ y);00;λx.(--x))
⊢ IsGroup(|omral(g;r)|;λx,y. (x ++ y);00g,r;λx.(--x))
BY
{ Unfolds ``omralist omral_plus omral_zero omral_minus`` 0 
THEN ((AGenRepD ["compound"]) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  r\mdownarrow{}+gp  \mmember{}  AbDGrp
4.  <|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|,  =\msubb{},  \mlambda{}x,y.  x  \mleq{}\mleq{}\msubb{}  y,  \mlambda{}x,y.  (x  ++  y),  00,  \mlambda{}x.(--x)>  \mmember{}  Group\{i\}
5.  IsMonoid(|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|;\mlambda{}x,y.  (x  ++  y);00)
6.  Inverse(|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|;\mlambda{}x,y.  (x  ++  y);00;\mlambda{}x.(--x))
\mvdash{}  IsGroup(|omral(g;r)|;\mlambda{}x,y.  (x  ++  y);00g,r;\mlambda{}x.(--x))


By

---

Latex:
Unfolds  ``omralist  omral\_plus  omral\_zero  omral\_minus``  0 
THEN  ((AGenRepD  ["compound"])  THEN  Auto)

---

Home Index