Nuprl Lemma : matrix-times-distrib-left

[n,k,m:ℕ]. ∀[r:Rng]. ∀[M:Matrix(n;k;r)]. ∀[N,K:Matrix(k;m;r)].  ((M*N K) (M*N) (M*K) ∈ Matrix(n;m;r))


Proof




Definitions occuring in Statement :  matrix-times: (M*N) matrix-plus: N matrix: Matrix(n;m;r) nat: uall: [x:A]. B[x] equal: t ∈ T rng: Rng
Definitions unfolded in proof :  rev_implies:  Q iff: ⇐⇒ Q subtype_rel: A ⊆B true: True infix_ap: y 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 ≥  and: P ∧ Q lelt: i ≤ j < k int_seg: {i..j-} guard: {T} uimplies: supposing a so_apply: x[s] so_lambda: λ2x.t[x] nat: rng: Rng prop: squash: T mx: matrix(M[x; y]) matrix-ap: M[i,j] matrix-plus: N matrix-times: (M*N) matrix: Matrix(n;m;r) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  nat_wf rng_wf matrix_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 int_seg_properties rng_sum_plus int_seg_wf rng_plus_wf matrix-ap_wf rng_times_wf infix_ap_wf rng_sum_wf rng_car_wf true_wf squash_wf equal_wf rng_times_over_plus rng_plus_comm
Rules used in proof :  axiomEquality baseClosed imageMemberEquality independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_functionElimination approximateComputation unionElimination dependent_functionElimination productElimination independent_isectElimination because_Cache natural_numberEquality setElimination universeEquality equalitySymmetry hypothesis equalityTransitivity hypothesisEquality isectElimination extract_by_obid imageElimination sqequalHypSubstitution lambdaEquality thin applyEquality sqequalRule rename functionExtensionality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n,k,m:\mBbbN{}].  \mforall{}[r:Rng].  \mforall{}[M:Matrix(n;k;r)].  \mforall{}[N,K:Matrix(k;m;r)].    ((M*N  +  K)  =  (M*N)  +  (M*K))



Date html generated: 2018_05_21-PM-09_34_42
Last ObjectModification: 2017_12_11-PM-00_29_30

Theory : matrices


Home Index