---

Step * of Lemma cdrng_is_abdgrp

∀[r:CDRng]. (r↓+gp ∈ AbDGrp)
BY
{ (xxxIntroxxx THEN Unhide THEN D 1 THEN MemTypeCD) }

1
1. r : CRng
2. IsEqFun(|r|;=b)
⊢ r↓+gp ∈ AbGrp

2
.....set predicate..... 
1. r : CRng
2. IsEqFun(|r|;=b)
⊢ IsEqFun(|r↓+gp|;=b)

3
.....wf..... 
1. r : CRng
2. IsEqFun(|r|;=b)
3. g : AbGrp
⊢ IsEqFun(|g|;=b) ∈ Type

---

Latex:

---

Latex:
\mforall{}[r:CDRng].  (r\mdownarrow{}+gp  \mmember{}  AbDGrp)


By

---

Latex:
(xxxIntroxxx  THEN  Unhide  THEN  D  1  THEN  MemTypeCD)

---

Home Index