---

Step * 4 of Lemma alg_act_is_rng_chom


1. a : CRng
2. m : algebra{i:l}(a)
3. a@0 : |a|
4. b : |a|
⊢ ((m.act a@0 m.one) m.times (m.act b m.one)) = ((m.act b m.one) m.times (m.act a@0 m.one)) ∈ m.car
BY
{ ((RWH (RevGenLemmaC 1 `algebra_act_times_r`) 0) THENA Auto) }

1
1. a : CRng
2. m : algebra{i:l}(a)
3. a@0 : |a|
4. b : |a|
⊢ (m.act a@0 (m.one m.times (m.act b m.one))) = (m.act b (m.one m.times (m.act a@0 m.one))) ∈ m.car

---

Latex:

---

Latex:

1.  a  :  CRng
2.  m  :  algebra\{i:l\}(a)
3.  a@0  :  |a|
4.  b  :  |a|
\mvdash{}  ((m.act  a@0  m.one)  m.times  (m.act  b  m.one))  =  ((m.act  b  m.one)  m.times  (m.act  a@0  m.one))


By

---

Latex:
((RWH  (RevGenLemmaC  1  `algebra\_act\_times\_r`)  0)  THENA  Auto)

---

Home Index