---

Step * of Lemma module_act_zero_l

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

1
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

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:A-Module.  \mforall{}u:m.car.    ((0  m.act  u)  =  m.zero)


By

---

Latex:
((RepD   
THENM  Assert  (0  m.act  u)  =  (0  m.act  u))  THENA  Auto)

---

Home Index