---

Step * of Lemma omral_inj_mon_op

∀g:OCMon. ∀r:CDRng. ∀k,k':|g|.  (inj(k * k',1) = (inj(k,1) ** inj(k',1)) ∈ |omral(g;r)|)
BY
{ (((RepD THENM BLemma `omral_lookups_same_a` 
   THENM D 0) THENA Auto)
   THEN (Assert ∀r:CDRng. (r↓+gp ∈ IAbMonoid) BY
               (InstLemma `cdrng_is_abdmonoid` [] THEN ParallelLast THEN Auto))
   ) }

1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. u : |g|
6. ∀r:CDRng. (r↓+gp ∈ IAbMonoid)
⊢ (inj(k * k',1)[u]) = ((inj(k,1) ** inj(k',1))[u]) ∈ |r|

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k,k':|g|.    (inj(k  *  k',1)  =  (inj(k,1)  **  inj(k',1)))


By

---

Latex:
(((RepD  THENM  BLemma  `omral\_lookups\_same\_a` 
  THENM  D  0)  THENA  Auto)
  THEN  (Assert  \mforall{}r:CDRng.  (r\mdownarrow{}+gp  \mmember{}  IAbMonoid)  BY
                          (InstLemma  `cdrng\_is\_abdmonoid`  []  THEN  ParallelLast  THEN  Auto))
  )

---

Home Index