Nuprl Lemma : bag-summation-linear

[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].
  ∀a:R. (x∈b). mul (f[x] add g[x]) (a mul (x∈b). f[x] add Σ(x∈b). g[x])) ∈ R) 
  supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)


Proof




Definitions occuring in Statement :  bag-summation: Σ(x∈b). f[x] bag: bag(T) comm: Comm(T;op) uimplies: supposing a uall: [x:A]. B[x] infix_ap: y so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T group_p: IsGroup(T;op;id;inv) bilinear: BiLinear(T;pl;tm)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] and: P ∧ Q exists: x:A. B[x] bag: bag(T) quotient: x,y:A//B[x; y] implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B subtype_rel: A ⊆B group_p: IsGroup(T;op;id;inv) monoid_p: IsMonoid(T;op;id) bag-summation: Σ(x∈b). f[x] bag-accum: bag-accum(v,x.f[v; x];init;bs) top: Top infix_ap: y bilinear: BiLinear(T;pl;tm) true: True squash: T guard: {T} iff: ⇐⇒ Q rev_implies:  Q assoc: Assoc(T;op) comm: Comm(T;op) ident: Ident(T;op;id) inverse: Inverse(T;op;id;inv)
Lemmas referenced :  list_wf quotient-member-eq permutation_wf permutation-equiv equal_wf bag-summation_wf infix_ap_wf list-subtype-bag equal-wf-base exists_wf group_p_wf comm_wf bilinear_wf bag_wf list_induction all_wf list_accum_wf list_accum_nil_lemma list_accum_cons_lemma squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution productElimination thin pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination cumulativity hypothesisEquality rename lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality functionExtensionality applyEquality independent_pairFormation productEquality axiomEquality functionEquality isect_memberEquality universeEquality voidElimination voidEquality natural_numberEquality imageElimination imageMemberEquality baseClosed

Latex:
\mforall{}[T,R:Type].  \mforall{}[add,mul:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[f,g:T  {}\mrightarrow{}  R].
    \mforall{}a:R.  (\mSigma{}(x\mmember{}b).  a  mul  (f[x]  add  g[x])  =  (a  mul  (\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}b).  g[x]))) 
    supposing  (\mexists{}minus:R  {}\mrightarrow{}  R.  IsGroup(R;add;zero;minus))  \mwedge{}  Comm(R;add)  \mwedge{}  BiLinear(R;add;mul)



Date html generated: 2017_10_01-AM-08_48_51
Last ObjectModification: 2017_07_26-PM-04_32_47

Theory : bags


Home Index