---

Step * 1 1 of Lemma hyptrans_decomp


1. rv : InnerProductSpace
2. e : Point
3. x : Point
4. e^2 = r1
5. rv-decomp(rv;x;e) ∈ {p:Point × ℝ| x ≡ fst(p) + snd(p)*e ∧ (fst(p) ⋅ e = r0)} 
6. rsqrt(r1 + fst(rv-decomp(rv;x;e))^2) ≠ r0
⊢ (fst(rv-decomp(rv;x;e)) ⋅ e = r0)
∧ x ≡ fst(rv-decomp(rv;x;e)) + sinh(inv-sinh((snd(rv-decomp(rv;x;e))/rsqrt(r1 + fst(rv-decomp(rv;x;e))^2))))
  * rsqrt(r1 + fst(rv-decomp(rv;x;e))^2)*e
BY
{ ((GenConclTerm ⌜rv-decomp(rv;x;e)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN D -2
   THEN All Reduce
   THEN (Assert rsqrt(r1 + v1^2) ≠ r0 BY
               (OrRight THEN Auto))
   THEN (RWO "sinh-inv-sinh" 0 THENA Auto)
   THEN (nRNorm 0 THEN Auto)
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  x  :  Point
4.  e\^{}2  =  r1
5.  rv-decomp(rv;x;e)  \mmember{}  \{p:Point  \mtimes{}  \mBbbR{}|  x  \mequiv{}  fst(p)  +  snd(p)*e  \mwedge{}  (fst(p)  \mcdot{}  e  =  r0)\} 
6.  rsqrt(r1  +  fst(rv-decomp(rv;x;e))\^{}2)  \mneq{}  r0
\mvdash{}  (fst(rv-decomp(rv;x;e))  \mcdot{}  e  =  r0)
\mwedge{}  x  \mequiv{}  fst(rv-decomp(rv;x;e))  +  sinh(inv-sinh((snd(rv-decomp(rv;x;e))/rsqrt(r1
    +  fst(rv-decomp(rv;x;e))\^{}2))))
    *  rsqrt(r1  +  fst(rv-decomp(rv;x;e))\^{}2)*e


By

---

Latex:
((GenConclTerm  \mkleeneopen{}rv-decomp(rv;x;e)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  D  -2
  THEN  All  Reduce
  THEN  (Assert  rsqrt(r1  +  v1\^{}2)  \mneq{}  r0  BY
                          (OrRight  THEN  Auto))
  THEN  (RWO  "sinh-inv-sinh"  0  THENA  Auto)
  THEN  (nRNorm  0  THEN  Auto)
  THEN  Unhide
  THEN  Auto)

---

Home Index