---

Step * 1 of Lemma hyptrans_decomp


1. rv : InnerProductSpace
2. e : Point
3. x : Point
4. e^2 = r1
⊢ ∃h:Point. ∃tau:ℝ. ((h ⋅ e = r0) ∧ x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e)
BY
{ ((InstLemma `rv-decomp_wf` [⌜rv⌝;⌜e⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Assert rsqrt(r1 + fst(rv-decomp(rv;x;e))^2) ≠ r0 BY
               (OrRight THEN Auto))
   THEN (InstConcl [⌜fst(rv-decomp(rv;x;e))⌝;⌜inv-sinh((snd(rv-decomp(rv;x;e))/rsqrt(r1 + fst(rv-decomp(rv;x;e))^2)))⌝]⋅
         THENA Auto
         )) }

1
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

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  x  :  Point
4.  e\^{}2  =  r1
\mvdash{}  \mexists{}h:Point.  \mexists{}tau:\mBbbR{}.  ((h  \mcdot{}  e  =  r0)  \mwedge{}  x  \mequiv{}  h  +  sinh(tau)  *  rsqrt(r1  +  h\^{}2)*e)


By

---

Latex:
((InstLemma  `rv-decomp\_wf`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  rsqrt(r1  +  fst(rv-decomp(rv;x;e))\^{}2)  \mneq{}  r0  BY
                          (OrRight  THEN  Auto))
  THEN  (InstConcl  [\mkleeneopen{}fst(rv-decomp(rv;x;e))\mkleeneclose{};\mkleeneopen{}inv-sinh((snd(rv-decomp(rv;x;e))/rsqrt(r1
                                                                                        +  fst(rv-decomp(rv;x;e))\^{}2)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index