Nuprl Lemma : omral_times_comm_a
∀g:OCMon. ∀a:CDRng. ∀[ps,qs:|omral(g;a)|]. ((ps ** qs) = (qs ** ps) ∈ |omral(g;a)|)
Proof
Definitions occuring in Statement :
omral_times: ps ** qs,
omralist: omral(g;r),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T,
cdrng: CDRng,
ocmon: OCMon,
set_car: |p|
Definitions unfolded in proof :
comm: Comm(T;op),
infix_ap: x f y
Lemmas referenced :
omral_times_comm
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
sqequalSubstitution,
hypothesis
Latex:
\mforall{}g:OCMon. \mforall{}a:CDRng. \mforall{}[ps,qs:|omral(g;a)|]. ((ps ** qs) = (qs ** ps))
Date html generated:
2016_05_16-AM-08_26_21
Last ObjectModification:
2015_12_28-PM-06_38_23
Theory : polynom_3
Home
Index