---

Step * 1 of Lemma module_over_triv_rng


1. A : Rng
2. m : A-Module
3. 1 = 0 ∈ |A|
4. u : m.car
⊢ u = m.zero ∈ m.car
BY
{ ((ApFunToHypEquands `a' a m.act u m.car 3) THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((ApFunToHypEquands  `a'  a  m.act  u  m.car  3)  THENA  Auto)

---

Home Index