Nuprl Lemma : cross-product-distrib1

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


Proof




Definitions occuring in Statement :  cross-product: (a b) vector-add: (a b) int_seg: {i..j-} uall: [x:A]. B[x] function: x:A ⟶ B[x] natural_number: $n equal: t ∈ T crng: CRng 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-add: (a b) 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_times_wf infix_ap_wf rng_minus_wf lelt_wf rng_plus_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_minus_over_plus rng_plus_assoc rng_plus_comm rng_plus_ac_1 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,c:\mBbbN{}3  {}\mrightarrow{}  |r|].    ((a  x  (b  +  c))  =  ((a  x  b)  +  (a  x  c)))



Date html generated: 2018_05_21-PM-09_41_12
Last ObjectModification: 2017_12_18-PM-00_33_50

Theory : matrices


Home Index