Step
*
of Lemma
rv-orthogonal-isometry
∀[rv:InnerProductSpace]. ∀[f:Point ⟶ Point].  Isometry(f) supposing Orthogonal(f)
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN DupHyp (-3)
   THEN (RWO  "rv-orthogonal-iff-norm-preserving" (-1) THENA Auto)
   THEN (Assert ⌜f x - f y ≡ f x - y⌝⋅ THENM (RWO  "-1" 0 THEN Auto))) }
1
.....assertion..... 
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. x : Point
5. y : Point
6. (∀x,y:Point.  f x + y ≡ f x + f y) ∧ (∀x:Point. ((∀a:ℝ. f a*x ≡ a*f x) ∧ (||f x|| = ||x||)))
⊢ f x - f y ≡ f x - y
Latex:
Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[f:Point  {}\mrightarrow{}  Point].    Isometry(f)  supposing  Orthogonal(f)
By
Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  DupHyp  (-3)
  THEN  (RWO    "rv-orthogonal-iff-norm-preserving"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}f  x  -  f  y  \mequiv{}  f  x  -  y\mkleeneclose{}\mcdot{}  THENM  (RWO    "-1"  0  THEN  Auto)))
Home
Index