Nuprl Lemma : zero-vector-add-left

[i:Type]. ∀[r:Rng]. ∀[a:i ⟶ |r|].  ((0 a) a ∈ (i ⟶ |r|))


Proof




Definitions occuring in Statement :  zero-vector: 0 vector-add: (a b) uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T rng: Rng rng_car: |r|
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T zero-vector: 0 vector-add: (a b) and: P ∧ Q rng: Rng
Lemmas referenced :  rng_plus_zero rng_car_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut functionExtensionality sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality productElimination hypothesis functionEquality setElimination rename isect_memberEquality axiomEquality because_Cache universeEquality

Latex:
\mforall{}[i:Type].  \mforall{}[r:Rng].  \mforall{}[a:i  {}\mrightarrow{}  |r|].    ((0  +  a)  =  a)



Date html generated: 2018_05_21-PM-09_40_48
Last ObjectModification: 2018_05_19-PM-04_33_09

Theory : matrices


Home Index