### Nuprl Lemma : omral_action_times_r1

`∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps,qs:|omral(g;r)|.  ((v ⋅⋅ (ps ** qs)) = ((v ⋅⋅ ps) ** qs) ∈ |omral(g;r)|)`

Proof

Definitions occuring in Statement :  omral_action: `v ⋅⋅ ps` omral_times: `ps ** qs` omralist: `omral(g;r)` all: `∀x:A. B[x]` equal: `s = t ∈ T` cdrng: `CDRng` rng_car: `|r|` ocmon: `OCMon` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` uall: `∀[x:A]. B[x]` ocmon: `OCMon` abmonoid: `AbMon` mon: `Mon` subtype_rel: `A ⊆r B` dset: `DSet` cdrng: `CDRng` crng: `CRng` rng: `Rng` squash: `↓T` prop: `ℙ` infix_ap: `x f y` omon: `OMon` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff` so_apply: `x[s]` cand: `A c∧ B` abgrp: `AbGrp` grp: `Group{i}` iabmonoid: `IAbMonoid` imon: `IMonoid` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` set_car: `|p|` pi1: `fst(t)` add_grp_of_rng: `r↓+gp` grp_car: `|g|` omralist: `omral(g;r)` oalist: `oal(a;b)` dset_set: dset_set mk_dset: `mk_dset(T, eq)` dset_list: `s List` set_prod: `s × t` grp_id: `e` pi2: `snd(t)` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rng_mssum: rng_mssum loset: `LOSet` poset: `POSet{i}` qoset: `QOSet`
Lemmas referenced :  omral_lookups_same_a omral_action_wf omral_times_wf2 grp_car_wf set_car_wf omralist_wf dset_wf rng_car_wf cdrng_wf ocmon_wf equal_wf squash_wf true_wf lookup_omral_action rng_times_wf lookup_omral_times mset_for_functionality oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf assert_wf infix_ap_wf bool_wf grp_le_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf add_grp_of_rng_wf_b grp_sig_wf monoid_p_wf grp_id_wf inverse_wf grp_inv_wf comm_wf set_wf mset_for_wf rng_when_wf oset_of_ocmon_wf0 dset_of_mon_wf0 add_grp_of_rng_wf lookup_wf rng_zero_wf omral_dom_wf rng_wf mset_mem_wf iff_weakening_equal loset_wf mset_for_functionality_wrt_bsubmset mset_diff_wf omral_dom_action assert_functionality_wrt_uiff bnot_wf mset_mem_diff omral_dom_wf2 iff_transitivity not_wf iff_weakening_uiff assert_of_band assert_of_bnot lookup_omral_eq_zero rng_times_zero rng_when_of_zero mset_for_of_id rng_times_mssum_l rng_mssum_wf rng_mssum_functionality_wrt_equal rng_times_when_l rng_times_assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis independent_functionElimination isectElimination setElimination rename applyEquality lambdaEquality sqequalRule because_Cache imageElimination equalityTransitivity equalitySymmetry universeEquality instantiate productEquality cumulativity functionEquality unionElimination equalityElimination productElimination independent_isectElimination setEquality independent_pairFormation natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}v:|r|.  \mforall{}ps,qs:|omral(g;r)|.    ((v  \mcdot{}\mcdot{}  (ps  **  qs))  =  ((v  \mcdot{}\mcdot{}  ps)  **  qs))

Date html generated: 2017_10_01-AM-10_07_00
Last ObjectModification: 2017_03_03-PM-01_16_24

Theory : polynom_3

Home Index