Nuprl Lemma : fps-product-single

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[t:T].`
`    (Π(x∈{t}).f[x] = f[t] ∈ PowerSeries(X;r)) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-product: `Π(x∈b).f[x]` power-series: `PowerSeries(X;r)` single-bag: `{x}` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` fps-product: `Π(x∈b).f[x]` bag-product: `Πx ∈ b. f[x]` and: `P ∧ Q` cand: `A c∧ B` monoid_p: `IsMonoid(T;op;id)` assoc: `Assoc(T;op)` infix_ap: `x f y` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` ident: `Ident(T;op;id)` comm: `Comm(T;op)` so_apply: `x[s]` prop: `ℙ` so_lambda: `λ2x.t[x]`
Lemmas referenced :  power-series_wf crng_wf deq_wf valueall-type_wf fps-mul_wf fps-one_wf equal_wf mul_assoc_fps iff_weakening_equal fps-mul-comm squash_wf true_wf bag-summation-single mul_one_fps
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis hypothesisEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality because_Cache functionEquality cumulativity extract_by_obid universeEquality equalityTransitivity equalitySymmetry lambdaEquality independent_isectElimination independent_pairFormation applyEquality imageElimination natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination independent_pairEquality functionExtensionality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  PowerSeries(X;r)].  \mforall{}[t:T].
(\mPi{}(x\mmember{}\{t\}).f[x]  =  f[t])
supposing  valueall-type(X)

Date html generated: 2018_05_21-PM-09_57_16
Last ObjectModification: 2017_07_26-PM-06_33_18

Theory : power!series

Home Index