### Nuprl Lemma : fps-mul-assoc

`∀[X:Type]. ∀[eq:EqDecider(X)].`
`  ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)].  (((f*g)*h) = (f*(g*h)) ∈ PowerSeries(X;r)) supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-mul: `(f*g)` power-series: `PowerSeries(X;r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  implies: `P `` Q` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` squash: `↓T` ring_p: `IsRing(T;plus;zero;neg;times;one)` true: `True` top: `Top` so_apply: `x[s]` pi2: `snd(t)` pi1: `fst(t)` so_lambda: `λ2x.t[x]` prop: `ℙ` rng: `Rng` exists: `∃x:A. B[x]` infix_ap: `x f y` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` fps-mul: `(f*g)` cand: `A c∧ B` and: `P ∧ Q` comm: `Comm(T;op)` crng: `CRng` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` group_p: `IsGroup(T;op;id;inv)`
Lemmas referenced :  bag-summation-linear1-right iff_weakening_equal bag-summation-linear1 true_wf squash_wf equal_wf pi1_wf_top pi2_wf bag-partitions_wf fps-coeff_wf rng_times_wf infix_ap_wf bag-summation_wf valueall-type_wf power-series_wf bag_wf rng_zero_wf rng_plus_wf rng_car_wf group_p_wf rng_properties crng_properties rng_minus_wf rng_all_properties rng_plus_comm bag-double-summation bag-map_wf bag-combine_wf bag-summation-map istype-universe bag-partitions-assoc pi1_wf subtype_rel_self rng_times_assoc
Rules used in proof :  independent_functionElimination universeEquality baseClosed imageMemberEquality dependent_functionElimination imageElimination natural_numberEquality voidEquality voidElimination independent_pairEquality independent_isectElimination productEquality equalitySymmetry equalityTransitivity axiomEquality isect_memberEquality cumulativity applyEquality functionExtensionality dependent_pairFormation lambdaEquality sqequalRule independent_pairFormation productElimination because_Cache hypothesis hypothesisEquality rename setElimination thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution hyp_replacement lambdaEquality_alt universeIsType instantiate inhabitedIsType productIsType lambdaFormation_alt equalityIstype applyLambdaEquality

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].
\mforall{}[r:CRng].  \mforall{}[f,g,h:PowerSeries(X;r)].    (((f*g)*h)  =  (f*(g*h)))  supposing  valueall-type(X)

Date html generated: 2020_05_20-AM-09_05_25
Last ObjectModification: 2020_01_27-PM-04_14_20

Theory : power!series

Home Index