Nuprl Lemma : nonzero-cross-imp_wf

∀[r:IntegDom{i}]. ∀[eq:∀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|)))} ].
  (nonzero-cross-imp(r;eq;a;b) ∈ {l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} | ((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|))\000C} )


Proof



Definitions occuring in Statement :  nonzero-cross-imp: nonzero-cross-imp(r;eq;a;b),  scalar-product: (a . b),  cross-product: (a x b),  zero-vector: 0,  int_seg: {i..j-},  decidable: Dec(P),  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  not: ¬A,  and: P ∧ Q,  member: t ∈ T,  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 :  so_apply: x[s],  and: P ∧ Q,  so_lambda: λ2x.t[x],  rng: Rng,  crng: CRng,  integ_dom: IntegDom{i},  prop: ℙ,  sq_exists: ∃x:A [B[x]],  member: t ∈ T,  uall: ∀[x:A]. B[x],  not: ¬A,  false: False,  less_than': less_than'(a;b),  le: A ≤ B,  nat: ℕ,  implies: P ⇒ Q,  all: ∀x:A. B[x],  subtype_rel: A ⊆r B,  cross-product-non-zero-implies-ext
Lemmas referenced :  integ_dom_wf,  decidable_wf,  all_wf,  cross-product_wf,  zero-vector_wf,  equal_wf,  not_wf,  rng_car_wf,  int_seg_wf,  set_wf,  rng_zero_wf,  le_wf,  false_wf,  scalar-product_wf,  sq_exists_wf,  cross-product-non-zero-implies-ext
Rules used in proof :  isect_memberEquality,  hypothesisEquality,  applyEquality,  functionExtensionality,  productEquality,  lambdaEquality,  because_Cache,  rename,  setElimination,  natural_numberEquality,  functionEquality,  thin,  isectElimination,  extract_by_obid,  equalitySymmetry,  equalityTransitivity,  axiomEquality,  sqequalRule,  hypothesis,  sqequalHypSubstitution,  cut,  introduction,  isect_memberFormation,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution,  independent_pairFormation,  dependent_set_memberEquality,  productElimination,  dependent_functionElimination,  lambdaFormation,  setEquality,  universeEquality,  cumulativity,  instantiate
Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[eq:\mforall{}x,y:|r|.    Dec(x  =  y)].  \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))\}  ].
    (nonzero-cross-imp(r;eq;a;b)  \mmember{}  \{l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  |  ((a  .  l)  =  0)  \mwedge{}  (\mneg{}((b  .  l)  =  0))\}  )


Date html generated: 2018_05_21-PM-09_44_03
Last ObjectModification: 2017_12_22-PM-02_59_21

Theory : matrices


Home Index