Nuprl Lemma : vs-mul-one

[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (1 x ∈ Point(vs))


Proof




Definitions occuring in Statement :  vs-mul: x vector-space: VectorSpace(K) vs-point: Point(vs) uall: [x:A]. B[x] equal: t ∈ T rng_one: 1 rng_sig: RngSig
Definitions unfolded in proof :  squash: T vs-mul: x infix_ap: y guard: {T} prop: all: x:A. B[x] 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) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_sig_wf vector-space_wf rng_plus_wf rng_times_wf infix_ap_wf rng_zero_wf rng_one_wf rng_car_wf equal_wf all_wf vs-point_wf subtype_rel_self
Rules used in proof :  dependent_functionElimination axiomEquality isect_memberEquality productElimination imageElimination baseClosed imageMemberEquality applyLambdaEquality rename setElimination equalitySymmetry equalityTransitivity functionExtensionality lambdaEquality productEquality because_Cache functionEquality setEquality universeEquality isectElimination extract_by_obid instantiate tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination sqequalRule dependentIntersectionElimination sqequalHypSubstitution hypothesisEquality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[x:Point(vs)].    (1  *  x  =  x)



Date html generated: 2018_05_22-PM-09_40_48
Last ObjectModification: 2018_01_09-PM-01_05_02

Theory : linear!algebra


Home Index