Nuprl Lemma : mk-real-vector-space_wf

∀[self:SeparationSpace]. ∀[z:Point(self)]. ∀[p:{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
                                                (∀x,y,z:Point(self).  f x (f y z) ≡ f (f x y) z)
                                                ∧ (∀x,y:Point(self).  f x y ≡ f y x)} ].
∀[m:{m:ℝ ⟶ Point(self) ⟶ Point(self)| 
     (∀a:ℝ. ∀x,y:Point(self).  m a (p x y) ≡ p (m a x) (m a y))
     ∧ (∀x:Point(self)
          (m r1 x ≡ x
          ∧ m r0 x ≡ z
          ∧ (∀a,b:ℝ.  m a (m b x) ≡ m (a * b) x)
          ∧ (∀a,b:ℝ.  m (a + b) x ≡ p (m a x) (m b x))))} ]. ∀[psep:∀x,x',y,y':Point(self).
                                                                     (p x y # p x' y' ⇒ (x # x' ∨ y # y'))].
∀[msep:∀a,b:ℝ. ∀x,y:Point(self).  (m a x # m b y ⇒ (a ≠ b ∨ x # y))].
  (ss=self;
   0=z;
   +=p;
   *=m;
   +sep=psep;
   *sep=msep ∈ RealVectorSpace)


Proof



Definitions occuring in Statement :  mk-real-vector-space: mk-real-vector-space,  real-vector-space: RealVectorSpace,  rneq: x ≠ y,  rmul: a * b,  radd: a + b,  int-to-real: r(n),  real: ℝ,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  or: 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,  separation-space: Error :separation-space,  record+: record+,  record-select: r.x,  subtype_rel: A ⊆r B,  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  btrue: tt,  so_lambda: λ2x.t[x],  so_apply: x[s],  prop: ℙ,  all: ∀x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  mk-real-vector-space: mk-real-vector-space,  real-vector-space: RealVectorSpace,  ss-sep: Error :ss-sep,  ss-point: Error :ss-point,  record-update: r[x := v],  record: record(x.T[x]),  bool: 𝔹,  unit: Unit,  it: ⋅,  uiff: uiff(P;Q),  and: P ∧ Q,  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  top: Top,  bfalse: ff,  iff: P ⇐⇒ Q,  not: ¬A,  rev_implies: P ⇐ Q,  false: False,  ss-eq: Error :ss-eq
Lemmas referenced :  subtype_rel_self,  record-select_wf,  top_wf,  istype-atom,  not_wf,  all_wf,  or_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,  iff_weakening_uiff,  eqff_to_assert,  assert_of_bnot,  istype-assert,  real_wf,  Error :ss-sep_wf,  rneq_wf,  Error :ss-eq_wf,  int-to-real_wf,  rmul_wf,  radd_wf,  Error :ss-point_wf,  Error :separation-space_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  introduction,  cut,  hypothesisEquality,  sqequalHypSubstitution,  dependentIntersectionElimination,  sqequalRule,  dependentIntersectionEqElimination,  thin,  hypothesis,  applyEquality,  tokenEquality,  instantiate,  extract_by_obid,  isectElimination,  universeEquality,  setEquality,  functionEquality,  cumulativity,  lambdaEquality_alt,  equalityTransitivity,  equalitySymmetry,  because_Cache,  applyLambdaEquality,  setElimination,  rename,  inhabitedIsType,  universeIsType,  dependentIntersection_memberEquality,  functionExtensionality_alt,  lambdaFormation_alt,  unionElimination,  equalityElimination,  baseApply,  closedConclusion,  baseClosed,  atomEquality,  independent_functionElimination,  productElimination,  independent_isectElimination,  dependent_functionElimination,  isect_memberEquality_alt,  voidElimination,  independent_pairFormation,  equalityIstype,  sqequalBase,  functionIsType,  functionExtensionality,  axiomEquality,  unionIsType,  isectIsTypeImplies,  setIsType,  productIsType,  natural_numberEquality
Latex:
\mforall{}[self:SeparationSpace].  \mforall{}[z:Point(self)].  \mforall{}[p:\{f:Point(self)  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  Point(self)| 
                                                                                                (\mforall{}x,y,z:Point(self).    f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                                                                                                \mwedge{}  (\mforall{}x,y:Point(self).    f  x  y  \mequiv{}  f  y  x)\}  ].
\mforall{}[m:\{m:\mBbbR{}  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  Point(self)| 
          (\mforall{}a:\mBbbR{}.  \mforall{}x,y:Point(self).    m  a  (p  x  y)  \mequiv{}  p  (m  a  x)  (m  a  y))
          \mwedge{}  (\mforall{}x:Point(self)
                    (m  r1  x  \mequiv{}  x
                    \mwedge{}  m  r0  x  \mequiv{}  z
                    \mwedge{}  (\mforall{}a,b:\mBbbR{}.    m  a  (m  b  x)  \mequiv{}  m  (a  *  b)  x)
                    \mwedge{}  (\mforall{}a,b:\mBbbR{}.    m  (a  +  b)  x  \mequiv{}  p  (m  a  x)  (m  b  x))))\}  ].  \mforall{}[psep:\mforall{}x,x',y,y':Point(self).
                                                                                                                                          (p  x  y  \#  p  x'  y'
                                                                                                                                          {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))].
\mforall{}[msep:\mforall{}a,b:\mBbbR{}.  \mforall{}x,y:Point(self).    (m  a  x  \#  m  b  y  {}\mRightarrow{}  (a  \mneq{}  b  \mvee{}  x  \#  y))].
    (ss=self;
      0=z;
      +=p;
      *=m;
      +sep=psep;
      *sep=msep  \mmember{}  RealVectorSpace)


Date html generated: 2020_05_20-PM-01_10_37
Last ObjectModification: 2019_12_10-AM-00_37_32

Theory : inner!product!spaces


Home Index