---

Step * 1 1 of Lemma module_act_zero_l


1. A : Rng
2. m : A-Module
3. u : m.car
4. ((0 +A 0) m.act u) = (0 m.act u) ∈ m.car
⊢ (0 m.act u) = m.zero ∈ m.car
BY
{ ((RWO "module_act_plus.1" 4) THENA Auto)⋅ }

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

---

Latex:

---

Latex:

1.  A  :  Rng
2.  m  :  A-Module
3.  u  :  m.car
4.  ((0  +A  0)  m.act  u)  =  (0  m.act  u)
\mvdash{}  (0  m.act  u)  =  m.zero


By

---

Latex:
((RWO  "module\_act\_plus.1"  4)  THENA  Auto)\mcdot{}

---

Home Index