Nuprl Lemma : scalar-product-add-left

[r:Rng]. ∀[n:ℕ]. ∀[a,b,c:ℕn ⟶ |r|].  (((a b) c) ((a c) +r (b c)) ∈ |r|)


Proof




Definitions occuring in Statement :  scalar-product: (a b) vector-add: (a b) int_seg: {i..j-} nat: uall: [x:A]. B[x] infix_ap: y function: x:A ⟶ B[x] natural_number: $n equal: t ∈ T rng: Rng rng_plus: +r rng_car: |r|
Definitions unfolded in proof :  rev_implies:  Q iff: ⇐⇒ Q guard: {T} subtype_rel: A ⊆B true: True infix_ap: y and: P ∧ Q top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) implies:  Q not: ¬A or: P ∨ Q decidable: Dec(P) all: x:A. B[x] ge: i ≥  uimplies: supposing a so_apply: x[s] so_lambda: λ2x.t[x] nat: rng: Rng prop: squash: T vector-add: (a b) scalar-product: (a b) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_wf nat_wf iff_weakening_equal int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties rng_sum_plus int_seg_wf rng_plus_wf rng_times_wf infix_ap_wf rng_sum_wf rng_car_wf true_wf squash_wf equal_wf rng_times_over_plus
Rules used in proof :  axiomEquality functionEquality productElimination baseClosed imageMemberEquality independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_functionElimination approximateComputation unionElimination dependent_functionElimination independent_isectElimination functionExtensionality because_Cache natural_numberEquality rename setElimination universeEquality equalitySymmetry hypothesis equalityTransitivity hypothesisEquality isectElimination extract_by_obid imageElimination sqequalHypSubstitution lambdaEquality thin applyEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbN{}].  \mforall{}[a,b,c:\mBbbN{}n  {}\mrightarrow{}  |r|].    (((a  +  b)  .  c)  =  ((a  .  c)  +r  (b  .  c)))



Date html generated: 2018_05_21-PM-09_42_08
Last ObjectModification: 2017_12_22-PM-01_26_31

Theory : matrices


Home Index