---

Step * of Lemma algebra_act_times_lr

∀A:Rng. ∀m:algebra{i:l}(A). ∀a,b:|A|. ∀u,v:m.car.
  (((a * b) m.act (u m.times v)) = ((a m.act u) m.times (b m.act v)) ∈ m.car)
BY
{ ((RepD) THENA Auto) }

1
1. A : Rng
2. m : algebra{i:l}(A)
3. a : |A|
4. b : |A|
5. u : m.car
6. v : m.car
⊢ ((a * b) m.act (u m.times v)) = ((a m.act u) m.times (b m.act v)) ∈ m.car

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:algebra\{i:l\}(A).  \mforall{}a,b:|A|.  \mforall{}u,v:m.car.
    (((a  *  b)  m.act  (u  m.times  v))  =  ((a  m.act  u)  m.times  (b  m.act  v)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index