Nuprl Lemma : matrix-plus-minus-right

[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)].  (N -(N) 0 ∈ Matrix(k;m;r))


Proof




Definitions occuring in Statement :  matrix-minus: -(M) zero-matrix: 0 matrix-plus: N matrix: Matrix(n;m;r) nat: uall: [x:A]. B[x] equal: t ∈ T rng: Rng
Definitions unfolded in proof :  true: True rng: Rng nat: matrix-ap: M[i,j] mx: matrix(M[x; y]) matrix-plus: N matrix-minus: -(M) zero-matrix: 0 matrix: Matrix(n;m;r) member: t ∈ T uall: [x:A]. B[x] squash: T prop: and: P ∧ Q subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  rng_zero_wf matrix-ap_wf rng_car_wf nat_wf rng_wf matrix_wf int_seg_wf equal_wf squash_wf true_wf rng_plus_inv iff_weakening_equal
Rules used in proof :  axiomEquality isect_memberEquality hypothesisEquality hypothesis because_Cache setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule rename functionExtensionality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality productElimination imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}[k,m:\mBbbN{}].  \mforall{}[r:Rng].  \mforall{}[N:Matrix(k;m;r)].    (N  +  -(N)  =  0)



Date html generated: 2018_05_21-PM-09_35_23
Last ObjectModification: 2017_12_11-PM-00_29_40

Theory : matrices


Home Index