Nuprl Lemma : rv-mul-add-alt

[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x,u:Point].  a*x b*x ≡ b*x


Proof




Definitions occuring in Statement :  rv-mul: a*x rv-add: y real-vector-space: RealVectorSpace radd: b real: ss-eq: x ≡ y ss-point: Point uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ss-eq: x ≡ y not: ¬A implies:  Q false: False subtype_rel: A ⊆B prop: all: x:A. B[x] uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  ss-sep_wf real-vector-space_subtype1 rv-add_wf rv-mul_wf radd_wf ss-point_wf real_wf real-vector-space_wf ss-eq_weakening rv-mul-add ss-eq_functionality ss-eq_inversion rv-add-assoc rv-add_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality because_Cache extract_by_obid isectElimination applyEquality hypothesis isect_memberEquality voidElimination independent_functionElimination independent_isectElimination productElimination

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[x,u:Point].    u  +  a*x  +  b*x  \mequiv{}  u  +  a  +  b*x



Date html generated: 2017_10_04-PM-11_50_25
Last ObjectModification: 2017_06_22-PM-06_44_30

Theory : inner!product!spaces


Home Index