---

Step * 8 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)
4. BiLinear(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).times)
5. a : |r|
⊢ Dist1op2opLR(omral_alg(g;r).car;omral_alg(g;r).act a;omral_alg(g;r).times)
BY
{ RWH AbRedexC 0 
THENM Force `5` (Eval ``dist_1op_2op_lr`` 0) 
THENM ((Backchain ``omral_action_times_r1 omral_action_times_r2``) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  IsMonoid(omral\_alg(g;r).car;omral\_alg(g;r).times;omral\_alg(g;r).one)
4.  BiLinear(omral\_alg(g;r).car;omral\_alg(g;r).plus;omral\_alg(g;r).times)
5.  a  :  |r|
\mvdash{}  Dist1op2opLR(omral\_alg(g;r).car;omral\_alg(g;r).act  a;omral\_alg(g;r).times)


By

---

Latex:
RWH  AbRedexC  0 
THENM  Force  `5`  (Eval  ``dist\_1op\_2op\_lr``  0) 
THENM  ((Backchain  ``omral\_action\_times\_r1  omral\_action\_times\_r2``)  THENA  Auto)

---

Home Index