Nuprl Lemma : rv-mul-add-1

[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x:Point].  a*x x ≡ r1*x


Proof




Definitions occuring in Statement :  rv-mul: a*x rv-add: y real-vector-space: RealVectorSpace radd: b int-to-real: r(n) real: ss-eq: x ≡ y ss-point: Point uall: [x:A]. B[x] natural_number: $n
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 int-to-real_wf ss-point_wf real_wf real-vector-space_wf ss-eq_weakening ss-eq_functionality ss-eq_transitivity ss-eq_inversion rv-mul-add rv-add_functionality rv-mul1
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 natural_numberEquality isect_memberEquality voidElimination independent_functionElimination independent_isectElimination productElimination

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



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

Theory : inner!product!spaces


Home Index