Step * 2 2 1 2 1 1 of Lemma implies-isometry-lemma2


1. rv InnerProductSpace
2. : ℝ
3. Point
4. v1 Point
5. v2 Point
6. r1*v1 v ≡ (r1/r(2))*v r(2)*v1 v2
⊢ v2 ≡ 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. : ℝ
3. Point
4. v1 Point
5. v2 Point
6. r(2)*v r(-1) J*v1 v ≡ r(-2) J*v1 v2
⊢ v2 ≡ 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