Step
*
1
1
1
of Lemma
kernel-trans-from-kernel
1. rv : InnerProductSpace
2. e : {e:Point| e^2 = r1}
3. f : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
6. ∀h:{h:Point| h ⋅ e = r0} . ((f h r0) = r0)
7. ∀h:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
8. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
9. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
10. h : Point
11. [%22] : h ⋅ e = r0
12. t : ℝ
13. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
14. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. h ⋅ e = r0
16. h - h ⋅ e*e ⋅ e = r0
17. h - h ⋅ e*e ≡ h
18. (g h - h ⋅ e*e h ⋅ e) = (g h r0)
⊢ h - h ⋅ e*e + f h - h ⋅ e*e ((g h - h ⋅ e*e h ⋅ e) + t)*e ⋅ e = (f h t)
BY
{ Assert ⌜(f h - h ⋅ e*e ((g h - h ⋅ e*e h ⋅ e) + t)) = (f h t)⌝⋅ }
1
.....assertion.....
1. rv : InnerProductSpace
2. e : {e:Point| e^2 = r1}
3. f : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
6. ∀h:{h:Point| h ⋅ e = r0} . ((f h r0) = r0)
7. ∀h:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
8. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
9. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
10. h : Point
11. [%22] : h ⋅ e = r0
12. t : ℝ
13. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
14. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. h ⋅ e = r0
16. h - h ⋅ e*e ⋅ e = r0
17. h - h ⋅ e*e ≡ h
18. (g h - h ⋅ e*e h ⋅ e) = (g h r0)
⊢ (f h - h ⋅ e*e ((g h - h ⋅ e*e h ⋅ e) + t)) = (f h t)
2
1. rv : InnerProductSpace
2. e : {e:Point| e^2 = r1}
3. f : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. g : {h:Point| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
5. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
6. ∀h:{h:Point| h ⋅ e = r0} . ((f h r0) = r0)
7. ∀h:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
8. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
9. ∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r)
10. h : Point
11. [%22] : h ⋅ e = r0
12. t : ℝ
13. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2)))
14. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))
15. h ⋅ e = r0
16. h - h ⋅ e*e ⋅ e = r0
17. h - h ⋅ e*e ≡ h
18. (g h - h ⋅ e*e h ⋅ e) = (g h r0)
19. (f h - h ⋅ e*e ((g h - h ⋅ e*e h ⋅ e) + t)) = (f h t)
⊢ h - h ⋅ e*e + f h - h ⋅ e*e ((g h - h ⋅ e*e h ⋅ e) + t)*e ⋅ e = (f h t)
Latex:
Latex:
1. rv : InnerProductSpace
2. e : \{e:Point| e\^{}2 = r1\}
3. f : \{h:Point| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
4. g : \{h:Point| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
5. \mforall{}h1,h2:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (f h1 t1 \mneq{} f h2 t2 {}\mRightarrow{} (h1 \# h2 \mvee{} t1 \mneq{} t2))
6. \mforall{}h:\{h:Point| h \mcdot{} e = r0\} . ((f h r0) = r0)
7. \mforall{}h:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. ((t1 < t2) {}\mRightarrow{} ((f h t1) < (f h t2)))
8. \mforall{}h:\{h:Point| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. \mexists{}t:\mBbbR{}. ((f h t) = r)
9. \mforall{}h:\{h:Point| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. ((f h (g h r)) = r)
10. h : Point
11. [\%22] : h \mcdot{} e = r0
12. t : \mBbbR{}
13. \mforall{}h1,h2:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (h1 \mequiv{} h2 {}\mRightarrow{} (t1 = t2) {}\mRightarrow{} ((f h1 t1) = (f h2 t2)))
14. \mforall{}h1,h2:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (h1 \mequiv{} h2 {}\mRightarrow{} (t1 = t2) {}\mRightarrow{} ((g h1 t1) = (g h2 t2)))
15. h \mcdot{} e = r0
16. h - h \mcdot{} e*e \mcdot{} e = r0
17. h - h \mcdot{} e*e \mequiv{} h
18. (g h - h \mcdot{} e*e h \mcdot{} e) = (g h r0)
\mvdash{} h - h \mcdot{} e*e + f h - h \mcdot{} e*e ((g h - h \mcdot{} e*e h \mcdot{} e) + t)*e \mcdot{} e = (f h t)
By
Latex:
Assert \mkleeneopen{}(f h - h \mcdot{} e*e ((g h - h \mcdot{} e*e h \mcdot{} e) + t)) = (f h t)\mkleeneclose{}\mcdot{}
Home
Index