---

Step * 2 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)
8. f 0 ≡ 0
⊢ Isometry(f)
BY
{ (FLemma `rv-isometry-inverse` [4;6] 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)
8.  f  0  \mequiv{}  0
\mvdash{}  Isometry(f)


By

---

Latex:
(FLemma  `rv-isometry-inverse`  [4;6]  THEN  Auto)

---

Home Index