Nuprl Lemma : omral_bilinear_a
∀g:OCMon. ∀a:CDRng.
∀[ps,qs,rs:|omral(g;a)|].
(((ps ** (qs ++ rs)) = ((ps ** qs) ++ (ps ** rs)) ∈ |omral(g;a)|)
∧ (((qs ++ rs) ** ps) = ((qs ** ps) ++ (rs ** ps)) ∈ |omral(g;a)|))
Proof
Definitions occuring in Statement :
omral_times: ps ** qs,
omral_plus: ps ++ qs,
omralist: omral(g;r),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
cdrng: CDRng,
ocmon: OCMon,
set_car: |p|
Definitions unfolded in proof :
bilinear: BiLinear(T;pl;tm),
infix_ap: x f y
Lemmas referenced :
omral_bilinear
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,rs:|omral(g;a)|].
(((ps ** (qs ++ rs)) = ((ps ** qs) ++ (ps ** rs)))
\mwedge{} (((qs ++ rs) ** ps) = ((qs ** ps) ++ (rs ** ps))))
Date html generated:
2016_05_16-AM-08_26_29
Last ObjectModification:
2015_12_28-PM-06_38_19
Theory : polynom_3
Home
Index