---

Step * of Lemma rv-mul-linear

∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point].  a*x + y ≡ a*x + a*y
BY
{ (Auto
   THEN (D 1 THENA Auto)
   THEN Unfolds ``rv-mul rv-add`` 0
   THEN OnMaybeHyp 10 (\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{}[a:\mBbbR{}].  \mforall{}[x,y:Point].    a*x  +  y  \mequiv{}  a*x  +  a*y


By

---

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

---

Home Index