---

Step * 1 1 1 of Lemma module_act_minus_l


1. A : Rng
2. m : A-Module
3. a : |A|
4. u : m.car
⊢ ((a +A (-A a)) m.act u) = m.zero ∈ m.car
BY
{ ((RW RngNormC 0 
THENM RWO "module_act_zero_l" 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RW  RngNormC  0 
THENM  RWO  "module\_act\_zero\_l"  0)  THEN  Auto)

---

Home Index