Step
*
1
1
2
1
1
of Lemma
trans-from-kernel-is-trans
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1}
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. e^2 = r1
6. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
8. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
11. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
12. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (g h1 t1 ≠ g h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
13. trans-kernel-fun(rv;e;f)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
16. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀tau,t:ℝ. trans-from-kernel(rv;e;f;g;t;h + f h tau*e) ≡ h + f h (tau + t)*e
17. ∀x:Point(rv). ∃h:{h:Point(rv)| h ⋅ e = r0} . ∃tau:ℝ. x ≡ h + f h tau*e
⊢ translation-group-fun(rv;e;λt,x. trans-from-kernel(rv;e;f;g;t;x))
BY
{ (D 0 THEN Reduce 0) }
1
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1}
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. e^2 = r1
6. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
8. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
11. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
12. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (g h1 t1 ≠ g h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
13. trans-kernel-fun(rv;e;f)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
16. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀tau,t:ℝ. trans-from-kernel(rv;e;f;g;t;h + f h tau*e) ≡ h + f h (tau + t)*e
17. ∀x:Point(rv). ∃h:{h:Point(rv)| h ⋅ e = r0} . ∃tau:ℝ. x ≡ h + f h tau*e
⊢ ∀s,t:ℝ. ∀x,y:Point(rv). (trans-from-kernel(rv;e;f;g;s;x) # trans-from-kernel(rv;e;f;g;t;y) ⇒ (x # y ∨ s ≠ t))
2
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1}
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. e^2 = r1
6. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
8. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
11. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
12. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (g h1 t1 ≠ g h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
13. trans-kernel-fun(rv;e;f)
14. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
16. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀tau,t:ℝ. trans-from-kernel(rv;e;f;g;t;h + f h tau*e) ≡ h + f h (tau + t)*e
17. ∀x:Point(rv). ∃h:{h:Point(rv)| h ⋅ e = r0} . ∃tau:ℝ. x ≡ h + f h tau*e
⊢ (∀t,s:ℝ. ∀x:Point(rv).
trans-from-kernel(rv;e;f;g;t + s;x) ≡ trans-from-kernel(rv;e;f;g;t;trans-from-kernel(rv;e;f;g;s;x)))
∧ (∀x:Point(rv). ∀r:ℝ.
∃t:ℝ. (trans-from-kernel(rv;e;f;g;t;x) ≡ x + r*e ∧ (∀y:ℝ. (y ≠ t ⇒ trans-from-kernel(rv;e;f;g;y;x) # x + r*e))))
∧ (∀x:Point(rv). ∀t:{t:ℝ| r0 ≤ t} . ∃r:{t:ℝ| r0 ≤ t} . trans-from-kernel(rv;e;f;g;t;x) ≡ x + r*e)
Latex:
Latex:
1. rv : InnerProductSpace
2. e : \{e:Point(rv)| e\^{}2 = r1\}
3. f : \{h:Point(rv)| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
4. g : \{h:Point(rv)| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
5. e\^{}2 = r1
6. \mforall{}h1,h2:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (f h1 t1 \mneq{} f h2 t2 {}\mRightarrow{} (h1 \# h2 \mvee{} t1 \mneq{} t2))
7. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . ((f h r0) = r0)
8. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. ((t1 < t2) {}\mRightarrow{} ((f h t1) < (f h t2)))
9. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. \mexists{}t:\mBbbR{}. ((f h t) = r)
10. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. ((f h (g h r)) = r)
11. \mforall{}h1,h2:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (h1 \mequiv{} h2 {}\mRightarrow{} (t1 = t2) {}\mRightarrow{} ((f h1 t1) = (f h2 t2)))
12. \mforall{}h1,h2:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (g h1 t1 \mneq{} g h2 t2 {}\mRightarrow{} (h1 \# h2 \mvee{} t1 \mneq{} t2))
13. trans-kernel-fun(rv;e;f)
14. \mforall{}h1,h2:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (h1 \mequiv{} h2 {}\mRightarrow{} (t1 = t2) {}\mRightarrow{} ((g h1 t1) = (g h2 t2)))
15. \mforall{}y:Point(rv). (y - y \mcdot{} e*e \mmember{} \{h:Point(rv)| h \mcdot{} e = r0\} )
16. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}tau,t:\mBbbR{}.
trans-from-kernel(rv;e;f;g;t;h + f h tau*e) \mequiv{} h + f h (tau + t)*e
17. \mforall{}x:Point(rv). \mexists{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mexists{}tau:\mBbbR{}. x \mequiv{} h + f h tau*e
\mvdash{} translation-group-fun(rv;e;\mlambda{}t,x. trans-from-kernel(rv;e;f;g;t;x))
By
Latex:
(D 0 THEN Reduce 0)
Home
Index