### Nuprl Lemma : fps-product-reindex

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

Proof

Definitions occuring in Statement :  fps-product: `Π(x∈b).f[x]` power-series: `PowerSeries(X;r)` bag-map: `bag-map(f;bs)` bag: `bag(T)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` apply: `f a` 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` comm: `Comm(T;op)` infix_ap: `x f y` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` assoc: `Assoc(T;op)` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  bag-summation-reindex power-series_wf fps-mul_wf fps-one_wf equal_wf squash_wf true_wf fps-mul-comm iff_weakening_equal mul_assoc_fps bag_wf all_wf crng_wf valueall-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis lambdaEquality independent_isectElimination sqequalRule applyEquality imageElimination equalityTransitivity equalitySymmetry because_Cache natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination isect_memberEquality axiomEquality independent_pairFormation functionExtensionality functionEquality

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

Date html generated: 2018_05_21-PM-09_57_11
Last ObjectModification: 2017_07_26-PM-06_33_15

Theory : power!series

Home Index