---

Step * of Lemma omral_action_times_r2

∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps,qs:|omral(g;r)|.  ((v ⋅⋅ (ps ** qs)) = (ps ** (v ⋅⋅ qs)) ∈ |omral(g;r)|)
BY
{ ((RepD  
THENM RWH (LemmaC `omral_times_comm_a`) 0 
THENM RWO "omral_action_times_r1<" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}v:|r|.  \mforall{}ps,qs:|omral(g;r)|.    ((v  \mcdot{}\mcdot{}  (ps  **  qs))  =  (ps  **  (v  \mcdot{}\mcdot{}  qs)))


By

---

Latex:
((RepD   
THENM  RWH  (LemmaC  `omral\_times\_comm\_a`)  0 
THENM  RWO  "omral\_action\_times\_r1<"  0)  THEN  Auto)

---

Home Index