---

Step * of Lemma hyptrans_ext

∀rv:InnerProductSpace. ∀e:Point. ∀s,t:ℝ. ∀x,y:Point.  (hyptrans(rv;e;s;x) # hyptrans(rv;e;t;y) ⇒ (x # y ∨ s ≠ t))
BY
{ (Auto
   THEN Unfold `hyptrans` -1
   THEN ((FLemma `rv-add-sep` [-1] THENM D -1) THEN Auto)
   THEN (FLemma `rv-mul-sep` [-1] THENM D -1)
   THEN Auto) }

1
1. rv : InnerProductSpace
2. e : Point
3. s : ℝ
4. t : ℝ
5. x : Point
6. y : Point
7. x + (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # y + (y ⋅ e * (cosh(t) - r1))
+ (rsqrt(r1 + y^2) * sinh(t))*e
8. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))*e
9. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s)) ≠ (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))
⊢ x # y ∨ s ≠ t

2
1. rv : InnerProductSpace
2. e : Point
3. s : ℝ
4. t : ℝ
5. x : Point
6. y : Point
7. x + (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # y + (y ⋅ e * (cosh(t) - r1))
+ (rsqrt(r1 + y^2) * sinh(t))*e
8. (x ⋅ e * (cosh(s) - r1)) + (rsqrt(r1 + x^2) * sinh(s))*e # (y ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + y^2) * sinh(t))*e
9. e # e
⊢ x # y ∨ s ≠ t

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}s,t:\mBbbR{}.  \mforall{}x,y:Point.
    (hyptrans(rv;e;s;x)  \#  hyptrans(rv;e;t;y)  {}\mRightarrow{}  (x  \#  y  \mvee{}  s  \mneq{}  t))


By

---

Latex:
(Auto
  THEN  Unfold  `hyptrans`  -1
  THEN  ((FLemma  `rv-add-sep`  [-1]  THENM  D  -1)  THEN  Auto)
  THEN  (FLemma  `rv-mul-sep`  [-1]  THENM  D  -1)
  THEN  Auto)

---

Home Index