### Nuprl Lemma : fps-compose-fps-product

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f:PowerSeries(X;r)]. ∀[T:Type]. ∀[b:bag(T)]. ∀[G:T ⟶ PowerSeries(X;r)].`
`    (Π(i∈b).G[i](x:=f) = Π(i∈b).G[i](x:=f) ∈ PowerSeries(X;r)) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-compose: `g(x:=f)` fps-product: `Π(x∈b).f[x]` power-series: `PowerSeries(X;r)` bag: `bag(T)` 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]` squash: `↓T` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_apply: `x[s]` subtype_rel: `A ⊆r B` cand: `A c∧ B` implies: `P `` Q` empty-bag: `{}` all: `∀x:A. B[x]` cons-bag: `x.b` prop: `ℙ` infix_ap: `x f y` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` top: `Top` assoc: `Assoc(T;op)` comm: `Comm(T;op)` monoid_p: `IsMonoid(T;op;id)` ident: `Ident(T;op;id)`
Lemmas referenced :  bag_to_squash_list list_induction equal_wf power-series_wf fps-compose_wf bag-summation_wf fps-mul_wf fps-one_wf list-subtype-bag list_wf bag_wf crng_wf deq_wf valueall-type_wf squash_wf true_wf mul_assoc_fps iff_weakening_equal fps-mul-comm single-bag_wf bag-summation-empty fps-compose-one cons-bag-as-append bag-summation-single bag-summation-append mul_one_fps fps-compose-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis rename sqequalRule lambdaEquality cumulativity because_Cache independent_isectElimination applyEquality functionExtensionality independent_pairFormation independent_functionElimination lambdaFormation dependent_functionElimination hyp_replacement equalitySymmetry applyLambdaEquality functionEquality isect_memberEquality axiomEquality universeEquality equalityTransitivity natural_numberEquality imageMemberEquality baseClosed voidElimination voidEquality equalityUniverse levelHypothesis independent_pairEquality

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

Date html generated: 2018_05_21-PM-10_10_10
Last ObjectModification: 2017_07_26-PM-06_34_19

Theory : power!series

Home Index