---

Step * 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. translation-group-fun(rv;e;T)
6. separable-kernel(rv;e;λh,t. ρ(h;t))
7. phi : ℝ ⟶ ℝ
8. psi : {h:Point(rv)| h ⋅ e = r0}  ⟶ {r:ℝ| r0 < r} 
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (((λh,t. ρ(h;t)) h t) = ((phi t) * (psi h)))
10. (phi r0) = r0
11. (psi 0) = r1
12. ∀t,s:ℝ.  ((t < s) ⇒ ((phi t) < (phi s)))
13. ∀t:ℝ. ∃s:ℝ. ((phi s) = t)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  (psi h1 ≠ psi h2 ⇒ h1 # h2)
15. ∀t,s:ℝ.  (phi t ≠ phi s ⇒ t ≠ s)
⊢ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
∧ (∀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)||))))
BY
{ (All Reduce
   THEN (Assert ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (||T_t(h) - h|| = (|phi t| * (psi h))) BY
               (Auto
                THEN (RWO "trans-kernel-equation" 0 THENA Auto)
                THEN (Assert h + ρ(h;t)*e - h ≡ ρ(h;t)*e BY
                            (RealVecEqual THEN Auto))
                THEN (RWW "-1 9" 0 THENA Auto)
                THEN GenConclTerms Auto [⌜phi t⌝;⌜psi h⌝]⋅
                THEN (RWW "rv-norm-mul rabs-rmul" 0 THENA 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. translation-group-fun(rv;e;T)
6. separable-kernel(rv;e;λh,t. ρ(h;t))
7. phi : ℝ ⟶ ℝ
8. psi : {h:Point(rv)| h ⋅ e = r0}  ⟶ {r:ℝ| r0 < r} 
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (ρ(h;t) = ((phi t) * (psi h)))
10. (phi r0) = r0
11. (psi 0) = r1
12. ∀t,s:ℝ.  ((t < s) ⇒ ((phi t) < (phi s)))
13. ∀t:ℝ. ∃s:ℝ. ((phi s) = t)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  (psi h1 ≠ psi h2 ⇒ h1 # h2)
15. ∀t,s:ℝ.  (phi t ≠ phi s ⇒ t ≠ s)
16. h : {h:Point(rv)| h ⋅ e = r0} 
17. t : ℝ
18. h + ρ(h;t)*e - h ≡ ρ(h;t)*e
19. v : ℝ
20. (phi t) = v ∈ ℝ
21. v1 : {r:ℝ| r0 < r} 
22. (psi h) = v1 ∈ {r:ℝ| r0 < r} 
⊢ ((|v| * |v1|) * ||e||) = (|v| * v1)

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. translation-group-fun(rv;e;T)
6. separable-kernel(rv;e;λh,t. ρ(h;t))
7. phi : ℝ ⟶ ℝ
8. psi : {h:Point(rv)| h ⋅ e = r0}  ⟶ {r:ℝ| r0 < r} 
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (ρ(h;t) = ((phi t) * (psi h)))
10. (phi r0) = r0
11. (psi 0) = r1
12. ∀t,s:ℝ.  ((t < s) ⇒ ((phi t) < (phi s)))
13. ∀t:ℝ. ∃s:ℝ. ((phi s) = t)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  (psi h1 ≠ psi h2 ⇒ h1 # h2)
15. ∀t,s:ℝ.  (phi t ≠ phi s ⇒ t ≠ s)
16. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  (||T_t(h) - h|| = (|phi t| * (psi h)))
⊢ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
∧ (∀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)||))))

---

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.  translation-group-fun(rv;e;T)
6.  separable-kernel(rv;e;\mlambda{}h,t.  \mrho{}(h;t))
7.  phi  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
8.  psi  :  \{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \{r:\mBbbR{}|  r0  <  r\} 
9.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    (((\mlambda{}h,t.  \mrho{}(h;t))  h  t)  =  ((phi  t)  *  (psi  h)))
10.  (phi  r0)  =  r0
11.  (psi  0)  =  r1
12.  \mforall{}t,s:\mBbbR{}.    ((t  <  s)  {}\mRightarrow{}  ((phi  t)  <  (phi  s)))
13.  \mforall{}t:\mBbbR{}.  \mexists{}s:\mBbbR{}.  ((phi  s)  =  t)
14.  \mforall{}h1,h2:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (psi  h1  \mneq{}  psi  h2  {}\mRightarrow{}  h1  \#  h2)
15.  \mforall{}t,s:\mBbbR{}.    (phi  t  \mneq{}  phi  s  {}\mRightarrow{}  t  \mneq{}  s)
\mvdash{}  (\mforall{}a:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (a  \mneq{}  r0  {}\mRightarrow{}  (r0  <  ||T\_a(h)  -  h||)))
\mwedge{}  (\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)||))))


By

---

Latex:
(All  Reduce
  THEN  (Assert  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    (||T\_t(h)  -  h||  =  (|phi  t|  *  (psi  h)))  BY
                          (Auto
                            THEN  (RWO  "trans-kernel-equation"  0  THENA  Auto)
                            THEN  (Assert  h  +  \mrho{}(h;t)*e  -  h  \mequiv{}  \mrho{}(h;t)*e  BY
                                                    (RealVecEqual  THEN  Auto))
                            THEN  (RWW  "-1  9"  0  THENA  Auto)
                            THEN  GenConclTerms  Auto  [\mkleeneopen{}phi  t\mkleeneclose{};\mkleeneopen{}psi  h\mkleeneclose{}]\mcdot{}
                            THEN  (RWW  "rv-norm-mul  rabs-rmul"  0  THENA  Auto)))
  )

---

Home Index