---

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


1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. ((||v|| * ||v1||) + v ⋅ v1) = r0
⊢ v ⋅ v1^2 = ||v|| * ||v1||^2
BY
{ (nRAdd ⌜-(v ⋅ v1)⌝ (-1)⋅ THENA Auto) }

1
1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. (||v|| * ||v1||) = -(v ⋅ v1)
⊢ v ⋅ v1^2 = ||v|| * ||v1||^2

---

Latex:

---

Latex:

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


By

---

Latex:
(nRAdd  \mkleeneopen{}-(v  \mcdot{}  v1)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index