---

Step * of Lemma omral_action_inj

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v,v':|r|.  ((v ⋅⋅ inj(k,v')) = inj(k,v * v') ∈ |omral(g;r)|)
BY
{ ((RepD THENM BLemma `omral_lookups_same_a` 
THENM D 0 
THENM RWW "lookup_omral_action lookup_omral_inj" 0) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. v' : |r|
6. u : |g|
⊢ (v * (when k =b u. v')) = (when k =b u. (v * v')) ∈ |r|

---

Latex:

---

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


By

---

Latex:
((RepD  THENM  BLemma  `omral\_lookups\_same\_a` 
THENM  D  0 
THENM  RWW  "lookup\_omral\_action  lookup\_omral\_inj"  0)  THENA  Auto)

---

Home Index