Nuprl Lemma : trans-kernel-0

rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  ((e^2 r1)  translation-group-fun(rv;e;T)  (∀h:{h:Point| h ⋅ r0} (h;r0) r0)))


Proof




Definitions occuring in Statement :  trans-kernel: ρ(h;t) translation-group-fun: translation-group-fun(rv;e;T) rv-ip: x ⋅ y inner-product-space: InnerProductSpace req: y int-to-real: r(n) real: ss-point: Point all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T trans-kernel-fun: trans-kernel-fun(rv;e;f) and: P ∧ Q prop: uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  trans-kernel-is-kernel-fun set_wf ss-point_wf real-vector-space_subtype1 inner-product-space_subtype subtype_rel_transitivity inner-product-space_wf real-vector-space_wf separation-space_wf req_wf rv-ip_wf int-to-real_wf translation-group-fun_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis productElimination sqequalRule isectElimination applyEquality instantiate independent_isectElimination lambdaEquality natural_numberEquality because_Cache functionExtensionality functionEquality

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    ((e\^{}2  =  r1)  {}\mRightarrow{}  translation-group-fun(rv;e;T)  {}\mRightarrow{}  (\mforall{}h:\{h:Point|  h  \mcdot{}  e  =  r0\}  .  (\mrho{}(h;r0)  =  r0)))



Date html generated: 2017_10_05-AM-00_23_23
Last ObjectModification: 2017_07_02-PM-03_19_12

Theory : inner!product!spaces


Home Index