---

Step * 1 1 of Lemma module_act_zero_r


1. A : Rng
2. m : A-Module
3. a : |A|
4. (a m.act (m.zero m.plus m.zero)) = (a m.act m.zero) ∈ m.car
⊢ (a m.act m.zero) = m.zero ∈ m.car
BY
{ ((RWO "module_act_plus.2" 4) THENA Auto) }

1
1. A : Rng
2. m : A-Module
3. a : |A|
4. ((a m.act m.zero) m.plus (a m.act m.zero)) = (a m.act m.zero) ∈ m.car
⊢ (a m.act m.zero) = m.zero ∈ m.car

---

Latex:

---

Latex:

1.  A  :  Rng
2.  m  :  A-Module
3.  a  :  |A|
4.  (a  m.act  (m.zero  m.plus  m.zero))  =  (a  m.act  m.zero)
\mvdash{}  (a  m.act  m.zero)  =  m.zero


By

---

Latex:
((RWO  "module\_act\_plus.2"  4)  THENA  Auto)

---

Home Index