Step * of Lemma module_act_minus_r

A:Rng. ∀m:A-Module. ∀a:|A|. ∀u:m.car.  ((a m.act (m.minus u)) (m.minus (a m.act u)) ∈ m.car)
BY
((RepD) THENA Auto) }

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


Latex:


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


By


Latex:
((RepD)  THENA  Auto)




Home Index