---

Step * of Lemma cdrng_is_abdmonoid

∀[r:CDRng]. ((r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon))
BY
{ (xxxIntroxxx
   THEN D 0
   THEN Unhide
   THEN DVar `r'
   THEN (InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
   THEN Fold `comm` (-1)
   THEN RepeatFor 2 (((MemTypeCD THEN Reduce 0 THEN Try (Trivial) THEN Try ((D 1 THEN Trivial))) THENW Auto))
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(xxxIntroxxx
  THEN  D  0
  THEN  Unhide
  THEN  DVar  `r'
  THEN  (InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `comm`  (-1)
  THEN  RepeatFor  2  (((MemTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)  THEN  Try  ((D  1  THEN  Trivial)))
                                        THENW  Auto
                                        ))
  THEN  Auto)

---

Home Index