### Nuprl Lemma : alg_act_is_rng_chom

`∀a:CRng. ∀m:algebra{i:l}(a).  rng_chom_p(a;m↓rg;λx:|a|. m.act x m.one)`

Proof

Definitions occuring in Statement :  algebra: `algebra{i:l}(A)` rng_of_alg: `a↓rg` alg_act: `a.act` alg_one: `a.one` tlambda: `λx:T. b[x]` all: `∀x:A. B[x]` apply: `f a` rng_chom_p: `rng_chom_p(r;s;f)` crng: `CRng` rng_car: `|r|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` rng_chom_p: `rng_chom_p(r;s;f)` and: `P ∧ Q` rng_hom_p: `rng_hom_p(r;s;f)` fun_thru_2op: `FunThru2op(A;B;opa;opb;f)` uall: `∀[x:A]. B[x]` member: `t ∈ T` rng_of_alg: `a↓rg` rng_car: `|r|` pi1: `fst(t)` tlambda: `λx:T. b[x]` rng_plus: `+r` pi2: `snd(t)` crng: `CRng` rng: `Rng` rng_times: `*` rng_one: `1` squash: `↓T` prop: `ℙ` algebra: `algebra{i:l}(A)` module: `A-Module` infix_ap: `x f y` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  rng_car_wf algebra_wf crng_wf equal_wf squash_wf true_wf alg_car_wf module_act_plus alg_one_wf infix_ap_wf alg_plus_wf alg_act_wf iff_weakening_equal rng_times_wf algebra_act_times_r module_action_p algebra_times_one crng_times_comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation isect_memberFormation introduction cut sqequalRule hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality isect_memberEquality axiomEquality because_Cache dependent_functionElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality productElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}a:CRng.  \mforall{}m:algebra\{i:l\}(a).    rng\_chom\_p(a;m\mdownarrow{}rg;\mlambda{}x:|a|.  m.act  x  m.one)

Date html generated: 2017_10_01-AM-09_52_03
Last ObjectModification: 2017_03_03-PM-00_46_47

Theory : algebras_1

Home Index