---

Step * 1 of Lemma algebra_act_times_lr


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
BY
{ ((RWO "module_action_p.1" 0 
THENM RWO "algebra_act_times_r.2" 0 
THENM RWO "algebra_act_times_r.1" 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "module\_action\_p.1"  0 
THENM  RWO  "algebra\_act\_times\_r.2"  0 
THENM  RWO  "algebra\_act\_times\_r.1"  0)  THEN  Auto)

---

Home Index