---

Step * 1 1 1 1 1 1 1 of Lemma ip-triangle-permute


1. rv : InnerProductSpace
2. v : Point(rv)
3. v1 : Point(rv)
⊢ (r1 * |v ⋅ v1|) = |v1 ⋅ v|
BY
{ ((Assert v ⋅ v1 = v1 ⋅ v BY Auto) THEN (RWO "-1" 0 THENA Auto) THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  v  \mcdot{}  v1  =  v1  \mcdot{}  v  BY  Auto)  THEN  (RWO  "-1"  0  THENA  Auto)  THEN  nRNorm  0  THEN  Auto)

---

Home Index