### Nuprl Lemma : neg_assoc_fps

`∀[X:Type]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].`
`  (((a+(-(a)+b)) = b ∈ PowerSeries(X;r)) ∧ ((-(a)+(a+b)) = b ∈ PowerSeries(X;r)))`

Proof

Definitions occuring in Statement :  fps-neg: `-(f)` fps-add: `(f+g)` power-series: `PowerSeries(X;r)` 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` and: `P ∧ Q` cand: `A c∧ B` fps-neg: `-(f)` fps-add: `(f+g)` power-series: `PowerSeries(X;r)` fps-coeff: `f[b]` crng: `CRng` rng: `Rng` true: `True` squash: `↓T` prop: `ℙ` infix_ap: `x f y` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  bag_wf power-series_wf crng_wf rng_car_wf rng_minus_wf equal_wf squash_wf true_wf rng_plus_inv_assoc iff_weakening_equal rng_plus_ac_1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule functionExtensionality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_pairFormation because_Cache productElimination independent_pairEquality axiomEquality cumulativity isect_memberEquality universeEquality setElimination rename applyEquality natural_numberEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[a,b:PowerSeries(X;r)].    (((a+(-(a)+b))  =  b)  \mwedge{}  ((-(a)+(a+b))  =  b))

Date html generated: 2018_05_21-PM-09_56_44
Last ObjectModification: 2017_07_26-PM-06_33_04

Theory : power!series

Home Index