---

Step * 1 of Lemma module_act_zero_r


1. A : Rng
2. m : A-Module
3. a : |A|
4. (a m.act m.zero) = (a m.act m.zero) ∈ m.car
⊢ (a m.act m.zero) = m.zero ∈ m.car
BY
{ ((RWN 1 (AssertC m.zero = (m.zero m.plus m.zero) ∈ m.car) 4) THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWN  1  (AssertC  m.zero  =  (m.zero  m.plus  m.zero))  4)  THENA  Auto)

---

Home Index