---

Step * of Lemma hyptrans_0

∀[rv:InnerProductSpace]. ∀[e,x:Point].  hyptrans(rv;e;r0;x) ≡ x
BY
{ ((Auto THEN RepUR ``hyptrans`` 0) THEN ((RWO "cosh0 sinh0" 0 THENM nRNorm 0) THENA Auto)) }

1
1. rv : InnerProductSpace
2. e : Point
3. x : Point
⊢ x + r0*e ≡ x

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e,x:Point].    hyptrans(rv;e;r0;x)  \mequiv{}  x


By

---

Latex:
((Auto  THEN  RepUR  ``hyptrans``  0)  THEN  ((RWO  "cosh0  sinh0"  0  THENM  nRNorm  0)  THENA  Auto))

---

Home Index