---

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


1. rv : InnerProductSpace
2. v : Point(rv)
3. v1 : Point(rv)
⊢ |v ⋅ r(-1)*v1| = |v1 ⋅ v|
BY
{ ((RWW "rv-ip-mul2 rabs-rmul rabs-int" 0⋅ THENA Auto) THEN Reduce 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWW  "rv-ip-mul2  rabs-rmul  rabs-int"  0\mcdot{}  THENA  Auto)  THEN  Reduce  0)

---

Home Index