`∀[X:Type]. ∀[r:CRng]. ∀[c1,c2:|r|]. ∀[f:PowerSeries(X;r)].  ((c1 +r c2)*f = ((c1)*f+(c2)*f) ∈ PowerSeries(X;r))`

Proof

Definitions occuring in Statement :  fps-scalar-mul: `(c)*f` fps-add: `(f+g)` power-series: `PowerSeries(X;r)` uall: `∀[x:A]. B[x]` infix_ap: `x f y` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_plus: `+r` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` infix_ap: `x f y` crng: `CRng` rng: `Rng` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` power-series: `PowerSeries(X;r)` true: `True` fps-scalar-mul: `(c)*f` fps-add: `(f+g)` fps-coeff: `f[b]` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  fps-ext fps-scalar-mul_wf rng_plus_wf fps-add_wf bag_wf power-series_wf rng_car_wf crng_wf rng_times_wf infix_ap_wf equal_wf squash_wf true_wf rng_times_over_plus crng_times_comm iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality cumulativity applyEquality setElimination rename because_Cache hypothesis productElimination independent_isectElimination lambdaFormation sqequalRule isect_memberEquality axiomEquality universeEquality natural_numberEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[c1,c2:|r|].  \mforall{}[f:PowerSeries(X;r)].    ((c1  +r  c2)*f  =  ((c1)*f+(c2)*f))

Date html generated: 2018_05_21-PM-09_57_29
Last ObjectModification: 2017_07_26-PM-06_33_23

Theory : power!series

Home Index