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: t ∈ T cdrng: CDRng ocmon: OCMon set_car: |p|
Definitions unfolded in proof :  bilinear: BiLinear(T;pl;tm) infix_ap: 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