---

Step * 2 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
⊢ IsGroup(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).zero;omral_alg(g;r).minus)
BY
{ Assert ⌜r↓+gp ∈ AbDGrp⌝⋅ }

1
.....assertion..... 
1. g : OCMon
2. r : CDRng
⊢ r↓+gp ∈ AbDGrp

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

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
\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  \mkleeneopen{}r\mdownarrow{}+gp  \mmember{}  AbDGrp\mkleeneclose{}\mcdot{}

---

Home Index