### Nuprl Lemma : omral_plus_non_zero_vals

`∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.`
`  ((¬↑(0 ∈b map(λx.(snd(x));ps))) `` (¬↑(0 ∈b map(λx.(snd(x));qs))) `` (¬↑(0 ∈b map(λx.(snd(x));ps ++ qs))))`

Proof

Definitions occuring in Statement :  omral_plus: `ps ++ qs` mem: `a ∈b as` map: `map(f;as)` list: `T List` assert: `↑b` pi2: `snd(t)` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` lambda: `λx.A[x]` product: `x:A × B[x]` add_grp_of_rng: `r↓+gp` cdrng: `CDRng` rng_zero: `0` rng_car: `|r|` ocmon: `OCMon` dset_of_mon: `g↓set` grp_car: `|g|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` ocmon: `OCMon` omon: `OMon` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` abmonoid: `AbMon` mon: `Mon` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` 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` infix_ap: `x f y` so_apply: `x[s]` cand: `A c∧ B` 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|` grp_id: `e` pi2: `snd(t)` omral_plus: `ps ++ qs`
Lemmas referenced :  oal_merge_non_id_vals oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf cdrng_wf ocmon_wf cdrng_is_abdmonoid
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:(|g|  \mtimes{}  |r|)  List.
((\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
{}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs)))
{}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps  ++  qs))))

Date html generated: 2017_10_01-AM-10_05_10
Last ObjectModification: 2017_03_03-PM-01_10_37

Theory : polynom_3

Home Index