### Nuprl Lemma : fps-mul-single-general

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:bag(X)]. ∀[f:PowerSeries(X;r)].`
`    ((<c>*f) = (λb.case bag-diff(eq;b;c) of inl(d) => f[d] | inr(z) => 0) ∈ PowerSeries(X;r)) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-mul: `(f*g)` fps-single: `<c>` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` bag-diff: `bag-diff(eq;bs;as)` bag: `bag(T)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` lambda: `λx.A[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_zero: `0`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` crng: `CRng` comm: `Comm(T;op)` rng: `Rng` power-series: `PowerSeries(X;r)` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` fps-coeff: `f[b]` fps-mul: `(f*g)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)` pi1: `fst(t)` pi2: `snd(t)` cand: `A c∧ B` squash: `↓T` top: `Top` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` fps-single: `<c>` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` infix_ap: `x f y`
Lemmas referenced :  rng_plus_comm crng_properties rng_properties fps-ext fps-mul_wf fps-single_wf subtype_rel_self bag_wf rng_car_wf bag-diff_wf unit_wf2 fps-coeff_wf rng_zero_wf equal_wf bag-diff-property bag-append_wf all_wf not_wf power-series_wf crng_wf deq_wf valueall-type_wf bag-partitions-with-one-given bag-summation_wf rng_plus_wf rng_times_wf crng_all_properties squash_wf true_wf bag-summation-single pi1_wf_top pi2_wf iff_weakening_equal bag-eq_wf bool_wf eqtt_to_assert assert-bag-eq eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot member_wf rng_times_one bag-summation-filter bag-partitions_wf bag-summation-equal ifthenelse_wf bag-member_wf rng_one_wf rng_times_zero bag-summation-is-zero bag-member-partitions and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis independent_isectElimination applyEquality sqequalRule functionEquality lambdaEquality unionEquality lambdaFormation equalityTransitivity equalitySymmetry unionElimination dependent_functionElimination independent_functionElimination productElimination because_Cache isect_memberEquality axiomEquality universeEquality hyp_replacement applyLambdaEquality productEquality cumulativity independent_pairFormation imageElimination independent_pairEquality voidElimination voidEquality natural_numberEquality imageMemberEquality baseClosed instantiate equalityElimination dependent_pairFormation promote_hyp dependent_set_memberEquality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[c:bag(X)].  \mforall{}[f:PowerSeries(X;r)].
((<c>*f)  =  (\mlambda{}b.case  bag-diff(eq;b;c)  of  inl(d)  =>  f[d]  |  inr(z)  =>  0))
supposing  valueall-type(X)

Date html generated: 2019_10_16-AM-11_34_30
Last ObjectModification: 2018_08_21-PM-01_59_49

Theory : power!series

Home Index