---

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


1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. ((||v|| * ||v1||) + v ⋅ v1) = r0
⊢ v1 ⋅ v^2 = ||v1|| * ||v||^2
BY
{ (RWO "rmul_comm rv-ip-symmetry" 0 THENA Auto) }

1
1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. ((||v|| * ||v1||) + v ⋅ v1) = r0
⊢ 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{}  v1  \mcdot{}  v\^{}2  =  ||v1||  *  ||v||\^{}2


By

---

Latex:
(RWO  "rmul\_comm  rv-ip-symmetry"  0  THENA  Auto)

---

Home Index