---

Step * 1 of Lemma module_act_minus_l


1. A : Rng
2. m : A-Module
3. a : |A|
4. u : m.car
⊢ ((-A a) m.act u) = (m.minus (a m.act u)) ∈ m.car
BY
{ ((RWH grp_of_moduleC 0 
THENM RWH (LemmaWithC [`c',a m.act u] 
            `grp_eq_op_l`) 0 
THENM RW GrpNormC 0) THENA Auto) }

1
1. A : Rng
2. m : A-Module
3. a : |A|
4. u : m.car
⊢ ((a m.act u) * ((-A a) m.act u)) = e ∈ |(m↓grp)|

---

Latex:

---

Latex:

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


By

---

Latex:
((RWH  grp\_of\_moduleC  0 
THENM  RWH  (LemmaWithC  [`c',a  m.act  u] 
                        `grp\_eq\_op\_l`)  0 
THENM  RW  GrpNormC  0)  THENA  Auto)

---

Home Index