---

Step * of Lemma hyptrans_add

∀[rv:InnerProductSpace]. ∀[e,x:Point]. ∀[t,s:ℝ].
  hyptrans(rv;e;t + s;x) ≡ hyptrans(rv;e;t;hyptrans(rv;e;s;x)) supposing e^2 = r1
BY
{ (Auto
   THEN (InstLemma `hyptrans_decomp` [⌜rv⌝;⌜e⌝;⌜x⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (RWW "hyptrans_lemma -1" 0 THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e,x:Point].  \mforall{}[t,s:\mBbbR{}].
    hyptrans(rv;e;t  +  s;x)  \mequiv{}  hyptrans(rv;e;t;hyptrans(rv;e;s;x))  supposing  e\^{}2  =  r1


By

---

Latex:
(Auto
  THEN  (InstLemma  `hyptrans\_decomp`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (RWW  "hyptrans\_lemma  -1"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index