---

Step * of Lemma rv-isometry-implies-extensional

∀rv:InnerProductSpace. ∀f:Point ⟶ Point.  ∀x,y:Point.  (f x # f y ⇒ x # y) supposing Isometry(f)
BY
{ ((Auto THEN (FLemma `rv-sep-iff-ext` [-1] THENA Auto) THEN (FLemma `rv-norm-positive-iff-ext` [-1] THENA Auto))
   THEN Unfold `rv-isometry` 3
   THEN (RWO "3" (-1) THENA Auto)
   THEN (RWO "rv-norm-positive-iff-ext<" (-1) THENA Auto)) }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. ∀[x,y:Point].  (||f x - f y|| = ||x - y||)
4. x : Point
5. y : Point
6. f x # f y
7. f x - f y # 0
8. x - y # 0
⊢ x # y

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point  {}\mrightarrow{}  Point.    \mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)  supposing  Isometry(f)


By

---

Latex:
((Auto
    THEN  (FLemma  `rv-sep-iff-ext`  [-1]  THENA  Auto)
    THEN  (FLemma  `rv-norm-positive-iff-ext`  [-1]  THENA  Auto))
  THEN  Unfold  `rv-isometry`  3
  THEN  (RWO  "3"  (-1)  THENA  Auto)
  THEN  (RWO  "rv-norm-positive-iff-ext<"  (-1)  THENA  Auto))

---

Home Index