Nuprl Lemma : ip-inner-Pasch1

∀rv:InnerProductSpace. ∀a,b,c,p,q:Point.
  (a # p
  ⇒ b # c
  ⇒ a_p_c
  ⇒ b_q_c
  ⇒ (∃x:Point
       (a_x_q
       ∧ b_x_p
       ∧ (a # q ⇒ x # a)
       ∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
       ∧ ((b # p ∧ b # q) ⇒ x # b)
       ∧ ((b # p ∧ q # c) ⇒ x # p))))


Proof



Definitions occuring in Statement :  ip-between: a_b_c,  inner-product-space: InnerProductSpace,  ss-sep: x # y,  ss-point: Point,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  member: t ∈ T,  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  iff: P ⇐⇒ Q,  and: P ∧ Q,  exists: ∃x:A. B[x],  top: Top,  prop: ℙ,  subtype_rel: A ⊆r B,  guard: {T},  or: P ∨ Q,  false: False,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  rsub: x - y,  rev_implies: P ⇐ Q,  cand: A c∧ B,  rge: x ≥ y,  rneq: x ≠ y,  squash: ↓T,  true: True,  rleq: x ≤ y,  rnonneg: rnonneg(x),  le: A ≤ B,  not: ¬A,  real: ℝ,  i-member: r ∈ I,  rccint: [l, u],  rcoint: [l, u)
Lemmas referenced :  ip-between-sep,  ip-between-iff2,  member_rccint_lemma,  ip-between_wf,  ss-sep_wf,  real-vector-space_subtype1,  inner-product-space_subtype,  subtype_rel_transitivity,  inner-product-space_wf,  real-vector-space_wf,  separation-space_wf,  ss-point_wf,  ip-dist-between-1,  rv-norm_wf,  rv-sub_wf,  rv-add_wf,  rv-mul_wf,  rsub_wf,  int-to-real_wf,  req_wf,  rv-ip_wf,  rmul_wf,  rabs_wf,  rv-norm-positive,  rv-sep-iff,  real_wf,  rleq_wf,  rmul-is-positive,  zero-rleq-rabs,  rless_transitivity1,  rless_irreflexivity,  radd-preserves-rleq,  radd_wf,  rminus_wf,  radd-preserves-rless,  req_functionality,  rv-norm_functionality,  rv-sub_functionality,  ss-eq_weakening,  ss-eq_inversion,  req_weakening,  rless_functionality,  rabs-of-nonneg,  uiff_transitivity,  rleq_functionality,  radd_comm,  radd-ac,  radd_functionality,  radd-rminus-both,  radd-zero-both,  rless_wf,  rmul_comm,  rless_functionality_wrt_implies,  rmul_functionality_wrt_rleq2,  rleq_weakening_equal,  rmul-one-both,  rmul_preserves_rleq,  rdiv_wf,  member_rcoint_lemma,  rmul_preserves_rless,  equal_wf,  squash_wf,  true_wf,  iff_weakening_equal,  rmul_preserves_rleq2,  less_than'_wf,  nat_plus_wf,  rmul-rdiv-cancel2,  req_transitivity,  rmul-distrib,  rmul_over_rminus,  rminus_functionality,  rmul-zero-both,  rminus-zero,  rmul_preserves_req,  rmul_functionality,  req_inversion,  rmul-assoc,  rminus-radd,  radd-assoc,  rminus-as-rmul,  rminus-rminus,  radd-rminus-assoc,  rmul-ac,  radd-preserves-req,  i-member_wf,  rcoint_wf,  rccint_wf,  ss-eq_wf,  ss-eq_functionality,  rv-add_functionality,  rv-mul_functionality,  ss-eq_transitivity,  rv-mul-linear,  rv-mul-mul,  rv-add-assoc,  rv-add-comm,  rleq_weakening_rless,  rv-mul-add,  rv-mul1,  ip-between_functionality,  rv-sep-iff-norm,  ip-dist-between-2,  rless_transitivity2,  ss-sep-symmetry,  ss-sep_functionality
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  dependent_functionElimination,  thin,  hypothesisEquality,  isectElimination,  independent_isectElimination,  hypothesis,  because_Cache,  productElimination,  independent_functionElimination,  rename,  isect_memberEquality,  voidElimination,  voidEquality,  applyEquality,  instantiate,  sqequalRule,  natural_numberEquality,  lambdaEquality,  setElimination,  setEquality,  productEquality,  unionElimination,  promote_hyp,  inlFormation,  independent_pairFormation,  addLevel,  levelHypothesis,  equalityTransitivity,  equalitySymmetry,  inrFormation,  imageElimination,  imageMemberEquality,  baseClosed,  universeEquality,  isect_memberFormation,  independent_pairEquality,  minusEquality,  axiomEquality,  dependent_pairFormation,  functionEquality
Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c,p,q:Point.
    (a  \#  p
    {}\mRightarrow{}  b  \#  c
    {}\mRightarrow{}  a\_p\_c
    {}\mRightarrow{}  b\_q\_c
    {}\mRightarrow{}  (\mexists{}x:Point
              (a\_x\_q
              \mwedge{}  b\_x\_p
              \mwedge{}  (a  \#  q  {}\mRightarrow{}  x  \#  a)
              \mwedge{}  ((a  \#  q  \mwedge{}  p  \#  c  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  q)
              \mwedge{}  ((b  \#  p  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  b)
              \mwedge{}  ((b  \#  p  \mwedge{}  q  \#  c)  {}\mRightarrow{}  x  \#  p))))


Date html generated: 2017_10_05-AM-00_05_04
Last ObjectModification: 2017_03_13-AM-00_16_06

Theory : inner!product!spaces


Home Index