---

Step * of Lemma rv-orthogonal-iff-norm-preserving

∀[rv:InnerProductSpace]
  ∀f:Point ⟶ Point
    (Orthogonal(f) ⇐⇒ (∀x,y:Point.  f x + y ≡ f x + f y) ∧ (∀x:Point. ((∀a:ℝ. f a*x ≡ a*f x) ∧ (||f x|| = ||x||))))
BY
{ Auto }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. x : Point
⊢ ||f x|| = ||x||

2
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. ∀x,y:Point.  f x + y ≡ f x + f y
4. ∀x:Point. ((∀a:ℝ. f a*x ≡ a*f x) ∧ (||f x|| = ||x||))
⊢ Orthogonal(f)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace]
    \mforall{}f:Point  {}\mrightarrow{}  Point
        (Orthogonal(f)
        \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x,y:Point.    f  x  +  y  \mequiv{}  f  x  +  f  y)
                \mwedge{}  (\mforall{}x:Point.  ((\mforall{}a:\mBbbR{}.  f  a*x  \mequiv{}  a*f  x)  \mwedge{}  (||f  x||  =  ||x||))))


By

---

Latex:
Auto

---

Home Index