Nuprl Lemma : mk-inner-product-space_wf

∀[self:RealVectorSpace]. ∀[ip:{ip:Point(self) ⟶ Point(self) ⟶ ℝ| 
                               (∀x1,x2,y1,y2:Point(self).  (x1 ≡ x2 ⇒ y1 ≡ y2 ⇒ ((ip x1 y1) = (ip x2 y2))))
                               ∧ (∀x,y:Point(self).  ((ip x y) = (ip y x)))
                               ∧ (∀x,y,z:Point(self).  ((ip x + y z) = ((ip x z) + (ip y z))))
                               ∧ (∀a:ℝ. ∀x,y:Point(self).  ((ip a*x y) = (a * (ip x y))))} ]. ∀[pos:∀x:Point(self)
                                                                                                     (x # 0
                                                                                                     ⇐⇒ r0 < (ip x 
                                                                                                               x))].
∀[perp:∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((ip x y) = r0))))].
  (vs=self;
   ip=ip;
   positive=pos;
   perp=perp ∈ InnerProductSpace)


Proof



Definitions occuring in Statement :  mk-inner-product-space: mk-inner-product-space,  inner-product-space: InnerProductSpace,  rv-mul: a*x,  rv-add: x + y,  rv-0: 0,  real-vector-space: RealVectorSpace,  rless: x < y,  req: x = y,  rmul: a * b,  radd: a + b,  int-to-real: r(n),  real: ℝ,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  iff: P ⇐⇒ Q,  implies: P ⇒ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ⟶ B[x],  natural_number: $n
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  mk-inner-product-space: mk-inner-product-space,  inner-product-space: InnerProductSpace,  record+: record+,  real-vector-space: RealVectorSpace,  record-select: r.x,  subtype_rel: A ⊆r B,  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  btrue: tt,  and: P ∧ Q,  all: ∀x:A. B[x],  prop: ℙ,  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  or: P ∨ Q,  so_apply: x[s],  record-update: r[x := v],  bool: 𝔹,  unit: Unit,  it: ⋅,  uiff: uiff(P;Q),  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  top: Top,  bfalse: ff,  ss-sep: Error :ss-sep,  ss-point: Error :ss-point,  ss-eq: Error :ss-eq,  rv-0: 0,  rv-mul: a*x,  rv-add: x + y,  iff: P ⇐⇒ Q,  not: ¬A,  rev_implies: P ⇐ Q,  false: False,  exists: ∃x:A. B[x],  separation-space: Error :separation-space,  record: record(x.T[x])
Lemmas referenced :  subtype_rel_self,  Error :ss-point_wf,  Error :ss-eq_wf,  all_wf,  Error :ss-sep_wf,  or_wf,  real_wf,  int-to-real_wf,  rmul_wf,  radd_wf,  rneq_wf,  eq_atom_wf,  uiff_transitivity,  equal-wf-base,  bool_wf,  atom_subtype_base,  assert_wf,  eqtt_to_assert,  assert_of_eq_atom,  subtype_base_sq,  rec_select_update_lemma,  istype-void,  iff_transitivity,  bnot_wf,  not_wf,  iff_weakening_uiff,  eqff_to_assert,  assert_of_bnot,  istype-assert,  istype-atom,  real-vector-space_subtype1,  rv-0_wf,  req_wf,  rless_wf,  rv-add_wf,  rv-mul_wf,  real-vector-space_wf,  record-select_wf,  top_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  introduction,  cut,  hypothesisEquality,  sqequalRule,  dependentIntersection_memberEquality,  sqequalHypSubstitution,  dependentIntersectionElimination,  dependentIntersectionEqElimination,  thin,  hypothesis,  applyEquality,  tokenEquality,  extract_by_obid,  isectElimination,  setEquality,  functionEquality,  productEquality,  lambdaEquality_alt,  because_Cache,  applyLambdaEquality,  setElimination,  rename,  inhabitedIsType,  equalityTransitivity,  equalitySymmetry,  universeIsType,  closedConclusion,  natural_numberEquality,  functionExtensionality_alt,  lambdaFormation_alt,  unionElimination,  equalityElimination,  baseApply,  baseClosed,  atomEquality,  independent_functionElimination,  productElimination,  independent_isectElimination,  instantiate,  cumulativity,  dependent_functionElimination,  isect_memberEquality_alt,  voidElimination,  independent_pairFormation,  equalityIstype,  sqequalBase,  functionIsType,  functionExtensionality,  axiomEquality,  productIsType,  isectIsTypeImplies,  setIsType,  universeEquality
Latex:
\mforall{}[self:RealVectorSpace].  \mforall{}[ip:\{ip:Point(self)  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  \mBbbR{}| 
                                                              (\mforall{}x1,x2,y1,y2:Point(self).
                                                                    (x1  \mequiv{}  x2  {}\mRightarrow{}  y1  \mequiv{}  y2  {}\mRightarrow{}  ((ip  x1  y1)  =  (ip  x2  y2))))
                                                              \mwedge{}  (\mforall{}x,y:Point(self).    ((ip  x  y)  =  (ip  y  x)))
                                                              \mwedge{}  (\mforall{}x,y,z:Point(self).    ((ip  x  +  y  z)  =  ((ip  x  z)  +  (ip  y  z))))
                                                              \mwedge{}  (\mforall{}a:\mBbbR{}.  \mforall{}x,y:Point(self).    ((ip  a*x  y)  =  (a  *  (ip  x  y))))\}  ].
\mforall{}[pos:\mforall{}x:Point(self).  (x  \#  0  \mLeftarrow{}{}\mRightarrow{}  r0  <  (ip  x  x))].  \mforall{}[perp:\mforall{}x:Point(self)
                                                                                                                      (x  \#  0
                                                                                                                      {}\mRightarrow{}  (\mexists{}y:Point(self)
                                                                                                                                (y  \#  0  \mwedge{}  ((ip  x  y)  =  r0))))].
    (vs=self;
      ip=ip;
      positive=pos;
      perp=perp  \mmember{}  InnerProductSpace)


Date html generated: 2020_05_20-PM-01_10_43
Last ObjectModification: 2019_12_10-AM-00_48_36

Theory : inner!product!spaces


Home Index