Nuprl Lemma : cross-product-anti-comm

[r:CRng]. ∀[a,b:ℕ3 ⟶ |r|].  ((b a) (-r 1*(a b)) ∈ (ℕ3 ⟶ |r|))


Proof




Definitions occuring in Statement :  cross-product: (a b) vector-mul: (c*a) int_seg: {i..j-} uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] natural_number: $n equal: t ∈ T crng: CRng rng_one: 1 rng_minus: -r rng_car: |r|
Definitions unfolded in proof :  true: True squash: T less_than: a < b rng: Rng crng: CRng top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) lelt: i ≤ j < k subtract: m prop: not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B and: P ∧ Q cons: [a b] select: L[n] vector-mul: (c*a) cross-product: (a b) guard: {T} implies:  Q sq_type: SQType(T) uimplies: supposing a or: P ∨ Q decidable: Dec(P) int_seg: {i..j-} all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] infix_ap: y subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  rng_one_wf rng_minus_wf lelt_wf rng_times_wf rng_plus_wf infix_ap_wf crng_wf rng_car_wf int_seg_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf full-omega-unsat int_seg_cases false_wf int_seg_subtype int_seg_properties int_subtype_base subtype_base_sq decidable__equal_int equal_wf squash_wf true_wf rng_times_over_plus rng_times_over_minus rng_times_one crng_times_comm rng_minus_minus rng_plus_comm iff_weakening_equal
Rules used in proof :  baseClosed imageMemberEquality dependent_set_memberEquality applyEquality axiomEquality functionEquality voidEquality voidElimination isect_memberEquality int_eqEquality lambdaEquality dependent_pairFormation approximateComputation productElimination lambdaFormation independent_pairFormation addEquality hypothesis_subsumption sqequalRule equalitySymmetry equalityTransitivity independent_functionElimination because_Cache independent_isectElimination intEquality cumulativity isectElimination instantiate unionElimination natural_numberEquality hypothesis hypothesisEquality rename setElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid functionExtensionality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution imageElimination universeEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[a,b:\mBbbN{}3  {}\mrightarrow{}  |r|].    ((b  x  a)  =  (-r  1*(a  x  b)))



Date html generated: 2018_05_21-PM-09_41_04
Last ObjectModification: 2017_12_18-PM-01_25_21

Theory : matrices


Home Index