### Nuprl Lemma : rng_to_alg_wf

`∀R:CRng. (rng_to_alg(R) ∈ algebra{i:l}(R))`

Proof

Definitions occuring in Statement :  rng_to_alg: `rng_to_alg(r)` algebra: `algebra{i:l}(A)` all: `∀x:A. B[x]` member: `t ∈ T` crng: `CRng`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` crng: `CRng` algebra: `algebra{i:l}(A)` module: `A-Module` rng: `Rng` rng_to_alg: `rng_to_alg(r)` algebra_sig: `algebra_sig{i:l}(A)` alg_car: `a.car` pi1: `fst(t)` alg_plus: `a.plus` pi2: `snd(t)` alg_zero: `a.zero` alg_minus: `a.minus` alg_act: `a.act` ring_p: `IsRing(T;plus;zero;neg;times;one)` and: `P ∧ Q` cand: `A c∧ B` action_p: `IsAction(A;x;e;S;f)` true: `True` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` bilinear_p: `IsBilinear(A;B;C;+a;+b;+c;f)` monoid_p: `IsMonoid(T;op;id)` assoc: `Assoc(T;op)` ident: `Ident(T;op;id)` alg_times: `a.times` alg_one: `a.one` dist_1op_2op_lr: `Dist1op2opLR(A;1op;2op)` infix_ap: `x f y` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  crng_properties crng_wf rng_properties rng_car_wf rng_eq_wf rng_le_wf rng_plus_wf rng_zero_wf rng_minus_wf rng_times_wf rng_one_wf rng_div_wf unit_wf2 bool_wf rng_plus_comm2 infix_ap_wf equal_wf squash_wf true_wf rng_times_assoc iff_weakening_equal rng_times_one rng_times_over_plus group_p_wf alg_car_wf alg_plus_wf alg_zero_wf alg_minus_wf comm_wf action_p_wf alg_act_wf bilinear_p_wf crng_times_ac_1 ring_p_wf monoid_p_wf alg_times_wf alg_one_wf bilinear_wf all_wf dist_1op_2op_lr_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename dependent_set_memberEquality dependent_pairEquality because_Cache functionEquality productEquality unionEquality cumulativity sqequalRule productElimination independent_pairFormation isect_memberFormation lambdaEquality dependent_functionElimination axiomEquality isect_memberEquality natural_numberEquality applyEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination independent_pairEquality

Latex:
\mforall{}R:CRng.  (rng\_to\_alg(R)  \mmember{}  algebra\{i:l\}(R))

Date html generated: 2017_10_01-AM-09_52_01
Last ObjectModification: 2017_03_03-PM-00_46_53

Theory : algebras_1

Home Index