Nuprl Lemma : scalar-triple-product-as-det
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (|a,b,c| = |λi.[a; b; c][i]| ∈ |r|)
Proof
Definitions occuring in Statement :
scalar-triple-product: |a,b,c|,
matrix-det: |M|,
select: L[n],
cons: [a / b],
nil: [],
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
lambda: λx.A[x],
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
crng: CRng,
rng_car: |r|
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
matrix: Matrix(n;m;r),
crng: CRng,
rng: Rng,
int_seg: {i..j-},
uimplies: b supposing a,
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
top: Top,
prop: ℙ,
nat: ℕ,
less_than': less_than'(a;b),
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
scalar-triple-product: |a,b,c|,
cross-product: (a x b),
scalar-product: (a . b),
determinant: determinant(n;r),
lt_int: i <z j,
subtract: n - m,
ifthenelse: if b then t else f fi ,
bfalse: ff,
rng_sum: rng_sum,
mon_itop: Π lb ≤ i < ub. E[i],
add_grp_of_rng: r↓+gp,
grp_op: *,
pi2: snd(t),
pi1: fst(t),
grp_id: e,
itop: Π(op,id) lb ≤ i < ub. E[i],
ycomb: Y,
btrue: tt,
select: L[n],
cons: [a / b],
matrix-minor: matrix-minor(i;j;m),
matrix-ap: M[i,j],
isEven: isEven(n),
modulus: a mod n,
remainder: n rem m,
absval: |i|,
eq_int: (i =z j),
infix_ap: x f y,
uiff: uiff(P;Q),
ringeq_int_terms: t1 ≡ t2
Lemmas referenced :
select_wf,
int_seg_wf,
rng_car_wf,
cons_wf,
nil_wf,
int_seg_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
istype-int,
int_formula_prop_and_lemma,
istype-void,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
length_of_cons_lemma,
length_of_nil_lemma,
decidable__lt,
intformless_wf,
itermAdd_wf,
int_formula_prop_less_lemma,
int_term_value_add_lemma,
equal_wf,
squash_wf,
true_wf,
istype-universe,
scalar-triple-product_wf,
matrix-det-is-determinant,
istype-le,
subtype_rel_self,
iff_weakening_equal,
primrec-unroll,
primrec1_lemma,
rng_times_over_minus,
rng_plus_zero,
rng_times_one,
crng_wf,
rng_plus_wf,
rng_times_wf,
istype-less_than,
rng_minus_wf,
rng_zero_wf,
rng_one_wf,
itermMultiply_wf,
itermMinus_wf,
ringeq-iff-rsub-is-0,
ring_polynomial_null,
int-to-ring_wf,
ring_term_value_add_lemma,
ring_term_value_mul_lemma,
ring_term_value_var_lemma,
ring_term_value_minus_lemma,
ring_term_value_const_lemma,
int-to-ring-zero
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
lambdaEquality_alt,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
functionEquality,
closedConclusion,
natural_numberEquality,
hypothesis,
setElimination,
rename,
because_Cache,
hypothesisEquality,
independent_isectElimination,
productElimination,
imageElimination,
dependent_functionElimination,
unionElimination,
approximateComputation,
independent_functionElimination,
dependent_pairFormation_alt,
int_eqEquality,
isect_memberEquality_alt,
voidElimination,
sqequalRule,
independent_pairFormation,
universeIsType,
addEquality,
applyEquality,
equalityTransitivity,
equalitySymmetry,
inhabitedIsType,
instantiate,
universeEquality,
dependent_set_memberEquality_alt,
lambdaFormation_alt,
imageMemberEquality,
baseClosed,
callbyvalueReduce,
sqleReflexivity,
axiomEquality,
isectIsTypeImplies,
functionIsType,
productIsType
Latex:
\mforall{}[r:CRng]. \mforall{}[a,b,c:\mBbbN{}3 {}\mrightarrow{} |r|]. (|a,b,c| = |\mlambda{}i.[a; b; c][i]|)
Date html generated:
2020_05_20-AM-09_04_05
Last ObjectModification:
2019_11_27-PM-02_54_26
Theory : matrices
Home
Index