---

Step * of Lemma hyptrans-is-translation-group-fun

∀rv:InnerProductSpace. ∀e:Point.  ((e^2 = r1) ⇒ translation-group-fun(rv;e;λt,x. hyptrans(rv;e;t;x)))
BY
{ ((Auto THEN D 0)
   THEN Reduce 0
   THEN SplitAndConcl
   THEN Try (((InstLemma `hyptrans_ext` [⌜rv⌝;⌜e⌝]⋅ THENA Auto) THEN Trivial))
   THEN InstLemma `hyptrans_add` [⌜rv⌝;⌜e⌝]⋅
   THEN Auto
   THEN (InstLemma `hyptrans_decomp` [⌜rv⌝;⌜e⌝;⌜x⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN Try (UnfoldTop `exists!` 0)
   THEN (RWW "hyptrans_lemma -1" 0 THENA Auto)
   THEN (Assert r0 < rsqrt(r1 + h^2) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl  ⌜rsqrt(r1 + h^2) = a ∈ ℝ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. e : Point
3. e^2 = r1
4. ∀[x:Point]. ∀[t,s:ℝ].  hyptrans(rv;e;t + s;x) ≡ hyptrans(rv;e;t;hyptrans(rv;e;s;x)) supposing e^2 = r1
5. x : Point
6. r : ℝ
7. h : Point
8. tau : ℝ
9. h ⋅ e = r0
10. x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e
11. a : ℝ
12. rsqrt(r1 + h^2) = a ∈ ℝ
13. r0 < a
⊢ ∃t:ℝ
   (h + sinh(tau + t) * a*e ≡ h + sinh(tau) * a*e + r*e
   ∧ (∀y:ℝ. (y ≠ t ⇒ h + sinh(tau + y) * a*e # h + sinh(tau) * a*e + r*e)))

2
1. rv : InnerProductSpace
2. e : Point
3. e^2 = r1
4. ∀[x:Point]. ∀[t,s:ℝ].  hyptrans(rv;e;t + s;x) ≡ hyptrans(rv;e;t;hyptrans(rv;e;s;x)) supposing e^2 = r1
5. x : Point
6. t : {t:ℝ| r0 ≤ t} 
7. h : Point
8. tau : ℝ
9. h ⋅ e = r0
10. x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e
11. a : ℝ
12. rsqrt(r1 + h^2) = a ∈ ℝ
13. r0 < a
⊢ ∃r:{t:ℝ| r0 ≤ t} . h + sinh(tau + t) * a*e ≡ h + sinh(tau) * a*e + r*e

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.    ((e\^{}2  =  r1)  {}\mRightarrow{}  translation-group-fun(rv;e;\mlambda{}t,x.  hyptrans(rv;e;t;x)\000C))


By

---

Latex:
((Auto  THEN  D  0)
  THEN  Reduce  0
  THEN  SplitAndConcl
  THEN  Try  (((InstLemma  `hyptrans\_ext`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Trivial))
  THEN  InstLemma  `hyptrans\_add`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `hyptrans\_decomp`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  Try  (UnfoldTop  `exists!`  0)
  THEN  (RWW  "hyptrans\_lemma  -1"  0  THENA  Auto)
  THEN  (Assert  r0  <  rsqrt(r1  +  h\^{}2)  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl    \mkleeneopen{}rsqrt(r1  +  h\^{}2)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index