### Nuprl Lemma : rng_times_over_minus

`∀[r:Rng]. ∀[a,b:|r|].  ((((-r a) * b) = (-r (a * b)) ∈ |r|) ∧ ((a * (-r b)) = (-r (a * b)) ∈ |r|))`

Proof

Definitions occuring in Statement :  rng: `Rng` rng_times: `*` rng_minus: `-r` rng_car: `|r|` uall: `∀[x:A]. B[x]` infix_ap: `x f y` and: `P ∧ Q` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` rng: `Rng` infix_ap: `x f y` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  rng_car_wf rng_wf rng_plus_cancel_l rng_times_wf rng_minus_wf equal_wf squash_wf true_wf infix_ap_wf rng_plus_wf rng_plus_inv iff_weakening_equal rng_times_over_plus rng_zero_wf rng_times_zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality extract_by_obid isectElimination setElimination rename hypothesisEquality isect_memberEquality because_Cache applyEquality independent_isectElimination lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].    ((((-r  a)  *  b)  =  (-r  (a  *  b)))  \mwedge{}  ((a  *  (-r  b))  =  (-r  (a  *  b))))

Date html generated: 2017_10_01-AM-08_17_27
Last ObjectModification: 2017_02_28-PM-02_02_43

Theory : rings_1

Home Index