Step
*
1
1
3
of Lemma
separable-kernel-properties
1. rv : InnerProductSpace
2. e : Point(rv)
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
5. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = (((g t) * (k 0)) * ((λh.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((λh.(k h/k 0)) 0) = r1
16. ∀t,s:ℝ. ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0))))
17. ∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t)
18. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ((λh.(k h/k 0)) h1 ≠ (λh.(k h/k 0)) h2 ⇒ h1 # h2)
19. t : ℝ
20. s : ℝ
21. (g t) * (k 0) ≠ (g s) * (k 0)
⊢ t ≠ s
BY
{ ((FLemma `rneq-rmul` [-1] THENA Auto) THEN D -1) }
1
1. rv : InnerProductSpace
2. e : Point(rv)
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
5. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = (((g t) * (k 0)) * ((λh.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((λh.(k h/k 0)) 0) = r1
16. ∀t,s:ℝ. ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0))))
17. ∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t)
18. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ((λh.(k h/k 0)) h1 ≠ (λh.(k h/k 0)) h2 ⇒ h1 # h2)
19. t : ℝ
20. s : ℝ
21. (g t) * (k 0) ≠ (g s) * (k 0)
22. g t ≠ g s
⊢ t ≠ s
2
1. rv : InnerProductSpace
2. e : Point(rv)
3. f : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ
4. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
5. ∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0} ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = (((g t) * (k 0)) * ((λh.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((λh.(k h/k 0)) 0) = r1
16. ∀t,s:ℝ. ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0))))
17. ∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t)
18. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ((λh.(k h/k 0)) h1 ≠ (λh.(k h/k 0)) h2 ⇒ h1 # h2)
19. t : ℝ
20. s : ℝ
21. (g t) * (k 0) ≠ (g s) * (k 0)
22. k 0 ≠ k 0
⊢ t ≠ s
Latex:
Latex:
1. rv : InnerProductSpace
2. e : Point(rv)
3. f : \{h:Point(rv)| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
4. \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))
5. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . ((f h r0) = r0)
6. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. ((t1 < t2) {}\mRightarrow{} ((f h t1) < (f h t2)))
7. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. \mexists{}t:\mBbbR{}. ((f h t) = r)
8. g : \mBbbR{} {}\mrightarrow{} \mBbbR{}
9. k : \{h:Point(rv)| h \mcdot{} e = r0\} {}\mrightarrow{} \mBbbR{}
10. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t:\mBbbR{}. ((f h t) = ((g t) * (k h)))
11. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . k h \mneq{} r0
12. k 0 \mneq{} r0
13. \mforall{}h:\{h:Point(rv)| h \mcdot{} e = r0\} . \mforall{}t:\mBbbR{}. ((f h t) = (((g t) * (k 0)) * ((\mlambda{}h.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((\mlambda{}h.(k h/k 0)) 0) = r1
16. \mforall{}t,s:\mBbbR{}. ((t < s) {}\mRightarrow{} (((g t) * (k 0)) < ((g s) * (k 0))))
17. \mforall{}t:\mBbbR{}. \mexists{}s:\mBbbR{}. (((g s) * (k 0)) = t)
18. \mforall{}h1,h2:\{h:Point(rv)| h \mcdot{} e = r0\} . ((\mlambda{}h.(k h/k 0)) h1 \mneq{} (\mlambda{}h.(k h/k 0)) h2 {}\mRightarrow{} h1 \# h2)
19. t : \mBbbR{}
20. s : \mBbbR{}
21. (g t) * (k 0) \mneq{} (g s) * (k 0)
\mvdash{} t \mneq{} s
By
Latex:
((FLemma `rneq-rmul` [-1] THENA Auto) THEN D -1)
Home
Index