---

Step * of Lemma hyptrans-perm_wf

∀[rv:InnerProductSpace]. ∀[e:Point]. ∀[t:ℝ].  hyptrans-perm(rv;e;t) ∈ Point supposing e^2 = r1
BY
{ (Auto THEN (InstLemma `translation-group-point`  [⌜rv⌝;⌜e⌝;⌜λt,x. hyptrans(rv;e;t;x)⌝]⋅ THENA EAuto 1) THEN Reduce -1)\000C }

1
1. rv : InnerProductSpace
2. e : Point
3. t : ℝ
4. e^2 = r1
5. Point ≡ {fg:Point ⟶ Point × (Point ⟶ Point)| 
            ∃t:ℝ. ((∀x:Point. (fst(fg)) x ≡ hyptrans(rv;e;t;x)) ∧ (∀x:Point. (snd(fg)) x ≡ hyptrans(rv;e;-(t);x)))} 
⊢ hyptrans-perm(rv;e;t) ∈ Point

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e:Point].  \mforall{}[t:\mBbbR{}].    hyptrans-perm(rv;e;t)  \mmember{}  Point  supposing  e\^{}2  =  r1


By

---

Latex:
(Auto
  THEN  (InstLemma  `translation-group-point`    [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}\mlambda{}t,x.  hyptrans(rv;e;t;x)\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  Reduce  -1)

---

Home Index