---

Step * of Lemma omral_times_dom

∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  (↑(dom(ps ** qs) ⊆b (dom(ps) × dom(qs))))
BY
{ (((RepD) THENA Auto)
   THEN (Assert (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon) BY
               ((InstLemma `cdrng_is_abdmonoid` [⌜r⌝]⋅ THEN Auto) THEN BLemma `omon_inc`⋅ THEN Auto))
   ) }

1
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. qs : |omral(g;r)|
5. (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon)
⊢ ↑(dom(ps ** qs) ⊆b (dom(ps) × dom(qs)))

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:|omral(g;r)|.    (\muparrow{}(dom(ps  **  qs)  \msubseteq{}\msubb{}  (dom(ps)  \mtimes{}  dom(qs))))


By

---

Latex:
(((RepD)  THENA  Auto)
  THEN  (Assert  (r\mdownarrow{}+gp  \mmember{}  AbDMon)  \mwedge{}  (g  \mmember{}  DMon)  BY
                          ((InstLemma  `cdrng\_is\_abdmonoid`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  BLemma  `omon\_inc`\mcdot{}  THEN  Auto))
  )

---

Home Index