---

Step * of Lemma rv-mul1

∀[rv:RealVectorSpace]. ∀[x:Point].  r1*x ≡ x
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{}[x:Point].    r1*x  \mequiv{}  x


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