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