---

Step * 1 1 1 of Lemma module_act_zero_l


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
BY
{ (All (RWH grp_of_moduleC) 
   THENM OnMCls [0;4]  
     (\i.RWH (LemmaC `grp_eq_shift_right`) i 
         THENM RW GrpNormC i)⋅
   THEN Auto
   ) }

---

Latex:

---

Latex:

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)
\mvdash{}  (0  m.act  u)  =  m.zero


By

---

Latex:
(All  (RWH  grp\_of\_moduleC) 
  THENM  OnMCls  [0;4]   
      (\mbackslash{}i.RWH  (LemmaC  `grp\_eq\_shift\_right`)  i 
              THENM  RW  GrpNormC  i)\mcdot{}
  THEN  Auto
  )

---

Home Index