Step * of Lemma rv-orthogonal-isometry

[rv:InnerProductSpace]. ∀[f:Point ⟶ Point].  Isometry(f) supposing Orthogonal(f)
BY
((Auto THEN THEN Auto)
   THEN DupHyp (-3)
   THEN (RWO  "rv-orthogonal-iff-norm-preserving" (-1) THENA Auto)
   THEN (Assert ⌜y ≡ y⌝⋅ THENM (RWO  "-1" THEN Auto))) }

1
.....assertion..... 
1. rv InnerProductSpace
2. Point ⟶ Point
3. Orthogonal(f)
4. Point
5. Point
6. (∀x,y:Point.  y ≡ y) ∧ (∀x:Point. ((∀a:ℝa*x ≡ a*f x) ∧ (||f x|| ||x||)))
⊢ y ≡ 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