### 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))`

Proof

Definitions occuring in Statement :  bilinear: `BiLinear(T;pl;tm)` comm: `Comm(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  bilinear: `BiLinear(T;pl;tm)` comm: `Comm(T;op)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` infix_ap: `x f y` so_apply: `x[s]` all: `∀x:A. B[x]` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` 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

Latex:
\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
Comm(T;tm))

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