---

Step * 1 1 of Lemma rv-unit_wf


1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. r0 < ||x||
5. r0 < (||x|| * ||x||)
⊢ ((r1 * r1/||x|| * ||x||) * x^2) = r1
BY
{ ((Assert x^2 = (||x|| * ||x||) BY (RWO "rv-norm-squared<" 0 THEN Auto)) THEN (RWO  "-1" 0 THENM nRNorm 0) THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  x  \#  0
4.  r0  <  ||x||
5.  r0  <  (||x||  *  ||x||)
\mvdash{}  ((r1  *  r1/||x||  *  ||x||)  *  x\^{}2)  =  r1


By

---

Latex:
((Assert  x\^{}2  =  (||x||  *  ||x||)  BY
                (RWO  "rv-norm-squared<"  0  THEN  Auto))
  THEN  (RWO    "-1"  0  THENM  nRNorm  0)
  THEN  Auto)

---

Home Index