Nuprl Lemma : bilinear_comm_elim

[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].
  (BiLinear(T;pl;tm)) supposing ((∀a,x,y:T.  ((a tm (x pl y)) ((a tm x) pl (a tm y)) ∈ T)) and Comm(T;tm))


Definitions occuring in Statement :  bilinear: BiLinear(T;pl;tm) comm: Comm(T;op) uimplies: supposing a uall: [x:A]. B[x] infix_ap: y all: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  bilinear: BiLinear(T;pl;tm) comm: Comm(T;op) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q prop: so_lambda: λ2x.t[x] infix_ap: y so_apply: x[s] all: x:A. B[x] squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  all_wf equal_wf uall_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation hypothesis sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality hypothesisEquality isect_memberEquality isectElimination because_Cache extract_by_obid cumulativity lambdaEquality applyEquality functionExtensionality equalityTransitivity equalitySymmetry functionEquality universeEquality dependent_functionElimination imageElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

\mforall{}[T:Type].  \mforall{}[pl,tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
    (BiLinear(T;pl;tm))  supposing 
          ((\mforall{}a,x,y:T.    ((a  tm  (x  pl  y))  =  ((a  tm  x)  pl  (a  tm  y))))  and 

Date html generated: 2017_10_01-AM-08_12_56
Last ObjectModification: 2017_02_28-PM-01_57_11

Theory : gen_algebra_1

Home Index