---

Step * 1 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 (a m.act m.zero)) = (a m.act m.zero) ∈ m.car
⊢ (a m.act m.zero) = 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.  a  :  |A|
4.  ((a  m.act  m.zero)  m.plus  (a  m.act  m.zero))  =  (a  m.act  m.zero)
\mvdash{}  (a  m.act  m.zero)  =  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)
  THEN  Auto
  )

---

Home Index