---

Step * 1 of Lemma rv-orthogonal-inverse


1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. g : Point ⟶ Point
4. ∀x:Point. g (f x) ≡ x
5. g 0 ≡ 0
6. Isometry(g)
7. ∀x,y:Point.  (g x ≡ g y ⇒ x ≡ y)
⊢ f 0 ≡ 0
BY
{ ((BHyp -1  THEN Auto) THEN RWO "4" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point  {}\mrightarrow{}  Point
3.  g  :  Point  {}\mrightarrow{}  Point
4.  \mforall{}x:Point.  g  (f  x)  \mequiv{}  x
5.  g  0  \mequiv{}  0
6.  Isometry(g)
7.  \mforall{}x,y:Point.    (g  x  \mequiv{}  g  y  {}\mRightarrow{}  x  \mequiv{}  y)
\mvdash{}  f  0  \mequiv{}  0


By

---

Latex:
((BHyp  -1    THEN  Auto)  THEN  RWO  "4"  0  THEN  Auto)

---

Home Index