Nuprl Lemma : rv-mul-sep-iff
∀rv:InnerProductSpace. ∀a,b:ℝ. ∀y:Point. (a*y # b*y ⇐⇒ a ≠ b ∧ y # 0)
Proof
Definitions occuring in Statement :
inner-product-space: InnerProductSpace,
rv-mul: a*x,
rv-0: 0,
rneq: x ≠ y,
real: ℝ,
ss-sep: x # y,
ss-point: Point,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
subtype_rel: A ⊆r B,
prop: ℙ,
uall: ∀[x:A]. B[x],
guard: {T},
uimplies: b supposing a,
rev_implies: P ⇐ Q,
cand: A c∧ B
Lemmas referenced :
rv-mul-sep1,
inner-product-space_subtype,
ss-sep_wf,
real-vector-space_subtype1,
subtype_rel_transitivity,
inner-product-space_wf,
real-vector-space_wf,
separation-space_wf,
rv-mul_wf,
rneq_wf,
rv-0_wf,
ss-point_wf,
real_wf,
rv-sep-iff,
rv-sub_wf,
rsub_wf,
ss-sep_functionality,
ss-eq_inversion,
rv-mul-sub,
ss-eq_weakening,
rv-mul-sep-zero,
rneq-iff-rabs
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
independent_pairFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
applyEquality,
hypothesis,
sqequalRule,
independent_functionElimination,
because_Cache,
isectElimination,
instantiate,
independent_isectElimination,
productElimination,
productEquality
Latex:
\mforall{}rv:InnerProductSpace. \mforall{}a,b:\mBbbR{}. \mforall{}y:Point. (a*y \# b*y \mLeftarrow{}{}\mRightarrow{} a \mneq{} b \mwedge{} y \# 0)
Date html generated:
2017_10_04-PM-11_51_55
Last ObjectModification:
2017_06_26-PM-09_11_10
Theory : inner!product!spaces
Home
Index