---

Step * of Lemma rv-orthogonal-injective

No Annotations
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇒ (∀x,y:Point(rv).  (f x ≡ f y ⇒ x ≡ y)))
BY
{ (Auto THEN (BLemma `rv-sub-is-zero` THENA Auto) THEN BLemma `rv-ip-zero-iff` THEN Auto) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. Orthogonal(f)
4. x : Point(rv)
5. y : Point(rv)
6. f x ≡ f y
⊢ x - y^2 = r0

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace]
    \mforall{}f:Point(rv)  {}\mrightarrow{}  Point(rv).  (Orthogonal(f)  {}\mRightarrow{}  (\mforall{}x,y:Point(rv).    (f  x  \mequiv{}  f  y  {}\mRightarrow{}  x  \mequiv{}  y)))


By

---

Latex:
(Auto  THEN  (BLemma  `rv-sub-is-zero`  THENA  Auto)  THEN  BLemma  `rv-ip-zero-iff`  THEN  Auto)

---

Home Index