Nuprl Lemma : matrix-mul-col_wf

[n,m:ℤ]. ∀[r:RngSig]. ∀[k:|r|]. ∀[i:ℕm]. ∀[M:Matrix(n;m;r)].  (matrix-mul-col(r;k;i;M) ∈ Matrix(n;m;r))


Proof




Definitions occuring in Statement :  matrix-mul-col: matrix-mul-col(r;k;i;M) matrix: Matrix(n;m;r) int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T natural_number: $n int: rng_car: |r| rng_sig: RngSig
Definitions unfolded in proof :  so_apply: x[s1;s2] not: ¬A implies:  Q false: False infix_ap: y int_seg: {i..j-} so_lambda: λ2y.t[x; y] matrix-mul-col: matrix-mul-col(r;k;i;M) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_sig_wf rng_car_wf matrix_wf int_seg_wf matrix-ap_wf rng_times_wf mx_wf
Rules used in proof :  intEquality because_Cache isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality natural_numberEquality applyEquality hypothesis rename setElimination int_eqEquality lambdaEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[r:RngSig].  \mforall{}[k:|r|].  \mforall{}[i:\mBbbN{}m].  \mforall{}[M:Matrix(n;m;r)].
    (matrix-mul-col(r;k;i;M)  \mmember{}  Matrix(n;m;r))



Date html generated: 2018_05_21-PM-09_34_24
Last ObjectModification: 2017_12_11-PM-04_20_51

Theory : matrices


Home Index