### Nuprl Lemma : mul_over_minus_fps

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

Proof

Definitions occuring in Statement :  fps-mul: `(f*g)` fps-neg: `-(f)` power-series: `PowerSeries(X;r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` subtype_rel: `A ⊆r B` fps-rng: `fps-rng(r)` rng_car: `|r|` pi1: `fst(t)` rng_times: `*` pi2: `snd(t)` rng_minus: `-r` infix_ap: `x f y` and: `P ∧ Q`
Lemmas referenced :  rng_times_over_minus fps-rng_wf crng_subtype_rng crng_wf deq_wf valueall-type_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis applyEquality sqequalRule isect_memberEquality_alt productElimination independent_pairEquality axiomEquality isectIsTypeImplies inhabitedIsType universeIsType instantiate universeEquality

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

Date html generated: 2020_05_20-AM-09_05_29
Last ObjectModification: 2020_02_03-PM-02_35_57

Theory : power!series

Home Index