Nuprl Lemma : vs-0_wf

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


Proof




Definitions occuring in Statement :  vs-0: 0 vector-space: VectorSpace(K) vs-point: Point(vs) uall: [x:A]. B[x] member: t ∈ T rng_sig: RngSig
Definitions unfolded in proof :  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) vs-point: Point(vs) vs-0: 0 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 :  isect_memberEquality dependent_functionElimination axiomEquality rename setElimination equalitySymmetry equalityTransitivity functionExtensionality lambdaEquality productEquality because_Cache functionEquality setEquality universeEquality isectElimination extract_by_obid instantiate tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination dependentIntersectionElimination sqequalHypSubstitution hypothesisEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].    (0  \mmember{}  Point(vs))



Date html generated: 2018_05_22-PM-09_40_18
Last ObjectModification: 2018_01_09-AM-10_15_32

Theory : linear!algebra


Home Index