Nuprl Lemma : omral_action_times

g:OCMon. ∀r:CDRng. ∀v,w:|r|. ∀ps:|omral(g;r)|.  (((v w) ⋅⋅ ps) (v ⋅⋅ (w ⋅⋅ ps)) ∈ |omral(g;r)|)


Proof




Definitions occuring in Statement :  omral_action: v ⋅⋅ ps omralist: omral(g;r) infix_ap: y all: x:A. B[x] equal: t ∈ T cdrng: CDRng rng_times: * rng_car: |r| ocmon: OCMon set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T infix_ap: y uall: [x:A]. B[x] cdrng: CDRng crng: CRng rng: Rng implies:  Q ocmon: OCMon abmonoid: AbMon mon: Mon subtype_rel: A ⊆B dset: DSet true: True oset_of_ocmon: g↓oset dset_of_mon: g↓set set_car: |p| pi1: fst(t) omralist: omral(g;r) oalist: oal(a;b) dset_set: dset_set mk_dset: mk_dset(T, eq) dset_list: List set_prod: s × t add_grp_of_rng: r↓+gp grp_id: e pi2: snd(t) grp_car: |g| squash: T prop: uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  omral_lookups_same_a omral_action_wf rng_times_wf grp_car_wf set_car_wf omralist_wf dset_wf rng_car_wf cdrng_wf ocmon_wf lookup_wf oset_of_ocmon_wf0 rng_zero_wf infix_ap_wf dset_of_mon_wf0 add_grp_of_rng_wf equal_wf squash_wf true_wf lookup_omral_action iff_weakening_equal rng_times_assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality applyEquality isectElimination setElimination rename hypothesis independent_functionElimination lambdaEquality sqequalRule because_Cache natural_numberEquality functionEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed independent_isectElimination productElimination

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



Date html generated: 2017_10_01-AM-10_06_56
Last ObjectModification: 2017_03_03-PM-01_14_36

Theory : polynom_3


Home Index