Nuprl Lemma : null-space-unique
∀[r:IntegDom{i}]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].
∀[u:Column(n;r)]. (((M*u) = 0 ∈ Column(n;r)) ⇒ (u = 0 ∈ Column(n;r))) supposing ¬(|M| = 0 ∈ |r|)
Proof
Definitions occuring in Statement :
matrix-det: |M|,
zero-matrix: 0,
matrix-times: (M*N),
matrix: Matrix(n;m;r),
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q,
natural_number: $n,
equal: s = t ∈ T,
integ_dom: IntegDom{i},
rng_zero: 0,
rng_car: |r|
Definitions unfolded in proof :
true: True,
not: ¬A,
false: False,
less_than': less_than'(a;b),
and: P ∧ Q,
le: A ≤ B,
prop: ℙ,
rng: Rng,
crng: CRng,
nat: ℕ,
implies: P ⇒ Q,
uimplies: b supposing a,
integ_dom: IntegDom{i},
member: t ∈ T,
uall: ∀[x:A]. B[x],
squash: ↓T,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
top: Top,
all: ∀x:A. B[x],
zero-matrix: 0,
matrix-ap: M[i,j],
matrix: Matrix(n;m;r),
matrix-scalar-mul: k*M,
integ_dom_p: IsIntegDom(r),
rev_implies: P ⇐ Q
Lemmas referenced :
le_wf,
false_wf,
integ_dom_wf,
nat_wf,
rng_zero_wf,
matrix-det_wf,
rng_car_wf,
not_wf,
zero-matrix_wf,
matrix_wf,
equal_wf,
identity-matrix_wf,
adjugate_wf,
matrix-times_wf,
adjugate-property2,
matrix-times-0-right,
squash_wf,
true_wf,
matrix-times-assoc,
rng_wf,
matrix-scalar-mul-times,
matrix-scalar-mul_wf,
rng_sig_wf,
matrix-times-id-left,
iff_weakening_equal,
int_seg_wf,
matrix_ap_mx_lemma,
matrix-ap_wf,
crng_times_comm
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
independent_pairFormation,
dependent_set_memberEquality,
isect_memberEquality,
axiomEquality,
dependent_functionElimination,
lambdaEquality,
sqequalRule,
natural_numberEquality,
because_Cache,
applyLambdaEquality,
lambdaFormation,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
hypothesis,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
extract_by_obid,
introduction,
cut,
applyEquality,
imageElimination,
universeEquality,
intEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
productElimination,
independent_functionElimination,
voidEquality,
voidElimination,
functionExtensionality,
hyp_replacement
Latex:
\mforall{}[r:IntegDom\{i\}]. \mforall{}[n:\mBbbN{}]. \mforall{}[M:Matrix(n;n;r)].
\mforall{}[u:Column(n;r)]. (((M*u) = 0) {}\mRightarrow{} (u = 0)) supposing \mneg{}(|M| = 0)
Date html generated:
2018_05_21-PM-09_39_19
Last ObjectModification:
2017_12_20-PM-06_11_20
Theory : matrices
Home
Index