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