Step
*
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. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
14. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
⊢ translation-group-fun(rv;e;λt,x. trans-from-kernel(rv;e;f;g;t;x))
BY
{ (Assert ∀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 BY
(RepeatFor 3 ((D 0 THENA Auto))
THEN Unfold `trans-from-kernel` 0
THEN (GenConclTerm ⌜rv-decomp(rv;h + f h tau*e;e)⌝⋅ THENA Auto)
THEN RepeatFor 2 (DVar `v')
THEN All Reduce
THEN (Unhide THENA Auto)
THEN (Assert h ⋅ e = r0 BY
(DVar `h' THEN Unhide THEN Auto))
THEN PromoteHyp (-1) (-3)
THEN RepUR ``rv-decomp`` -1
THEN (EqTypeHD (-1) THENA Auto)
THEN Thin (-1)
THEN (EqHD (-1) THENA Auto)
THEN All Reduce)) }
1
.....aux.....
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. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
14. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
15. h : {h:Point(rv)| h ⋅ e = r0}
16. tau : ℝ
17. t : ℝ
18. v1 : Point(rv)
19. v2 : ℝ
20. h ⋅ e = r0
21. h + f h tau*e ≡ v1 + v2*e ∧ (v1 ⋅ e = r0)
22. h + f h tau*e - h + f h tau*e ⋅ e*e = v1 ∈ Point(rv)
23. h + f h tau*e ⋅ e = v2 ∈ ℝ
⊢ v1 + f v1 ((g v1 v2) + t)*e ≡ h + f h (tau + t)*e
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. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
14. ∀y:Point(rv). (y - y ⋅ e*e ∈ {h:Point(rv)| h ⋅ e = r0} )
15. ∀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
⊢ translation-group-fun(rv;e;λt,x. trans-from-kernel(rv;e;f;g;t;x))
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. \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)))
14. \mforall{}y:Point(rv). (y - y \mcdot{} e*e \mmember{} \{h:Point(rv)| h \mcdot{} e = r0\} )
\mvdash{} translation-group-fun(rv;e;\mlambda{}t,x. trans-from-kernel(rv;e;f;g;t;x))
By
Latex:
(Assert \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 BY
(RepeatFor 3 ((D 0 THENA Auto))
THEN Unfold `trans-from-kernel` 0
THEN (GenConclTerm \mkleeneopen{}rv-decomp(rv;h + f h tau*e;e)\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepeatFor 2 (DVar `v')
THEN All Reduce
THEN (Unhide THENA Auto)
THEN (Assert h \mcdot{} e = r0 BY
(DVar `h' THEN Unhide THEN Auto))
THEN PromoteHyp (-1) (-3)
THEN RepUR ``rv-decomp`` -1
THEN (EqTypeHD (-1) THENA Auto)
THEN Thin (-1)
THEN (EqHD (-1) THENA Auto)
THEN All Reduce))
Home
Index