---

Step * 1 1 of Lemma module_act_minus_r


1. A : Rng
2. m : A-Module
3. a : |A|
4. u : m.car
⊢ ((a m.act u) * (a m.act (~ u))) = e ∈ |(m↓grp)|
BY
{ ((RWH rem_grp_of_moduleC 0 
THENM RWO "module_act_plus.2<" 0) THENA Auto) }

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

---

Latex:

---

Latex:

1.  A  :  Rng
2.  m  :  A-Module
3.  a  :  |A|
4.  u  :  m.car
\mvdash{}  ((a  m.act  u)  *  (a  m.act  (\msim{}  u)))  =  e


By

---

Latex:
((RWH  rem\_grp\_of\_moduleC  0 
THENM  RWO  "module\_act\_plus.2<"  0)  THENA  Auto)

---

Home Index