---

Step * 1 of Lemma module_act_zero_l


1. A : Rng
2. m : A-Module
3. u : m.car
4. (0 m.act u) = (0 m.act u) ∈ m.car
⊢ (0 m.act u) = m.zero ∈ m.car
BY
{ ((RWN 1 (AssertThenC (RW RngNormC 0)  
        0 = (0 +A 0) ∈ |A|) 4) THENA Auto)⋅ }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWN  1  (AssertThenC  (RW  RngNormC  0)   
                0  =  (0  +A  0))  4)  THENA  Auto)\mcdot{}

---

Home Index