Nuprl Lemma : lookup_omral_times_a
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|. ∀z:|g|.
(((ps ** qs)[z]) = (Σx ∈ dom(ps). Σy ∈ dom(qs). (when (x * y) =b z. ((ps[x]) * (qs[y])))) ∈ |r|)
Proof
Definitions occuring in Statement :
omral_times: ps ** qs,
omral_dom: dom(ps),
omralist: omral(g;r),
lookup: as[k],
rng_mssum: rng_mssum,
infix_ap: x f y,
all: ∀x:A. B[x],
equal: s = t ∈ T,
rng_when: rng_when,
cdrng: CDRng,
rng_times: *,
rng_zero: 0,
rng_car: |r|,
oset_of_ocmon: g↓oset,
ocmon: OCMon,
grp_op: *,
grp_eq: =b,
grp_car: |g|,
set_car: |p|
Definitions unfolded in proof :
rng_mssum: rng_mssum
Lemmas referenced :
lookup_omral_times
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}g:OCMon. \mforall{}r:CDRng. \mforall{}ps,qs:|omral(g;r)|. \mforall{}z:|g|.
(((ps ** qs)[z]) = (\mSigma{}x \mmember{} dom(ps). \mSigma{}y \mmember{} dom(qs). (when (x * y) =\msubb{} z. ((ps[x]) * (qs[y])))))
Date html generated:
2016_05_16-AM-08_25_45
Last ObjectModification:
2015_12_28-PM-06_38_39
Theory : polynom_3
Home
Index