---

Step * 2 2 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. r↓+gp ∈ AbDGrp
⊢ IsGroup(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).zero;omral_alg(g;r).minus)
BY
{ ((Assert oal_grp(g↓oset;r↓+gp) ∈ Group{i} 
THENM AddAllProperties (-1) 
THENM All (\i.Force `5` (Eval ``oal_grp omral_alg`` i))) THENA Auto) }

1
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))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  r\mdownarrow{}+gp  \mmember{}  AbDGrp
\mvdash{}  IsGroup(omral\_alg(g;r).car;omral\_alg(g;r).plus;omral\_alg(g;r).zero;omral\_alg(g;r).minus)


By

---

Latex:
((Assert  oal\_grp(g\mdownarrow{}oset;r\mdownarrow{}+gp)  \mmember{}  Group\{i\} 
THENM  AddAllProperties  (-1) 
THENM  All  (\mbackslash{}i.Force  `5`  (Eval  ``oal\_grp  omral\_alg``  i)))  THENA  Auto)

---

Home Index