### Nuprl Lemma : fps-scalar-mul-property

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng].`
`    ((IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)`
`    ∧ IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f))`
`    ∧ (∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g)))) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-scalar-mul: `(c)*f` fps-mul: `(f*g)` fps-add: `(f+g)` power-series: `PowerSeries(X;r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` lambda: `λx.A[x]` universe: `Type` crng: `CRng` rng_one: `1` rng_times: `*` rng_plus: `+r` rng_car: `|r|` dist_1op_2op_lr: `Dist1op2opLR(A;1op;2op)` action_p: `IsAction(A;x;e;S;f)` bilinear_p: `IsBilinear(A;B;C;+a;+b;+c;f)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` crng: `CRng` comm: `Comm(T;op)` rng: `Rng` prop: `ℙ` and: `P ∧ Q` cand: `A c∧ B` exists: `∃x:A. B[x]` action_p: `IsAction(A;x;e;S;f)` all: `∀x:A. B[x]` bilinear_p: `IsBilinear(A;B;C;+a;+b;+c;f)` dist_1op_2op_lr: `Dist1op2opLR(A;1op;2op)` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)` infix_ap: `x f y` uiff: `uiff(P;Q)` fps-scalar-mul: `(c)*f` fps-coeff: `f[b]` fps-add: `(f+g)` fps-mul: `(f*g)` power-series: `PowerSeries(X;r)` true: `True` so_lambda: `λ2x.t[x]` pi1: `fst(t)` pi2: `snd(t)` so_apply: `x[s]` top: `Top` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  rng_plus_comm crng_properties rng_properties rng_all_properties ring_p_wf rng_car_wf rng_plus_wf rng_zero_wf rng_minus_wf rng_times_wf rng_one_wf group_p_wf crng_wf deq_wf valueall-type_wf power-series_wf fps-ext fps-scalar-mul_wf bag_wf fps-add_wf fps-mul_wf infix_ap_wf bag-summation_wf bag-partitions_wf pi1_wf_top pi2_wf equal_wf bag-summation-linear1-right iff_weakening_equal bag-summation-equal rng_times_assoc bag-member_wf squash_wf true_wf crng_times_comm crng_times_ac_1 rng_times_one rng_times_over_plus assoc_wf comm_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis dependent_set_memberEquality productElimination because_Cache independent_pairFormation dependent_pairFormation functionExtensionality applyEquality sqequalRule independent_pairEquality isect_memberEquality lambdaEquality dependent_functionElimination axiomEquality cumulativity equalityTransitivity equalitySymmetry universeEquality lambdaFormation independent_isectElimination natural_numberEquality productEquality voidElimination voidEquality imageElimination imageMemberEquality baseClosed independent_functionElimination functionEquality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].
((IsAction(|r|;*;1;PowerSeries(X;r);\mlambda{}c,f.  (c)*f)
\mwedge{}  IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;\mlambda{}f,g.  (f+g);\mlambda{}f,g.  (f+g);\mlambda{}c,f.  (c)*f))
\mwedge{}  (\mforall{}c:|r|.  Dist1op2opLR(PowerSeries(X;r);\mlambda{}f.(c)*f;\mlambda{}f,g.  (f*g))))
supposing  valueall-type(X)

Date html generated: 2018_05_21-PM-09_57_26
Last ObjectModification: 2017_07_26-PM-06_33_21

Theory : power!series

Home Index