---

Step * of Lemma module_act_plus

∀[A:Rng]. ∀[m:A-Module].
  ((∀[a1,a2:|A|]. ∀[b:m.car].  (((a1 +A a2) m.act b) = ((a1 m.act b) m.plus (a2 m.act b)) ∈ m.car))
  ∧ (∀[a:|A|]. ∀[b1,b2:m.car].  ((a m.act (b1 m.plus b2)) = ((a m.act b1) m.plus (a m.act b2)) ∈ m.car)))
BY
{ ((ProvePropertyLemma `bilinear_p` 2) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:A-Module].
    ((\mforall{}[a1,a2:|A|].  \mforall{}[b:m.car].    (((a1  +A  a2)  m.act  b)  =  ((a1  m.act  b)  m.plus  (a2  m.act  b))))
    \mwedge{}  (\mforall{}[a:|A|].  \mforall{}[b1,b2:m.car].    ((a  m.act  (b1  m.plus  b2))  =  ((a  m.act  b1)  m.plus  (a  m.act  b2)))))


By

---

Latex:
((ProvePropertyLemma  `bilinear\_p`  2)  THEN  Auto)

---

Home Index