Nuprl Lemma : bag-summation-linear1

[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
  ∀a:R. (x∈b). mul f[x] (a mul Σ(x∈b). f[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 so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B prop: squash: T exists: x:A. B[x] infix_ap: y true: True group_p: IsGroup(T;op;id;inv) monoid_p: IsMonoid(T;op;id) guard: {T} ident: Ident(T;op;id) subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q implies:  Q assoc: Assoc(T;op)
Lemmas referenced :  bag-summation-linear equal_wf squash_wf true_wf bag-summation_wf exists_wf group_p_wf comm_wf bilinear_wf bag_wf bag-summation-zero iff_weakening_equal
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation productElimination sqequalRule lambdaEquality cumulativity independent_isectElimination independent_pairFormation dependent_functionElimination hyp_replacement equalitySymmetry applyEquality imageElimination equalityTransitivity universeEquality because_Cache imageMemberEquality baseClosed natural_numberEquality axiomEquality productEquality functionEquality functionExtensionality independent_functionElimination

Latex:
\mforall{}[T,R:Type].  \mforall{}[add,mul:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  R].
    \mforall{}a:R.  (\mSigma{}(x\mmember{}b).  a  mul  f[x]  =  (a  mul  \mSigma{}(x\mmember{}b).  f[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_50_53
Last ObjectModification: 2017_07_26-PM-04_32_58

Theory : bags


Home Index