---

Step * of Lemma rv-unit-property

∀rv:InnerProductSpace. ∀x:Point.  (x # 0 ⇒ (∃t:ℝ. (t ≠ r0 ∧ rv-unit(rv;x) ≡ t*x)))
BY
{ (Auto
   THEN (FLemma `rv-norm-positive` [-1] THENA Auto)
   THEN Unfold `rv-unit` 0
   THEN D 0 With ⌜(r1/||x||)⌝ 
   THEN Auto) }

1
1. rv : InnerProductSpace
2. x : Point
3. x # 0
4. r0 < ||x||
⊢ (r1/||x||) ≠ r0

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x:Point.    (x  \#  0  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  (t  \mneq{}  r0  \mwedge{}  rv-unit(rv;x)  \mequiv{}  t*x)))


By

---

Latex:
(Auto
  THEN  (FLemma  `rv-norm-positive`  [-1]  THENA  Auto)
  THEN  Unfold  `rv-unit`  0
  THEN  D  0  With  \mkleeneopen{}(r1/||x||)\mkleeneclose{} 
  THEN  Auto)

---

Home Index