---

Step * 3 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. x : ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. a : ℝ
7. b : ℝ
8. h : {h:Point(rv)| h ⋅ e = r0} 
9. x1 : a ≠ r0
10. x2 : b ≠ r0
⊢ ||T_b(0)|| ≠ r0
BY
{ (Assert ||T_b(0)|| = ||T_b(0) - 0|| BY
         Auto) }

1
.....aux..... 
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. x : ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. a : ℝ
7. b : ℝ
8. h : {h:Point(rv)| h ⋅ e = r0} 
9. x1 : a ≠ r0
10. x2 : b ≠ r0
⊢ ||T_b(0)|| = ||T_b(0) - 0||

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. x : ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. a : ℝ
7. b : ℝ
8. h : {h:Point(rv)| h ⋅ e = r0} 
9. x1 : a ≠ r0
10. x2 : b ≠ r0
11. ||T_b(0)|| = ||T_b(0) - 0||
⊢ ||T_b(0)|| ≠ r0

---

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.  x  :  \mforall{}a:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (a  \mneq{}  r0  {}\mRightarrow{}  (r0  <  ||T\_a(h)  -  h||))
6.  a  :  \mBbbR{}
7.  b  :  \mBbbR{}
8.  h  :  \{h:Point(rv)|  h  \mcdot{}  e  =  r0\} 
9.  x1  :  a  \mneq{}  r0
10.  x2  :  b  \mneq{}  r0
\mvdash{}  ||T\_b(0)||  \mneq{}  r0


By

---

Latex:
(Assert  ||T\_b(0)||  =  ||T\_b(0)  -  0||  BY
              Auto)

---

Home Index