Nuprl Lemma : det-row-op
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a,b:ℕn]. ∀[k:|r|]. |row-op(r;a;b;k;M)| = |M| ∈ |r| supposing ¬(a = b ∈ ℤ)
Proof
Definitions occuring in Statement :
row-op: row-op(r;a;b;k;M),
matrix-det: |M|,
matrix: Matrix(n;m;r),
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T,
crng: CRng,
rng_car: |r|
Definitions unfolded in proof :
crng: CRng,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
crng_wf,
nat_wf,
matrix-det-is-det-fun,
det-fun-row-op
Rules used in proof :
sqequalRule,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
hypothesis,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}[r:CRng]. \mforall{}[n:\mBbbN{}]. \mforall{}[M:Matrix(n;n;r)]. \mforall{}[a,b:\mBbbN{}n]. \mforall{}[k:|r|].
|row-op(r;a;b;k;M)| = |M| supposing \mneg{}(a = b)
Date html generated:
2018_05_21-PM-09_37_05
Last ObjectModification:
2018_01_02-PM-00_55_46
Theory : matrices
Home
Index