---

Step * of Lemma rv-mul0

∀[rv:RealVectorSpace]. ∀[x:Point].  r0*x ≡ 0
BY
{ (Auto
   THEN (D 1 THENA Auto)
   THEN Unfolds ``rv-mul rv-add rv-0`` 0
   THEN OnMaybeHyp 8 (\h. (MemTypeHD h
                           THEN ∀h:hyp. Fold `member` h 
                           THEN Try (MemCD)
                           THEN (Unhide THENM (ExRepD THEN BackThruSomeHyp))
                           THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[x:Point].    r0*x  \mequiv{}  0


By

---

Latex:
(Auto
  THEN  (D  1  THENA  Auto)
  THEN  Unfolds  ``rv-mul  rv-add  rv-0``  0
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  (MemTypeHD  h
                                                  THEN  \mforall{}h:hyp.  Fold  `member`  h 
                                                  THEN  Try  (MemCD)
                                                  THEN  (Unhide  THENM  (ExRepD  THEN  BackThruSomeHyp))
                                                  THEN  Auto)))

---

Home Index