Nuprl Lemma : cross-product-non-zero-implies-ext
∀r:IntegDom{i}
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ (∀a:{a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} . ∀b:{b:ℕ3 ⟶ |r||
(¬(b = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))} .
(∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} [(((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|)))])))
Proof
Definitions occuring in Statement :
scalar-product: (a . b),
cross-product: (a x b),
zero-vector: 0,
int_seg: {i..j-},
decidable: Dec(P),
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
integ_dom: IntegDom{i},
rng_zero: 0,
rng_car: |r|
Definitions unfolded in proof :
member: t ∈ T,
bfalse: ff,
it: ⋅,
mk_deq: mk_deq(p),
isl: isl(x),
btrue: tt,
vector-mul: (c*a),
infix_ap: x f y,
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
nonzero-cross-imp: nonzero-cross-imp(r;eq;a;b),
cross-product-non-zero-implies,
sq_stable__and,
sq_stable__not,
decidable__exists_int_seg,
decidable__cand,
decidable__not,
decidable__equal_compact_domain,
compact-finite,
any: any x,
decidable__and2,
decidable__implies,
decidable__false,
deq-exists,
decidable__equal_bool,
decidable__and,
btrue_neq_bfalse,
uall: ∀[x:A]. B[x],
so_lambda: so_lambda4,
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x.t[x],
top: Top,
so_apply: x[s],
uimplies: b supposing a,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
has-value: (a)↓
Lemmas referenced :
cross-product-non-zero-implies,
lifting-strict-decide,
istype-void,
strict4-decide,
lifting-strict-int_eq,
strict4-spread,
has-value_wf_base,
is-exception_wf,
sq_stable__and,
sq_stable__not,
decidable__exists_int_seg,
decidable__cand,
decidable__not,
decidable__equal_compact_domain,
compact-finite,
decidable__and2,
decidable__implies,
decidable__false,
deq-exists,
decidable__equal_bool,
decidable__and,
btrue_neq_bfalse
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
isectElimination,
baseClosed,
isect_memberEquality_alt,
voidElimination,
independent_isectElimination,
inhabitedIsType,
lambdaFormation_alt,
sqequalSqle,
divergentSqle,
callbyvalueSpread,
productElimination,
sqleReflexivity,
equalityIstype,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
spreadExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion
Latex:
\mforall{}r:IntegDom\{i\}
((\mforall{}x,y:|r|. Dec(x = y))
{}\mRightarrow{} (\mforall{}a:\{a:\mBbbN{}3 {}\mrightarrow{} |r|| \mneg{}(a = 0)\} . \mforall{}b:\{b:\mBbbN{}3 {}\mrightarrow{} |r|| (\mneg{}(b = 0)) \mwedge{} (\mneg{}((a x b) = 0))\} .
(\mexists{}l:\{p:\mBbbN{}3 {}\mrightarrow{} |r|| \mneg{}(p = 0)\} [(((a . l) = 0) \mwedge{} (\mneg{}((b . l) = 0)))])))
Date html generated:
2020_05_20-AM-09_03_58
Last ObjectModification:
2020_01_10-PM-02_17_37
Theory : matrices
Home
Index