Nuprl Lemma : vs-mul-linear

[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[a:|K|]. ∀[x,y:Point(vs)].  (a y ∈ Point(vs))


Proof




Definitions occuring in Statement :  vs-mul: x vs-add: y vector-space: VectorSpace(K) vs-point: Point(vs) uall: [x:A]. B[x] equal: t ∈ T rng_car: |r| rng_sig: RngSig
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] squash: T vs-add: y vs-mul: x infix_ap: y guard: {T} prop: so_apply: x[s] so_lambda: λ2x.t[x] and: P ∧ Q btrue: tt ifthenelse: if then else fi  eq_atom: =a y subtype_rel: A ⊆B record-select: r.x record+: record+ vector-space: VectorSpace(K)
Lemmas referenced :  rng_sig_wf vector-space_wf rng_car_wf vs-point_wf rng_plus_wf rng_times_wf infix_ap_wf rng_zero_wf rng_one_wf equal_wf all_wf subtype_rel_self
Rules used in proof :  dependent_functionElimination because_Cache axiomEquality isect_memberEquality sqequalRule thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis hypothesisEquality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination imageElimination baseClosed imageMemberEquality applyLambdaEquality rename setElimination equalitySymmetry equalityTransitivity functionExtensionality lambdaEquality productEquality functionEquality setEquality universeEquality instantiate tokenEquality applyEquality dependentIntersectionEqElimination dependentIntersectionElimination

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[a:|K|].  \mforall{}[x,y:Point(vs)].    (a  *  x  +  y  =  a  *  x  +  a  *  y)



Date html generated: 2018_05_22-PM-09_40_41
Last ObjectModification: 2018_01_09-AM-10_27_24

Theory : linear!algebra


Home Index