---

Step * 2 1 1 1 1 of Lemma separable-translation-group_iff


1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. ∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
     (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀a:ℝ.  T_a(h) - h ≡ ρ(h;a)*e
⊢ ∃psi:{h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (ρ(h;t) = (ρ(0;t) * (psi h)))
BY
{ Assert ⌜ρ(0;r1) ≠ r0⌝⋅ }

1
.....assertion..... 
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. ∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
     (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀a:ℝ.  T_a(h) - h ≡ ρ(h;a)*e
⊢ ρ(0;r1) ≠ r0

2
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. ∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
     (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀a:ℝ.  T_a(h) - h ≡ ρ(h;a)*e
8. ρ(0;r1) ≠ r0
⊢ ∃psi:{h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (ρ(h;t) = (ρ(0;t) * (psi h)))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  \{e:Point(rv)|  e\^{}2  =  r1\} 
3.  T  :  \mBbbR{}  {}\mrightarrow{}  Point(rv)  {}\mrightarrow{}  Point(rv)
4.  translation-group-fun(rv;e;T)
5.  \mforall{}a:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (a  \mneq{}  r0  {}\mRightarrow{}  (r0  <  ||T\_a(h)  -  h||))
6.  \mforall{}a,b:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .
          (a  \mneq{}  r0  {}\mRightarrow{}  b  \mneq{}  r0  {}\mRightarrow{}  ((||T\_a(h)  -  h||/||T\_b(h)  -  h||)  =  (||T\_a(0)||/||T\_b(0)||)))
7.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}a:\mBbbR{}.    T\_a(h)  -  h  \mequiv{}  \mrho{}(h;a)*e
\mvdash{}  \mexists{}psi:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}
      \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    (\mrho{}(h;t)  =  (\mrho{}(0;t)  *  (psi  h)))


By

---

Latex:
Assert  \mkleeneopen{}\mrho{}(0;r1)  \mneq{}  r0\mkleeneclose{}\mcdot{}

---

Home Index