---

Step * of Lemma rv-isometry-injective

∀[rv:InnerProductSpace]. ∀f:Point ⟶ Point. (Isometry(f) ⇒ (∀x,y:Point.  (f x ≡ f y ⇒ x ≡ y)))
BY
{ (Auto
   THEN (BLemma `rv-sub-is-zero` THENA Auto)
   THEN (FLemma `rv-sub-is-zero` [-1] THENA Auto)
   THEN (BLemma `rv-norm-is-zero` THENA Auto)
   THEN (FLemma `rv-norm-is-zero` [-1] THENA Auto)) }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Isometry(f)
4. x : Point
5. y : Point
6. f x ≡ f y
7. f x - f y ≡ 0
8. ||f x - f y|| = r0
⊢ ||x - y|| = r0

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (BLemma  `rv-sub-is-zero`  THENA  Auto)
  THEN  (FLemma  `rv-sub-is-zero`  [-1]  THENA  Auto)
  THEN  (BLemma  `rv-norm-is-zero`  THENA  Auto)
  THEN  (FLemma  `rv-norm-is-zero`  [-1]  THENA  Auto))

---

Home Index