---

Step * 1 1 1 1 1 1 of Lemma ip-between-iff


1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. (||v|| * ||v1||) = -(v ⋅ v1)
⊢ v ⋅ v1^2 = ||v|| * ||v1||^2
BY
{ ((RWW "-1 rnexp2" 0⋅ THENA Auto) THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  v  :  Point
3.  v1  :  Point
4.  (||v||  *  ||v1||)  =  -(v  \mcdot{}  v1)
\mvdash{}  v  \mcdot{}  v1\^{}2  =  ||v||  *  ||v1||\^{}2


By

---

Latex:
((RWW  "-1  rnexp2"  0\mcdot{}  THENA  Auto)  THEN  nRNorm  0  THEN  Auto)

---

Home Index