Nuprl Lemma : fps-mul-single-general

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


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: supposing a uall: [x:A]. B[x] lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] universe: Type equal: t ∈ T crng: CRng rng_zero: 0
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a crng: CRng comm: Comm(T;op) rng: Rng power-series: PowerSeries(X;r) subtype_rel: A ⊆B all: x:A. B[x] implies:  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: c∧ B squash: T top: Top true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q fps-single: <c> bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else 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: 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

    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[c:bag(X)].  \mforall{}[f:PowerSeries(X;r)].
        ((<c>*f)  =  (\mlambda{}  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