Nuprl Lemma : itermMultiply_functionality_wrt_ringeq

[r:Rng]. ∀[a,b,c,d:int_term()].  (a (*) c ≡ (*) d) supposing (a ≡ and c ≡ d)


Definitions occuring in Statement :  ringeq_int_terms: t1 ≡ t2 rng: Rng itermMultiply: left (*) right int_term: int_term() uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  implies:  Q rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q guard: {T} subtype_rel: A ⊆B true: True infix_ap: y rng: Rng prop: squash: T int_term_ind: int_term_ind itermMultiply: left (*) right ring_term_value: ring_term_value(f;t) all: x:A. B[x] ringeq_int_terms: t1 ≡ t2 uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_wf int_term_wf ringeq_int_terms_wf iff_weakening_equal infix_ap_wf rng_times_wf rng_car_wf true_wf squash_wf equal_wf
Rules used in proof :  isect_memberEquality axiomEquality intEquality functionEquality independent_functionElimination productElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality because_Cache rename setElimination universeEquality equalitySymmetry equalityTransitivity isectElimination extract_by_obid imageElimination lambdaEquality applyEquality sqequalRule hypothesisEquality thin dependent_functionElimination hypothesis lambdaFormation sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

\mforall{}[r:Rng].  \mforall{}[a,b,c,d:int\_term()].    (a  (*)  c  \mequiv{}  b  (*)  d)  supposing  (a  \mequiv{}  b  and  c  \mequiv{}  d)

Date html generated: 2018_05_21-PM-03_16_17
Last ObjectModification: 2018_01_25-PM-02_19_15

Theory : rings_1

Home Index