Step
*
2
2
1
2
1
1
of Lemma
implies-isometry-lemma2
1. rv : InnerProductSpace
2. J : ℝ
3. v : Point
4. v1 : Point
5. v2 : Point
6. v + J - r1*v1 - v ≡ (r1/r(2))*v + J - r(2)*v1 - v + v2
⊢ v2 ≡ v + J*v1 - v
BY
{ ((RealVecMul ⌜r(2)⌝ (-1)⋅ THENA Auto)
   THEN (RWO  "rv-mul-mul" (-1) THENA Auto)
   THEN nRNorm (-1)
   THEN (RWO "rv-mul1" (-1) THENA Auto)) }
1
1. rv : InnerProductSpace
2. J : ℝ
3. v : Point
4. v1 : Point
5. v2 : Point
6. r(2)*v + r(-1) + J*v1 - v ≡ v + r(-2) + J*v1 - v + v2
⊢ v2 ≡ v + J*v1 - v
Latex:
Latex:
1.  rv  :  InnerProductSpace
2.  J  :  \mBbbR{}
3.  v  :  Point
4.  v1  :  Point
5.  v2  :  Point
6.  v  +  J  -  r1*v1  -  v  \mequiv{}  (r1/r(2))*v  +  J  -  r(2)*v1  -  v  +  v2
\mvdash{}  v2  \mequiv{}  v  +  J*v1  -  v
By
Latex:
((RealVecMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO    "rv-mul-mul"  (-1)  THENA  Auto)
  THEN  nRNorm  (-1)
  THEN  (RWO  "rv-mul1"  (-1)  THENA  Auto))
Home
Index