---

Step * of Lemma module_act_zero_r

∀A:Rng. ∀m:A-Module. ∀a:|A|.  ((a m.act m.zero) = m.zero ∈ m.car)
BY
{ ((RepD THENM Assert (a m.act m.zero) = (a m.act m.zero) ∈ m.car) THENA Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:A-Module.  \mforall{}a:|A|.    ((a  m.act  m.zero)  =  m.zero)


By

---

Latex:
((RepD  THENM  Assert  (a  m.act  m.zero)  =  (a  m.act  m.zero))  THENA  Auto)

---

Home Index